67172
|
1 |
/* Title: Pure/Thy/latex.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for LaTeX.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
67173
|
10 |
import java.io.{File => JFile}
|
|
11 |
|
67172
|
12 |
import scala.annotation.tailrec
|
|
13 |
|
|
14 |
|
|
15 |
object Latex
|
|
16 |
{
|
67173
|
17 |
/** latex errors **/
|
|
18 |
|
|
19 |
/* generated .tex file */
|
|
20 |
|
|
21 |
private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
|
|
22 |
private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r
|
|
23 |
private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
|
|
24 |
|
|
25 |
def read_tex_file(tex_file: Path): Tex_File =
|
|
26 |
new Tex_File(tex_file, split_lines(File.read(tex_file)).toArray)
|
|
27 |
|
|
28 |
final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
|
|
29 |
{
|
|
30 |
override def toString: String = tex_file.toString
|
|
31 |
|
|
32 |
val source_file: Option[Path] =
|
|
33 |
if (tex_lines.length > 0) {
|
|
34 |
tex_lines(0) match {
|
|
35 |
case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file =>
|
|
36 |
Some(Path.explode(file))
|
|
37 |
case _ => None
|
|
38 |
}
|
|
39 |
}
|
|
40 |
else None
|
|
41 |
|
|
42 |
val source_content: Line.Document =
|
|
43 |
source_file match {
|
|
44 |
case Some(file) => Line.Document(Symbol.decode(File.read(file)))
|
|
45 |
case None => Line.Document.empty
|
|
46 |
}
|
|
47 |
|
|
48 |
lazy val source_chunk: Symbol.Text_Chunk =
|
|
49 |
Symbol.Text_Chunk(source_content.text)
|
67172
|
50 |
|
67173
|
51 |
def source_position(l: Int): Option[Position.T] =
|
|
52 |
for {
|
|
53 |
file <- source_file
|
|
54 |
if 0 < l && l <= tex_lines.length
|
|
55 |
line = tex_lines(l - 1)
|
|
56 |
if line.endsWith("%:%")
|
|
57 |
symbol_range <-
|
|
58 |
(line match {
|
|
59 |
case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
|
|
60 |
case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1))
|
|
61 |
case _ => None
|
|
62 |
})
|
|
63 |
range <- source_chunk.incorporate(symbol_range)
|
|
64 |
}
|
|
65 |
yield {
|
|
66 |
Position.Line_File(source_content.position(range.start).line1, file.implode) :::
|
|
67 |
Position.Range(symbol_range)
|
|
68 |
}
|
|
69 |
|
|
70 |
def tex_position(line: Int): Position.T =
|
|
71 |
Position.File(tex_file.implode) ::: Position.Line(line)
|
|
72 |
|
|
73 |
def position(line: Int): Position.T =
|
|
74 |
source_position(line) getOrElse tex_position(line)
|
|
75 |
}
|
|
76 |
|
|
77 |
|
|
78 |
/* latex log */
|
|
79 |
|
|
80 |
def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
|
67172
|
81 |
{
|
67173
|
82 |
val seen_files = Synchronized(Map.empty[JFile, Tex_File])
|
|
83 |
|
|
84 |
def check_tex_file(path: Path): Option[Tex_File] =
|
|
85 |
seen_files.change_result(seen =>
|
|
86 |
seen.get(path.file) match {
|
|
87 |
case None =>
|
|
88 |
if (path.is_file) {
|
|
89 |
val tex_file = read_tex_file(path)
|
|
90 |
(Some(tex_file), seen + (path.file -> tex_file))
|
|
91 |
}
|
|
92 |
else (None, seen)
|
|
93 |
case some => (some, seen)
|
|
94 |
})
|
|
95 |
|
|
96 |
def tex_file_position(path: Path, line: Int): Position.T =
|
|
97 |
check_tex_file(path) match {
|
|
98 |
case Some(tex_file) => tex_file.position(line)
|
|
99 |
case None => Position.Line_File(line, path.implode)
|
|
100 |
}
|
|
101 |
|
67172
|
102 |
object File_Line_Error
|
|
103 |
{
|
|
104 |
val Pattern = """^(.*):(\d+): (.*)$""".r
|
67173
|
105 |
def unapply(line: String): Option[(Path, Int, String)] =
|
67172
|
106 |
line match {
|
|
107 |
case Pattern(file, Value.Int(line), message) =>
|
|
108 |
val path = File.standard_path(file)
|
|
109 |
if (Path.is_wellformed(path)) {
|
67173
|
110 |
val file = dir + Path.explode(path)
|
|
111 |
if (file.is_file) Some((file, line, message)) else None
|
67172
|
112 |
}
|
|
113 |
else None
|
|
114 |
case _ => None
|
|
115 |
}
|
|
116 |
}
|
|
117 |
|
|
118 |
object Line_Error
|
|
119 |
{
|
|
120 |
val Pattern = """^l\.(\d+) (.*)$""".r
|
67173
|
121 |
def unapply(line: String): Option[(Int, String)] =
|
67172
|
122 |
line match {
|
67173
|
123 |
case Pattern(Value.Int(line), message) => Some((line, message))
|
67172
|
124 |
case _ => None
|
|
125 |
}
|
|
126 |
}
|
|
127 |
|
67173
|
128 |
@tailrec def filter(lines: List[String], result: List[(String, Position.T)])
|
|
129 |
: List[(String, Position.T)] =
|
|
130 |
{
|
67172
|
131 |
lines match {
|
67173
|
132 |
case File_Line_Error((file, line, msg1)) :: rest1 =>
|
|
133 |
val pos = tex_file_position(file, line)
|
67172
|
134 |
rest1 match {
|
67173
|
135 |
case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
|
|
136 |
filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
|
|
137 |
case _ =>
|
|
138 |
filter(rest1, (msg1, pos) :: result)
|
67172
|
139 |
}
|
|
140 |
case _ :: rest => filter(rest, result)
|
|
141 |
case Nil => result.reverse
|
|
142 |
}
|
67173
|
143 |
}
|
67172
|
144 |
|
67173
|
145 |
filter(split_lines(root_log), Nil)
|
|
146 |
}
|
|
147 |
|
|
148 |
|
|
149 |
/* errors */
|
|
150 |
|
|
151 |
val default_root_name: String = "root"
|
|
152 |
|
|
153 |
def latex_errors(dir: Path = Path.current, root_name: String = default_root_name)
|
|
154 |
{
|
|
155 |
val root_log_path = dir + Path.explode(root_name).ext("log")
|
|
156 |
val errors =
|
|
157 |
if (root_log_path.is_file) {
|
|
158 |
for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
|
|
159 |
yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _))
|
|
160 |
}
|
|
161 |
else Nil
|
|
162 |
if (errors.nonEmpty) Output.writeln(cat_lines(errors))
|
67172
|
163 |
}
|
67173
|
164 |
|
|
165 |
|
|
166 |
/* Isabelle tool wrapper */
|
|
167 |
|
|
168 |
val isabelle_tool =
|
|
169 |
Isabelle_Tool("latex_errors", "print latex errors for Isabelle document output", args =>
|
|
170 |
{
|
|
171 |
var dir = Path.current
|
|
172 |
var root_name = default_root_name
|
|
173 |
|
|
174 |
val getopts = Getopts("""
|
|
175 |
Usage: isabelle latex_errors
|
|
176 |
|
|
177 |
Options are:
|
|
178 |
-d DIR alternative document directory (default: current)
|
|
179 |
-n NAME alternative root name (default: """ + quote(default_root_name) + """)
|
|
180 |
|
|
181 |
Print latex errors for Isabelle document output directory (with root.tex,
|
|
182 |
root.log etc.).
|
|
183 |
""",
|
|
184 |
"d:" -> (arg => dir = Path.explode(arg)),
|
|
185 |
"n:" -> (arg => root_name = arg))
|
|
186 |
|
|
187 |
val more_args = getopts(args)
|
|
188 |
if (more_args.nonEmpty) getopts.usage()
|
|
189 |
|
|
190 |
latex_errors(dir = dir, root_name = root_name)
|
|
191 |
})
|
67172
|
192 |
}
|