Add --line-overhang option

This commit is contained in:
Joscha 2025-02-06 22:36:24 +01:00
parent fca156e1cc
commit c354ba2151
6 changed files with 56 additions and 41 deletions

View file

@ -1,6 +1,6 @@
package de.plugh.asciiprooftree package de.plugh.asciiprooftree
import de.plugh.asciiprooftree.file.Formatter import de.plugh.asciiprooftree.file.FileFormatter
import org.rogach.scallop.* import org.rogach.scallop.*
import java.nio.file.{Files, Path} import java.nio.file.{Files, Path}
@ -17,8 +17,9 @@ class Conf(args: Seq[String]) extends ScallopConf(args):
val blockRegex: ScallopOption[String] = opt[String]() val blockRegex: ScallopOption[String] = opt[String]()
val lineRegex: ScallopOption[String] = opt[String]() val lineRegex: ScallopOption[String] = opt[String]()
val useScalaDocstringRegexes: ScallopOption[Boolean] = opt[Boolean]() val useScalaDocstringRegexes: ScallopOption[Boolean] = opt[Boolean]()
val indent: ScallopOption[Int] = opt[Int](default = Some(2))
val noHeuristics: ScallopOption[Boolean] = opt[Boolean]() val noHeuristics: ScallopOption[Boolean] = opt[Boolean]()
val indent: ScallopOption[Int] = opt[Int](default = Some(2))
val lineOverhang: ScallopOption[Int] = opt[Int](default = Some(0))
verify() verify()
@main @main
@ -29,16 +30,17 @@ def main(args: String*): Unit =
if conf.useScalaDocstringRegexes() then (scalaDocstringBlockRe, scalaDocstringLineRe) if conf.useScalaDocstringRegexes() then (scalaDocstringBlockRe, scalaDocstringLineRe)
else (markerBlockRe, markerLineRe) else (markerBlockRe, markerLineRe)
val formatter = Formatter( val formatter = FileFormatter(
blockRe = conf.blockRegex.map(Regex(_)).getOrElse(defaultBlockRe), blockRe = conf.blockRegex.map(Regex(_)).getOrElse(defaultBlockRe),
lineRe = conf.lineRegex.map(Regex(_)).getOrElse(defaultLineRe), lineRe = conf.lineRegex.map(Regex(_)).getOrElse(defaultLineRe),
indent = conf.indent(),
heuristics = !conf.noHeuristics(), heuristics = !conf.noHeuristics(),
indent = conf.indent(),
lineOverhang = conf.lineOverhang(),
) )
reformat(conf.path(), formatter) reformat(conf.path(), formatter)
def reformat(path: Path, formatter: Formatter): Unit = def reformat(path: Path, formatter: FileFormatter): Unit =
if Files.isDirectory(path) then if Files.isDirectory(path) then
val files = Files.list(path).toScala(Seq) val files = Files.list(path).toScala(Seq)
for file <- files do reformat(file, formatter) for file <- files do reformat(file, formatter)

View file

@ -1,15 +1,16 @@
package de.plugh.asciiprooftree.file package de.plugh.asciiprooftree.file
import de.plugh.asciiprooftree.tree.Parser import de.plugh.asciiprooftree.tree.{Parser, ProofTreeFormatter}
import scala.collection.mutable import scala.collection.mutable
import scala.util.boundary 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 Formatter(blockRe: Regex, lineRe: Regex, indent: Int, heuristics: Boolean): case class FileFormatter(blockRe: Regex, lineRe: Regex, heuristics: Boolean, indent: 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 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))
@ -46,7 +47,8 @@ case class Formatter(blockRe: Regex, lineRe: Regex, indent: Int, heuristics: Boo
for info <- findBlocks(cleanText) do for info <- findBlocks(cleanText) do
if resultEnd < info.start then result.append(cleanText.slice(resultEnd, info.start)) if resultEnd < info.start then result.append(cleanText.slice(resultEnd, info.start))
val block = info.block.replace(info.tree.formatted.toString.linesIterator.toIndexedSeq) // Clunky :D val formattedTree = proofTreeFormatter.formatTree(info.tree)
val block = info.block.replace(formattedTree.shiftAlignLeft.toLines)
result.append(block.toLines(indent).mkString("\n")) result.append(block.toLines(indent).mkString("\n"))
if info.endsWithNewline then result.append("\n") if info.endsWithNewline then result.append("\n")
resultEnd = info.end resultEnd = info.end

View file

@ -7,11 +7,14 @@ case class FormattedProofTree(lines: Lines, conclusionStart: Int, conclusionEnd:
conclusionEnd = conclusionEnd + delta, conclusionEnd = conclusionEnd + delta,
) )
/** Shift so that the start is always zero. */
def shiftAlignLeft: FormattedProofTree = shift(-lines.lines.map(_.start).minOption.getOrElse(0))
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): FormattedProofTree = FormattedProofTree.joinHorizontally(this, right)
override def toString: String = lines.toString def toLines: IndexedSeq[String] = lines.toLines
object FormattedProofTree: object FormattedProofTree:
val separation = 3 val separation = 3

View file

@ -9,7 +9,7 @@ case class Lines(lines: IndexedSeq[Line]):
def joinHorizontally(right: Lines): (Lines, Int) = Lines.joinHorizontally(this, right) def joinHorizontally(right: Lines): (Lines, Int) = Lines.joinHorizontally(this, right)
override def toString: String = lines.reverse.mkString("\n") def toLines: IndexedSeq[String] = lines.reverse.map(_.toString)
object Lines: object Lines:
def empty: Lines = Lines(IndexedSeq()) def empty: Lines = Lines(IndexedSeq())

View file

@ -12,37 +12,6 @@ case class ProofTree(premises: Seq[ProofTree] = Seq(), line: Option[String] = No
if this.conclusion.isEmpty then copy(conclusion = Some(conclusion)) if this.conclusion.isEmpty then copy(conclusion = Some(conclusion))
else ProofTree().addPremise(this).addConclusion(conclusion) else ProofTree().addPremise(this).addConclusion(conclusion)
private def formatLine(start: Int, end: Int, rule: String): Line =
val lineStr = "-" * (end - start)
val lineText = if rule.isEmpty then lineStr else s"$lineStr $rule"
Line(lineText, start)
def formatted: FormattedProofTree =
val fPremises = premises.map(_.formatted).reduceOption(_.joinHorizontally(_)).getOrElse(FormattedProofTree.empty)
val lConclusion = conclusion match
case Some(conclusion) => Line(conclusion)
case None => return line match
case Some(rule) => fPremises.extend(formatLine(fPremises.conclusionStart, fPremises.conclusionEnd, rule))
case None => fPremises
val aboveMiddle = (fPremises.conclusionStart + fPremises.conclusionEnd) / 2
val belowMiddle = (lConclusion.start + lConclusion.end) / 2
val (aboveCentered, belowCentered) =
if aboveMiddle < belowMiddle then (fPremises.shift(belowMiddle - aboveMiddle), lConclusion)
else if aboveMiddle > belowMiddle then (fPremises, lConclusion.shift(aboveMiddle - belowMiddle))
else (fPremises, lConclusion)
val combined = line match
case Some(rule) =>
val lineStart = aboveCentered.conclusionStart min belowCentered.start
val lineEnd = aboveCentered.conclusionEnd max belowCentered.end
aboveCentered.extend(formatLine(lineStart, lineEnd, rule)).extend(belowCentered)
case None => aboveCentered.extend(belowCentered)
combined.copy(conclusionStart = belowCentered.start, conclusionEnd = belowCentered.end)
def containsNoLines: Boolean = line.isEmpty && premises.forall(_.containsNoLines) def containsNoLines: Boolean = line.isEmpty && premises.forall(_.containsNoLines)
object ProofTree: object ProofTree:

View file

@ -0,0 +1,39 @@
package de.plugh.asciiprooftree.tree
case class ProofTreeFormatter(lineOverhang: Int = 0):
private def formatLine(start: Int, end: Int, rule: String): Line =
val lineStart = start - lineOverhang
val lineEnd = end + lineOverhang
val lineStr = "-" * (lineEnd - lineStart)
val lineText = if rule.isEmpty then lineStr else s"$lineStr $rule"
Line(lineText, lineStart)
def formatTree(tree: ProofTree): FormattedProofTree =
val fPremises = tree
.premises
.map(formatTree)
.reduceOption(_.joinHorizontally(_))
.getOrElse(FormattedProofTree.empty)
val lConclusion = tree.conclusion match
case Some(conclusion) => Line(conclusion)
case None => return tree.line match
case Some(rule) => fPremises.extend(formatLine(fPremises.conclusionStart, fPremises.conclusionEnd, rule))
case None => fPremises
val aboveMiddle = (fPremises.conclusionStart + fPremises.conclusionEnd) / 2
val belowMiddle = (lConclusion.start + lConclusion.end) / 2
val (aboveCentered, belowCentered) =
if aboveMiddle < belowMiddle then (fPremises.shift(belowMiddle - aboveMiddle), lConclusion)
else if aboveMiddle > belowMiddle then (fPremises, lConclusion.shift(aboveMiddle - belowMiddle))
else (fPremises, lConclusion)
val combined = tree.line match
case Some(rule) =>
val lineStart = aboveCentered.conclusionStart min belowCentered.start
val lineEnd = aboveCentered.conclusionEnd max belowCentered.end
aboveCentered.extend(formatLine(lineStart, lineEnd, rule)).extend(belowCentered)
case None => aboveCentered.extend(belowCentered)
combined.copy(conclusionStart = belowCentered.start, conclusionEnd = belowCentered.end)