author | wenzelm |
Sun, 10 Dec 2017 18:31:41 +0100 | |
changeset 67176 | 13b5c3ff1954 |
parent 67174 | 258e1394e76a |
child 67182 | bdc03e20fce3 |
permissions | -rw-r--r-- |
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 |
||
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
19 |
def latex_errors(dir: Path, root_name: String): List[String] = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
20 |
{ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
21 |
val root_log_path = dir + Path.explode(root_name).ext("log") |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
22 |
if (root_log_path.is_file) { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
23 |
for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) } |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
24 |
yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _)) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
25 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
26 |
else Nil |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
27 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
28 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67174
diff
changeset
|
29 |
|
67173 | 30 |
/* generated .tex file */ |
31 |
||
32 |
private val File_Pattern = """^.*%:%file=(.+)%:%$""".r |
|
33 |
private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r |
|
34 |
private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r |
|
35 |
||
36 |
def read_tex_file(tex_file: Path): Tex_File = |
|
67174 | 37 |
new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray) |
67173 | 38 |
|
39 |
final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String]) |
|
40 |
{ |
|
41 |
override def toString: String = tex_file.toString |
|
42 |
||
43 |
val source_file: Option[Path] = |
|
44 |
if (tex_lines.length > 0) { |
|
45 |
tex_lines(0) match { |
|
46 |
case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file => |
|
47 |
Some(Path.explode(file)) |
|
48 |
case _ => None |
|
49 |
} |
|
50 |
} |
|
51 |
else None |
|
52 |
||
53 |
val source_content: Line.Document = |
|
54 |
source_file match { |
|
55 |
case Some(file) => Line.Document(Symbol.decode(File.read(file))) |
|
56 |
case None => Line.Document.empty |
|
57 |
} |
|
58 |
||
59 |
lazy val source_chunk: Symbol.Text_Chunk = |
|
60 |
Symbol.Text_Chunk(source_content.text) |
|
67172 | 61 |
|
67173 | 62 |
def source_position(l: Int): Option[Position.T] = |
63 |
for { |
|
64 |
file <- source_file |
|
65 |
if 0 < l && l <= tex_lines.length |
|
66 |
line = tex_lines(l - 1) |
|
67 |
if line.endsWith("%:%") |
|
68 |
symbol_range <- |
|
69 |
(line match { |
|
70 |
case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j)) |
|
71 |
case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1)) |
|
72 |
case _ => None |
|
73 |
}) |
|
74 |
range <- source_chunk.incorporate(symbol_range) |
|
75 |
} |
|
76 |
yield { |
|
77 |
Position.Line_File(source_content.position(range.start).line1, file.implode) ::: |
|
78 |
Position.Range(symbol_range) |
|
79 |
} |
|
80 |
||
81 |
def tex_position(line: Int): Position.T = |
|
82 |
Position.File(tex_file.implode) ::: Position.Line(line) |
|
83 |
||
84 |
def position(line: Int): Position.T = |
|
85 |
source_position(line) getOrElse tex_position(line) |
|
86 |
} |
|
87 |
||
88 |
||
89 |
/* latex log */ |
|
90 |
||
91 |
def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = |
|
67172 | 92 |
{ |
67173 | 93 |
val seen_files = Synchronized(Map.empty[JFile, Tex_File]) |
94 |
||
95 |
def check_tex_file(path: Path): Option[Tex_File] = |
|
96 |
seen_files.change_result(seen => |
|
97 |
seen.get(path.file) match { |
|
98 |
case None => |
|
99 |
if (path.is_file) { |
|
100 |
val tex_file = read_tex_file(path) |
|
101 |
(Some(tex_file), seen + (path.file -> tex_file)) |
|
102 |
} |
|
103 |
else (None, seen) |
|
104 |
case some => (some, seen) |
|
105 |
}) |
|
106 |
||
107 |
def tex_file_position(path: Path, line: Int): Position.T = |
|
108 |
check_tex_file(path) match { |
|
109 |
case Some(tex_file) => tex_file.position(line) |
|
110 |
case None => Position.Line_File(line, path.implode) |
|
111 |
} |
|
112 |
||
67172 | 113 |
object File_Line_Error |
114 |
{ |
|
115 |
val Pattern = """^(.*):(\d+): (.*)$""".r |
|
67173 | 116 |
def unapply(line: String): Option[(Path, Int, String)] = |
67172 | 117 |
line match { |
118 |
case Pattern(file, Value.Int(line), message) => |
|
119 |
val path = File.standard_path(file) |
|
120 |
if (Path.is_wellformed(path)) { |
|
67173 | 121 |
val file = dir + Path.explode(path) |
122 |
if (file.is_file) Some((file, line, message)) else None |
|
67172 | 123 |
} |
124 |
else None |
|
125 |
case _ => None |
|
126 |
} |
|
127 |
} |
|
128 |
||
129 |
object Line_Error |
|
130 |
{ |
|
131 |
val Pattern = """^l\.(\d+) (.*)$""".r |
|
67173 | 132 |
def unapply(line: String): Option[(Int, String)] = |
67172 | 133 |
line match { |
67173 | 134 |
case Pattern(Value.Int(line), message) => Some((line, message)) |
67172 | 135 |
case _ => None |
136 |
} |
|
137 |
} |
|
138 |
||
67173 | 139 |
@tailrec def filter(lines: List[String], result: List[(String, Position.T)]) |
140 |
: List[(String, Position.T)] = |
|
141 |
{ |
|
67172 | 142 |
lines match { |
67173 | 143 |
case File_Line_Error((file, line, msg1)) :: rest1 => |
144 |
val pos = tex_file_position(file, line) |
|
67172 | 145 |
rest1 match { |
67173 | 146 |
case Line_Error((line2, msg2)) :: rest2 if line == line2 => |
147 |
filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) |
|
148 |
case _ => |
|
149 |
filter(rest1, (msg1, pos) :: result) |
|
67172 | 150 |
} |
151 |
case _ :: rest => filter(rest, result) |
|
152 |
case Nil => result.reverse |
|
153 |
} |
|
67173 | 154 |
} |
67172 | 155 |
|
67174 | 156 |
filter(Line.logical_lines(root_log), Nil) |
67173 | 157 |
} |
67172 | 158 |
} |