Add --separation option

This commit is contained in:
Joscha 2025-02-06 22:40:25 +01:00
parent c354ba2151
commit 8ae97b410d
5 changed files with 19 additions and 11 deletions

View file

@ -19,6 +19,7 @@ class Conf(args: Seq[String]) extends ScallopConf(args):
val useScalaDocstringRegexes: ScallopOption[Boolean] = opt[Boolean]() val useScalaDocstringRegexes: ScallopOption[Boolean] = opt[Boolean]()
val noHeuristics: ScallopOption[Boolean] = opt[Boolean]() val noHeuristics: ScallopOption[Boolean] = opt[Boolean]()
val indent: ScallopOption[Int] = opt[Int](default = Some(2)) 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)) val lineOverhang: ScallopOption[Int] = opt[Int](default = Some(0))
verify() verify()
@ -35,6 +36,7 @@ def main(args: String*): Unit =
lineRe = conf.lineRegex.map(Regex(_)).getOrElse(defaultLineRe), lineRe = conf.lineRegex.map(Regex(_)).getOrElse(defaultLineRe),
heuristics = !conf.noHeuristics(), heuristics = !conf.noHeuristics(),
indent = conf.indent(), indent = conf.indent(),
separation = conf.separation(),
lineOverhang = conf.lineOverhang(), lineOverhang = conf.lineOverhang(),
) )

View file

@ -7,10 +7,17 @@ import scala.util.boundary
import scala.util.matching.Regex import scala.util.matching.Regex
import scala.util.matching.Regex.Match 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 blockReI = blockRe.pattern.namedGroups().get("block")
private val lineReI = lineRe.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: private def parseBlockLine(line: String): Option[Block] = boundary:
val m = lineRe.findFirstMatchIn(line).getOrElse(boundary.break(None)) val m = lineRe.findFirstMatchIn(line).getOrElse(boundary.break(None))

View file

@ -12,17 +12,16 @@ case class FormattedProofTree(lines: Lines, conclusionStart: Int, conclusionEnd:
def extend(line: Line): FormattedProofTree = copy(lines = lines.extend(line)) 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 def toLines: IndexedSeq[String] = lines.toLines
object FormattedProofTree: object FormattedProofTree:
val separation = 3
def empty: FormattedProofTree = FormattedProofTree(lines = Lines.empty, conclusionStart = 0, conclusionEnd = 0) def empty: FormattedProofTree = FormattedProofTree(lines = Lines.empty, conclusionStart = 0, conclusionEnd = 0)
def joinHorizontally(left: FormattedProofTree, right: FormattedProofTree): FormattedProofTree = def joinHorizontally(left: FormattedProofTree, right: FormattedProofTree, separation: Int): FormattedProofTree =
val (lines, deltaRight) = left.lines.joinHorizontally(right.lines) val (lines, deltaRight) = left.lines.joinHorizontally(right.lines, separation)
FormattedProofTree( FormattedProofTree(
lines = lines, lines = lines,
conclusionStart = left.conclusionStart min (right.conclusionStart + deltaRight), conclusionStart = left.conclusionStart min (right.conclusionStart + deltaRight),

View file

@ -7,7 +7,7 @@ case class Lines(lines: IndexedSeq[Line]):
def shift(delta: Int): Lines = Lines(lines.map(_.shift(delta))) def shift(delta: Int): Lines = Lines(lines.map(_.shift(delta)))
def extend(line: Line): Lines = Lines(line +: lines) 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) 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 = result.max(minDelta(left.at(y), right.at(y + 1), separation))
result 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 deltaRight = minDeltaForVisualSeparation(left, right, separation)
val lines = val lines =
for y <- 0 until (left.height max right.height) yield (left.at(y), right.at(y)) match for y <- 0 until (left.height max right.height) yield (left.at(y), right.at(y)) match

View file

@ -1,6 +1,6 @@
package de.plugh.asciiprooftree.tree 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 = private def formatLine(start: Int, end: Int, rule: String): Line =
val lineStart = start - lineOverhang val lineStart = start - lineOverhang
val lineEnd = end + lineOverhang val lineEnd = end + lineOverhang
@ -12,7 +12,7 @@ case class ProofTreeFormatter(lineOverhang: Int = 0):
val fPremises = tree val fPremises = tree
.premises .premises
.map(formatTree) .map(formatTree)
.reduceOption(_.joinHorizontally(_)) .reduceOption(_.joinHorizontally(_, separation))
.getOrElse(FormattedProofTree.empty) .getOrElse(FormattedProofTree.empty)
val lConclusion = tree.conclusion match val lConclusion = tree.conclusion match