Use regex to detect blocks
This commit is contained in:
parent
f429b3934e
commit
7f1c71a6e2
5 changed files with 65 additions and 41 deletions
|
|
@ -18,8 +18,8 @@ To reformat all proof trees in your project, run:
|
|||
java -jar asciiprooftree.jar path/to/your/src
|
||||
```
|
||||
|
||||
If you want to use a different marker string than `§`, you can use the `--marker` option:
|
||||
For available options, run:
|
||||
|
||||
```shell
|
||||
java -jar asciiprooftree.jar path/to/your/src --marker 't>'
|
||||
java -jar asciiprooftree.jar --help
|
||||
```
|
||||
|
|
|
|||
|
|
@ -5,24 +5,30 @@ import org.rogach.scallop.*
|
|||
|
||||
import java.nio.file.{Files, Path}
|
||||
import scala.jdk.StreamConverters.*
|
||||
import scala.util.matching.Regex
|
||||
|
||||
val blockRe = "(?m)^(?<block>(\\s*)§.*\\n(?:\\2§.*\\n)*)".r
|
||||
val lineRe = "^\\s*§(?<block>.*)$".r
|
||||
|
||||
class Conf(args: Seq[String]) extends ScallopConf(args):
|
||||
val path: ScallopOption[Path] = trailArg[Path]()
|
||||
val marker: ScallopOption[String] = opt[String](default = Some("§"))
|
||||
val blockRegex: ScallopOption[String] = opt[String](default = Some(blockRe.regex))
|
||||
val lineRegex: ScallopOption[String] = opt[String](default = Some(lineRe.regex))
|
||||
verify()
|
||||
|
||||
@main
|
||||
def main(args: String*): Unit =
|
||||
val conf = new Conf(args)
|
||||
reformat(conf.path(), conf.marker())
|
||||
val formatter = Formatter(blockRe = Regex(conf.blockRegex()), lineRe = Regex(conf.lineRegex()))
|
||||
reformat(conf.path(), formatter)
|
||||
|
||||
def reformat(path: Path, marker: String): Unit =
|
||||
def reformat(path: Path, formatter: Formatter): Unit =
|
||||
if Files.isDirectory(path) then
|
||||
val files = Files.list(path).toScala(Seq)
|
||||
for file <- files do reformat(file, marker)
|
||||
for file <- files do reformat(file, formatter)
|
||||
else if Files.isRegularFile(path) then
|
||||
val text = Files.readString(path)
|
||||
val newText = Formatter.reformat(text, marker = marker)
|
||||
val newText = formatter.reformat(text)
|
||||
if text != newText then
|
||||
println(path)
|
||||
Files.writeString(path, newText)
|
||||
|
|
|
|||
|
|
@ -7,7 +7,8 @@ case class Block(lines: Seq[(String, String)]):
|
|||
def content: Seq[String] = lines.map((_, content) => content)
|
||||
def toLines: Seq[String] = lines.map((prefix, content) => s"$prefix $content")
|
||||
|
||||
def extend(prefix: String, content: String): Block = Block(lines :+ (prefix, content))
|
||||
def extend(block: Block): Block = Block(lines ++ block.lines)
|
||||
def extend(prefix: String, content: String): Block = extend(Block(prefix, content))
|
||||
|
||||
def resize(height: Int): Block =
|
||||
require(height > 0)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,5 @@
|
|||
package de.plugh.asciiprooftree.file
|
||||
|
||||
import de.plugh.asciiprooftree.tree.ProofTree
|
||||
|
||||
case class BlockInfo(block: Block, tree: ProofTree, start: Int, end: Int, endsWithNewline: Boolean)
|
||||
|
|
@ -1,45 +1,57 @@
|
|||
package de.plugh.asciiprooftree.file
|
||||
|
||||
import de.plugh.asciiprooftree.tree.{Line, Parser}
|
||||
import de.plugh.asciiprooftree.tree.Parser
|
||||
|
||||
import scala.collection.mutable
|
||||
import scala.util.boundary
|
||||
import scala.util.matching.Regex
|
||||
import scala.util.matching.Regex.Match
|
||||
|
||||
private class Formatter(marker: String):
|
||||
private val lines: mutable.Buffer[String] = mutable.Buffer()
|
||||
private var block: Option[Block] = None
|
||||
case class Formatter(blockRe: Regex, lineRe: Regex):
|
||||
private val blockReI = blockRe.pattern.namedGroups().get("block")
|
||||
private val lineReI = lineRe.pattern.namedGroups().get("block")
|
||||
|
||||
private def flushBlock(): Unit = for block <- this.block do
|
||||
val newBlock = Parser(block.content).parse match
|
||||
case Some(tree) => block.replace(tree.formatted.toString.linesIterator.toIndexedSeq)
|
||||
case None => block
|
||||
lines.appendAll(newBlock.toLines)
|
||||
this.block = None
|
||||
private def parseBlockLine(line: String): Option[Block] = boundary:
|
||||
val m = lineRe.findFirstMatchIn(line).getOrElse(boundary.break(None))
|
||||
require(m.end(lineReI) == line.length)
|
||||
val prefix = line.slice(0, m.start(lineReI))
|
||||
val content = line.slice(m.start(lineReI), line.length)
|
||||
Some(Block(prefix, content))
|
||||
|
||||
private def pushBlockLine(prefix: String, content: String): Unit = this.block match
|
||||
case Some(block) if Line(block.last._1).width == Line(prefix).width =>
|
||||
this.block = Some(block.extend(prefix, content))
|
||||
case _ =>
|
||||
flushBlock()
|
||||
this.block = Some(Block(prefix, content))
|
||||
private def parseBlockLines(lines: String): Option[Block] =
|
||||
val blocks = lines.linesIterator.map(parseBlockLine).toSeq
|
||||
if blocks.isEmpty || blocks.exists(_.isEmpty) then return None
|
||||
Some(blocks.flatten.reduce(_.extend(_)))
|
||||
|
||||
private def pushPlainLine(line: String): Unit =
|
||||
flushBlock()
|
||||
lines.append(line)
|
||||
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))
|
||||
Some(BlockInfo(
|
||||
block = block,
|
||||
tree = tree,
|
||||
start = m.start(blockReI),
|
||||
end = m.end(blockReI),
|
||||
endsWithNewline = text.endsWith("\n"),
|
||||
))
|
||||
|
||||
private def pushLine(line: String): Unit =
|
||||
val i = line.indexOf(marker)
|
||||
if i < 0 then pushPlainLine(line)
|
||||
else
|
||||
val prefix = line.slice(0, i + marker.length)
|
||||
val content = line.slice(i + marker.length, line.length)
|
||||
pushBlockLine(prefix, content)
|
||||
def findBlocks(text: String): Seq[BlockInfo] = blockRe.findAllMatchIn(text).flatMap(parseBlock(text, _)).toSeq
|
||||
|
||||
private def pushText(text: String): Unit = text.linesIterator.foreach(pushLine)
|
||||
def reformat(text: String): String =
|
||||
// Things just become nicer if we can assume that even the last line ends with a newline.
|
||||
val cleanText = if text.endsWith("\n") then text else text + "\n"
|
||||
|
||||
override def toString: String = lines.map(l => s"$l\n").mkString
|
||||
val result = StringBuilder()
|
||||
var resultEnd = 0
|
||||
|
||||
object Formatter:
|
||||
def reformat(text: String, marker: String = "§"): String =
|
||||
val fmt = new Formatter(marker)
|
||||
fmt.pushText(text)
|
||||
fmt.toString
|
||||
for info <- findBlocks(cleanText) do
|
||||
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
|
||||
result.append(block.toLines.mkString("\n"))
|
||||
if info.endsWithNewline then result.append("\n")
|
||||
resultEnd = info.end
|
||||
|
||||
// No need to update resultEnd since we don't need it from this point on
|
||||
if resultEnd < cleanText.length then result.append(cleanText.slice(resultEnd, cleanText.length))
|
||||
|
||||
// Remove final newline if the original text didn't have it
|
||||
if text.endsWith("\n") then result.toString() else result.toString().stripLineEnd
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue