diff --git a/src/main/scala/de/plugh/asciiprooftree/Main.scala b/src/main/scala/de/plugh/asciiprooftree/Main.scala index 9bc9a8d..3d29f66 100644 --- a/src/main/scala/de/plugh/asciiprooftree/Main.scala +++ b/src/main/scala/de/plugh/asciiprooftree/Main.scala @@ -19,6 +19,7 @@ class Conf(args: Seq[String]) extends ScallopConf(args): val useScalaDocstringRegexes: ScallopOption[Boolean] = opt[Boolean]() val noHeuristics: ScallopOption[Boolean] = opt[Boolean]() val indent: ScallopOption[Int] = opt[Int](default = Some(2)) + val separation: ScallopOption[Int] = opt[Int](default = Some(3)) val lineOverhang: ScallopOption[Int] = opt[Int](default = Some(0)) verify() @@ -35,6 +36,7 @@ def main(args: String*): Unit = lineRe = conf.lineRegex.map(Regex(_)).getOrElse(defaultLineRe), heuristics = !conf.noHeuristics(), indent = conf.indent(), + separation = conf.separation(), lineOverhang = conf.lineOverhang(), ) diff --git a/src/main/scala/de/plugh/asciiprooftree/file/FileFormatter.scala b/src/main/scala/de/plugh/asciiprooftree/file/FileFormatter.scala index 12b7a0e..d588bec 100644 --- a/src/main/scala/de/plugh/asciiprooftree/file/FileFormatter.scala +++ b/src/main/scala/de/plugh/asciiprooftree/file/FileFormatter.scala @@ -7,10 +7,17 @@ import scala.util.boundary import scala.util.matching.Regex import scala.util.matching.Regex.Match -case class FileFormatter(blockRe: Regex, lineRe: Regex, heuristics: Boolean, indent: Int, lineOverhang: Int): +case class FileFormatter( + blockRe: Regex, + lineRe: Regex, + heuristics: Boolean, + indent: Int, + separation: Int, + lineOverhang: Int, +): private val blockReI = blockRe.pattern.namedGroups().get("block") private val lineReI = lineRe.pattern.namedGroups().get("block") - private val proofTreeFormatter = ProofTreeFormatter(lineOverhang = lineOverhang) + private val proofTreeFormatter = ProofTreeFormatter(separation = separation, lineOverhang = lineOverhang) private def parseBlockLine(line: String): Option[Block] = boundary: val m = lineRe.findFirstMatchIn(line).getOrElse(boundary.break(None)) diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala b/src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala index 21d7225..a6f0b60 100644 --- a/src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala +++ b/src/main/scala/de/plugh/asciiprooftree/tree/FormattedProofTree.scala @@ -12,17 +12,16 @@ case class FormattedProofTree(lines: Lines, conclusionStart: Int, conclusionEnd: def extend(line: Line): FormattedProofTree = copy(lines = lines.extend(line)) - def joinHorizontally(right: FormattedProofTree): FormattedProofTree = FormattedProofTree.joinHorizontally(this, right) + def joinHorizontally(right: FormattedProofTree, separation: Int): FormattedProofTree = FormattedProofTree + .joinHorizontally(this, right, separation) def toLines: IndexedSeq[String] = lines.toLines object FormattedProofTree: - val separation = 3 - def empty: FormattedProofTree = FormattedProofTree(lines = Lines.empty, conclusionStart = 0, conclusionEnd = 0) - def joinHorizontally(left: FormattedProofTree, right: FormattedProofTree): FormattedProofTree = - val (lines, deltaRight) = left.lines.joinHorizontally(right.lines) + def joinHorizontally(left: FormattedProofTree, right: FormattedProofTree, separation: Int): FormattedProofTree = + val (lines, deltaRight) = left.lines.joinHorizontally(right.lines, separation) FormattedProofTree( lines = lines, conclusionStart = left.conclusionStart min (right.conclusionStart + deltaRight), diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala b/src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala index 49ddad1..78313ad 100644 --- a/src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala +++ b/src/main/scala/de/plugh/asciiprooftree/tree/Lines.scala @@ -7,7 +7,7 @@ case class Lines(lines: IndexedSeq[Line]): def shift(delta: Int): Lines = Lines(lines.map(_.shift(delta))) def extend(line: Line): Lines = Lines(line +: lines) - def joinHorizontally(right: Lines): (Lines, Int) = Lines.joinHorizontally(this, right) + def joinHorizontally(right: Lines, separation: Int): (Lines, Int) = Lines.joinHorizontally(this, right, separation) def toLines: IndexedSeq[String] = lines.reverse.map(_.toString) @@ -26,7 +26,7 @@ object Lines: result = result.max(minDelta(left.at(y), right.at(y + 1), separation)) result - def joinHorizontally(left: Lines, right: Lines, separation: Int = 3): (Lines, Int) = + def joinHorizontally(left: Lines, right: Lines, separation: Int): (Lines, Int) = val deltaRight = minDeltaForVisualSeparation(left, right, separation) val lines = for y <- 0 until (left.height max right.height) yield (left.at(y), right.at(y)) match diff --git a/src/main/scala/de/plugh/asciiprooftree/tree/ProofTreeFormatter.scala b/src/main/scala/de/plugh/asciiprooftree/tree/ProofTreeFormatter.scala index 57b131d..a9d5463 100644 --- a/src/main/scala/de/plugh/asciiprooftree/tree/ProofTreeFormatter.scala +++ b/src/main/scala/de/plugh/asciiprooftree/tree/ProofTreeFormatter.scala @@ -1,6 +1,6 @@ package de.plugh.asciiprooftree.tree -case class ProofTreeFormatter(lineOverhang: Int = 0): +case class ProofTreeFormatter(separation: Int = 3, lineOverhang: Int = 0): private def formatLine(start: Int, end: Int, rule: String): Line = val lineStart = start - lineOverhang val lineEnd = end + lineOverhang @@ -12,7 +12,7 @@ case class ProofTreeFormatter(lineOverhang: Int = 0): val fPremises = tree .premises .map(formatTree) - .reduceOption(_.joinHorizontally(_)) + .reduceOption(_.joinHorizontally(_, separation)) .getOrElse(FormattedProofTree.empty) val lConclusion = tree.conclusion match