1/*  Title:      Pure/Thy/latex.scala
2    Author:     Makarius
3
4Support for LaTeX.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12import scala.annotation.tailrec
13
14
15object Latex
16{
17  /** latex errors **/
18
19  def latex_errors(dir: Path, root_name: String): List[String] =
20  {
21    val root_log_path = dir + Path.explode(root_name).ext("log")
22    if (root_log_path.is_file) {
23      for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
24      yield "Latex error" + Position.here(pos) + ":\n" + Library.prefix_lines("  ", msg)
25    }
26    else Nil
27  }
28
29
30  /* generated .tex file */
31
32  private val File_Pattern = """^%:%file=(.+)%:%$""".r
33  private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
34
35  def read_tex_file(tex_file: Path): Tex_File =
36  {
37    val positions =
38      Line.logical_lines(File.read(tex_file)).reverse.
39        takeWhile(_ != "\\endinput").reverse
40
41    val source_file =
42      positions match {
43        case File_Pattern(file) :: _ => Some(file)
44        case _ => None
45      }
46
47    val source_lines =
48      if (source_file.isEmpty) Nil
49      else
50        positions.flatMap(line =>
51          line match {
52            case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
53            case _ => None
54          })
55
56    new Tex_File(tex_file, source_file, source_lines)
57  }
58
59  final class Tex_File private[Latex](
60    tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)])
61  {
62    override def toString: String = tex_file.toString
63
64    def source_position(l: Int): Option[Position.T] =
65      source_file match {
66        case None => None
67        case Some(file) =>
68          val source_line =
69            (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
70              { case (_, (_, n)) => n })
71          if (source_line == 0) None else Some(Position.Line_File(source_line, file))
72      }
73
74    def position(line: Int): Position.T =
75      source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
76  }
77
78
79  /* latex log */
80
81  def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
82  {
83    val seen_files = Synchronized(Map.empty[JFile, Tex_File])
84
85    def check_tex_file(path: Path): Option[Tex_File] =
86      seen_files.change_result(seen =>
87        seen.get(path.file) match {
88          case None =>
89            if (path.is_file) {
90              val tex_file = read_tex_file(path)
91              (Some(tex_file), seen + (path.file -> tex_file))
92            }
93            else (None, seen)
94          case some => (some, seen)
95        })
96
97    def tex_file_position(path: Path, line: Int): Position.T =
98      check_tex_file(path) match {
99        case Some(tex_file) => tex_file.position(line)
100        case None => Position.Line_File(line, path.implode)
101      }
102
103    object File_Line_Error
104    {
105      val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
106      def unapply(line: String): Option[(Path, Int, String)] =
107        line match {
108          case Pattern(file, Value.Int(line), message) =>
109            val path = File.standard_path(file)
110            if (Path.is_wellformed(path)) {
111              val file = (dir + Path.explode(path)).canonical
112              val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
113              if (file.is_file) Some((file, line, msg)) else None
114            }
115            else None
116          case _ => None
117        }
118    }
119
120    val Line_Error = """^l\.\d+ (.*)$""".r
121    val More_Error =
122      List(
123        "<argument>",
124        "<template>",
125        "<recently read>",
126        "<to be read again>",
127        "<inserted text>",
128        "<output>",
129        "<everypar>",
130        "<everymath>",
131        "<everydisplay>",
132        "<everyhbox>",
133        "<everyvbox>",
134        "<everyjob>",
135        "<everycr>",
136        "<mark>",
137        "<everyeof>",
138        "<write>").mkString("^(?:", "|", ") (.*)$").r
139
140    val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
141
142    val error_ignore =
143      Set(
144        "See the LaTeX manual or LaTeX Companion for explanation.",
145        "Type  H <return>  for immediate help.")
146
147    def error_suffix1(lines: List[String]): Option[String] =
148    {
149      val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true })
150      lines1.zipWithIndex.collectFirst({
151        case (Line_Error(msg), i) =>
152          cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
153    }
154    def error_suffix2(lines: List[String]): Option[String] =
155      lines match {
156        case More_Error(msg) :: _ => Some(msg)
157        case _ => None
158      }
159
160    @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
161      : List[(String, Position.T)] =
162    {
163      lines match {
164        case File_Line_Error((file, line, msg1)) :: rest1 =>
165          val pos = tex_file_position(file, line)
166          val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
167          filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
168        case Bad_File(msg) :: rest =>
169          filter(rest, (msg, Position.none) :: result)
170        case _ :: rest => filter(rest, result)
171        case Nil => result.reverse
172      }
173    }
174
175    filter(Line.logical_lines(root_log), Nil)
176  }
177}
178