--- a/src/Pure/Thy/latex.scala Fri Dec 08 23:43:58 2017 +0100
+++ b/src/Pure/Thy/latex.scala Sun Dec 10 14:29:14 2017 +0100
@@ -7,25 +7,108 @@
package isabelle
+import java.io.{File => JFile}
+
import scala.annotation.tailrec
object Latex
{
- sealed case class Error(file: Option[Path], line: Int, message: String)
+ /** latex errors **/
+
+ /* generated .tex file */
+
+ private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
+ private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r
+ private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
+
+ def read_tex_file(tex_file: Path): Tex_File =
+ new Tex_File(tex_file, split_lines(File.read(tex_file)).toArray)
+
+ final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
+ {
+ override def toString: String = tex_file.toString
+
+ val source_file: Option[Path] =
+ if (tex_lines.length > 0) {
+ tex_lines(0) match {
+ case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file =>
+ Some(Path.explode(file))
+ case _ => None
+ }
+ }
+ else None
+
+ val source_content: Line.Document =
+ source_file match {
+ case Some(file) => Line.Document(Symbol.decode(File.read(file)))
+ case None => Line.Document.empty
+ }
+
+ lazy val source_chunk: Symbol.Text_Chunk =
+ Symbol.Text_Chunk(source_content.text)
- def filter_errors(dir: Path, text: String): List[Error] =
+ def source_position(l: Int): Option[Position.T] =
+ for {
+ file <- source_file
+ if 0 < l && l <= tex_lines.length
+ line = tex_lines(l - 1)
+ if line.endsWith("%:%")
+ symbol_range <-
+ (line match {
+ case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
+ case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1))
+ case _ => None
+ })
+ range <- source_chunk.incorporate(symbol_range)
+ }
+ yield {
+ Position.Line_File(source_content.position(range.start).line1, file.implode) :::
+ Position.Range(symbol_range)
+ }
+
+ def tex_position(line: Int): Position.T =
+ Position.File(tex_file.implode) ::: Position.Line(line)
+
+ def position(line: Int): Position.T =
+ source_position(line) getOrElse tex_position(line)
+ }
+
+
+ /* latex log */
+
+ def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
{
+ val seen_files = Synchronized(Map.empty[JFile, Tex_File])
+
+ def check_tex_file(path: Path): Option[Tex_File] =
+ seen_files.change_result(seen =>
+ seen.get(path.file) match {
+ case None =>
+ if (path.is_file) {
+ val tex_file = read_tex_file(path)
+ (Some(tex_file), seen + (path.file -> tex_file))
+ }
+ else (None, seen)
+ case some => (some, seen)
+ })
+
+ def tex_file_position(path: Path, line: Int): Position.T =
+ check_tex_file(path) match {
+ case Some(tex_file) => tex_file.position(line)
+ case None => Position.Line_File(line, path.implode)
+ }
+
object File_Line_Error
{
val Pattern = """^(.*):(\d+): (.*)$""".r
- def unapply(line: String): Option[Error] =
+ def unapply(line: String): Option[(Path, Int, String)] =
line match {
case Pattern(file, Value.Int(line), message) =>
val path = File.standard_path(file)
if (Path.is_wellformed(path)) {
- val file = Path.explode(path)
- if ((dir + file).is_file) Some(Error(Some(file), line, message)) else None
+ val file = dir + Path.explode(path)
+ if (file.is_file) Some((file, line, message)) else None
}
else None
case _ => None
@@ -35,26 +118,75 @@
object Line_Error
{
val Pattern = """^l\.(\d+) (.*)$""".r
- def unapply(line: String): Option[Error] =
+ def unapply(line: String): Option[(Int, String)] =
line match {
- case Pattern(Value.Int(line), message) => Some(Error(None, line, message))
+ case Pattern(Value.Int(line), message) => Some((line, message))
case _ => None
}
}
- @tailrec def filter(lines: List[String], result: List[Error]): List[Error] =
+ @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
+ : List[(String, Position.T)] =
+ {
lines match {
- case File_Line_Error(err1) :: rest1 =>
+ case File_Line_Error((file, line, msg1)) :: rest1 =>
+ val pos = tex_file_position(file, line)
rest1 match {
- case Line_Error(err2) :: rest2 if err1.line == err2.line =>
- val err = err1.copy(message = Exn.cat_message(err1.message, err2.message))
- filter(rest2, err :: result)
- case _ => filter(rest1, err1 :: result)
+ case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
+ filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
+ case _ =>
+ filter(rest1, (msg1, pos) :: result)
}
case _ :: rest => filter(rest, result)
case Nil => result.reverse
}
+ }
- filter(split_lines(text), Nil)
+ filter(split_lines(root_log), Nil)
+ }
+
+
+ /* errors */
+
+ val default_root_name: String = "root"
+
+ def latex_errors(dir: Path = Path.current, root_name: String = default_root_name)
+ {
+ val root_log_path = dir + Path.explode(root_name).ext("log")
+ val errors =
+ if (root_log_path.is_file) {
+ for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
+ yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _))
+ }
+ else Nil
+ if (errors.nonEmpty) Output.writeln(cat_lines(errors))
}
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("latex_errors", "print latex errors for Isabelle document output", args =>
+ {
+ var dir = Path.current
+ var root_name = default_root_name
+
+ val getopts = Getopts("""
+Usage: isabelle latex_errors
+
+ Options are:
+ -d DIR alternative document directory (default: current)
+ -n NAME alternative root name (default: """ + quote(default_root_name) + """)
+
+ Print latex errors for Isabelle document output directory (with root.tex,
+ root.log etc.).
+""",
+ "d:" -> (arg => dir = Path.explode(arg)),
+ "n:" -> (arg => root_name = arg))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ latex_errors(dir = dir, root_name = root_name)
+ })
}