From fac0f3605d1d43677b0a5d6469cf44909ea02923 Mon Sep 17 00:00:00 2001 From: Joscha Date: Thu, 6 Feb 2025 22:09:03 +0100 Subject: [PATCH] Use heuristics to detect whether a block contains a tree --- src/main/scala/de/plugh/asciiprooftree/Main.scala | 11 ++++++++--- .../de/plugh/asciiprooftree/file/Formatter.scala | 3 ++- .../de/plugh/asciiprooftree/tree/ProofTree.scala | 2 ++ 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/main/scala/de/plugh/asciiprooftree/Main.scala b/src/main/scala/de/plugh/asciiprooftree/Main.scala index ccf9943..e814a07 100644 --- a/src/main/scala/de/plugh/asciiprooftree/Main.scala +++ b/src/main/scala/de/plugh/asciiprooftree/Main.scala @@ -12,16 +12,21 @@ val lineRe = "^\\s*ยง(?.*)$".r class Conf(args: Seq[String]) extends ScallopConf(args): val path: ScallopOption[Path] = trailArg[Path]() - val indent: ScallopOption[Int] = opt[Int](default = Some(2)) val blockRegex: ScallopOption[String] = opt[String](default = Some(blockRe.regex)) val lineRegex: ScallopOption[String] = opt[String](default = Some(lineRe.regex)) + val indent: ScallopOption[Int] = opt[Int](default = Some(2)) + val noHeuristics: ScallopOption[Boolean] = opt[Boolean]() verify() @main def main(args: String*): Unit = val conf = new Conf(args) - val formatter = - Formatter(indent = conf.indent(), blockRe = Regex(conf.blockRegex()), lineRe = Regex(conf.lineRegex())) + val formatter = Formatter( + blockRe = Regex(conf.blockRegex()), + lineRe = Regex(conf.lineRegex()), + indent = conf.indent(), + heuristics = !conf.noHeuristics(), + ) reformat(conf.path(), formatter) def reformat(path: Path, formatter: Formatter): Unit = diff --git a/src/main/scala/de/plugh/asciiprooftree/file/Formatter.scala b/src/main/scala/de/plugh/asciiprooftree/file/Formatter.scala index 752037f..540e90a 100644 --- a/src/main/scala/de/plugh/asciiprooftree/file/Formatter.scala +++ b/src/main/scala/de/plugh/asciiprooftree/file/Formatter.scala @@ -7,7 +7,7 @@ import scala.util.boundary import scala.util.matching.Regex import scala.util.matching.Regex.Match -case class Formatter(indent: Int, blockRe: Regex, lineRe: Regex): +case class Formatter(blockRe: Regex, lineRe: Regex, indent: Int, heuristics: Boolean): private val blockReI = blockRe.pattern.namedGroups().get("block") private val lineReI = lineRe.pattern.namedGroups().get("block") @@ -26,6 +26,7 @@ case class Formatter(indent: Int, blockRe: Regex, lineRe: Regex): private def parseBlock(text: String, m: Match): Option[BlockInfo] = boundary: val block = parseBlockLines(m.group(blockReI)).getOrElse(boundary.break(None)) val tree = Parser(block.content).parse.getOrElse(boundary.break(None)) + if heuristics && tree.containsNoLines then return None Some(BlockInfo( block = block, tree = tree, diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala b/src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala index f40855b..dbe6114 100644 --- a/src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala +++ b/src/main/scala/de/plugh/asciiprooftree/tree/ProofTree.scala @@ -43,6 +43,8 @@ case class ProofTree(premises: Seq[ProofTree] = Seq(), line: Option[String] = No combined.copy(conclusionStart = belowCentered.start, conclusionEnd = belowCentered.end) + def containsNoLines: Boolean = line.isEmpty && premises.forall(_.containsNoLines) + object ProofTree: def empty: ProofTree = ProofTree() def star: ProofTree = ProofTree().addConclusion("*")