author | wenzelm |
Sun, 10 Dec 2017 20:50:09 +0100 | |
changeset 67180 | dcac4659d482 |
parent 67177 | af5b89bc065c |
child 67187 | 3457d7d43ee9 |
permissions | -rw-r--r-- |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/present.scala |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
3 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
4 |
Theory presentation: HTML. |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
6 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
8 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
9 |
|
61372 | 10 |
import java.io.{File => JFile} |
11 |
||
51402 | 12 |
import scala.collection.immutable.SortedMap |
13 |
||
14 |
||
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
15 |
object Present |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
16 |
{ |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
17 |
/* maintain chapter index -- NOT thread-safe */ |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
18 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
19 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
20 |
|
51402 | 21 |
private def read_sessions(dir: Path): List[(String, String)] = |
22 |
{ |
|
51416 | 23 |
val path = dir + sessions_path |
24 |
if (path.is_file) { |
|
25 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset
|
26 |
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) |
51416 | 27 |
} |
28 |
else Nil |
|
51402 | 29 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
30 |
|
51402 | 31 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
32 |
{ |
|
33 |
import XML.Encode._ |
|
34 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
35 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
36 |
|
61372 | 37 |
def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
38 |
{ |
61372 | 39 |
val dir = browser_info + Path.basic(chapter) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
40 |
Isabelle_System.mkdirs(dir) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
41 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
42 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
43 |
try { read_sessions(dir) } |
51987 | 44 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
45 |
|
51402 | 46 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
65988 | 47 |
write_sessions(dir, sessions) |
51402 | 48 |
|
65988 | 49 |
val title = "Isabelle/" + chapter + " sessions" |
50 |
HTML.write_document(dir, "index.html", |
|
51 |
List(HTML.title(title + " (" + Distribution.version + ")")), |
|
52 |
HTML.chapter(title) :: |
|
53 |
(if (sessions.isEmpty) Nil |
|
54 |
else |
|
65992 | 55 |
List(HTML.div("sessions", |
56 |
List(HTML.description( |
|
65988 | 57 |
sessions.map({ case (name, description) => |
65989 | 58 |
(List(HTML.link(name + "/index.html", HTML.text(name))), |
59 |
if (description == "") Nil |
|
66038 | 60 |
else HTML.break ::: List(HTML.pre(HTML.text(description)))) }))))))) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
61 |
} |
61372 | 62 |
|
63 |
def make_global_index(browser_info: Path) |
|
64 |
{ |
|
65 |
if (!(browser_info + Path.explode("index.html")).is_file) { |
|
66 |
Isabelle_System.mkdirs(browser_info) |
|
67 |
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
|
68 |
browser_info + Path.explode("isabelle.gif")) |
|
69 |
File.write(browser_info + Path.explode("index.html"), |
|
70 |
File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
|
71 |
File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
|
72 |
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
|
73 |
} |
|
74 |
} |
|
75 |
||
76 |
||
77 |
/* finish session */ |
|
78 |
||
79 |
def finish( |
|
80 |
progress: Progress, |
|
81 |
browser_info: Path, |
|
82 |
graph_file: JFile, |
|
62631 | 83 |
info: Sessions.Info, |
61372 | 84 |
name: String) |
85 |
{ |
|
86 |
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) |
|
65089 | 87 |
val session_fonts = session_prefix + Path.explode("fonts") |
61372 | 88 |
|
89 |
if (info.options.bool("browser_info")) { |
|
65089 | 90 |
Isabelle_System.mkdirs(session_fonts) |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
91 |
|
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
92 |
val session_graph = session_prefix + Path.basic("session_graph.pdf") |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
93 |
File.copy(graph_file, session_graph.file) |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
94 |
Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph)) |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
95 |
|
66000 | 96 |
HTML.write_isabelle_css(session_prefix) |
61500 | 97 |
|
65083 | 98 |
for (font <- Isabelle_System.fonts(html = true)) |
65089 | 99 |
File.copy(font, session_fonts) |
61372 | 100 |
} |
101 |
} |
|
66040 | 102 |
|
103 |
||
104 |
/* theory document */ |
|
105 |
||
106 |
private val document_span_elements = |
|
66075 | 107 |
Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT |
66040 | 108 |
|
66075 | 109 |
private def make_html(xml: XML.Body): XML.Body = |
66040 | 110 |
xml map { |
111 |
case XML.Wrapped_Elem(markup, body1, body2) => |
|
112 |
XML.Wrapped_Elem(markup, make_html(body1), make_html(body2)) |
|
113 |
case XML.Elem(markup, body) => |
|
66044 | 114 |
val name = markup.name |
115 |
val html = |
|
116 |
markup.properties match { |
|
117 |
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => |
|
118 |
List(HTML.span(kind, make_html(body))) |
|
119 |
case _ => |
|
120 |
make_html(body) |
|
121 |
} |
|
66075 | 122 |
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { |
123 |
case Some(c) => HTML.span(c.toString, html) |
|
124 |
case None => HTML.span(name, html) |
|
66044 | 125 |
} |
66040 | 126 |
case XML.Text(text) => |
127 |
XML.Text(Symbol.decode(text)) |
|
128 |
} |
|
129 |
||
130 |
def theory_document(snapshot: Document.Snapshot): XML.Body = |
|
131 |
{ |
|
66043 | 132 |
make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements)) |
66040 | 133 |
} |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
134 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
135 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
136 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
137 |
/** build document **/ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
138 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
139 |
val default_document_name = "document" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
140 |
val default_document_format = "pdf" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
141 |
val document_formats = List("pdf", "dvi") |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
142 |
def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
143 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
144 |
def document_tags(tags: List[String]): String = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
145 |
{ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
146 |
cat_lines( |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
147 |
tags.map(tag => |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
148 |
tag.toList match { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
149 |
case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
150 |
case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
151 |
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
152 |
case cs => "\\isafoldtag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
153 |
})) + "\n" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
154 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
155 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
156 |
def build_document( |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
157 |
document_name: String = default_document_name, |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
158 |
document_format: String = default_document_format, |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
159 |
document_dir: Option[Path] = None, |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
160 |
tags: List[String] = Nil) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
161 |
{ |
67177 | 162 |
val document_target = Path.parent + Path.explode(document_name).ext(document_format) |
163 |
||
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
164 |
if (!document_formats.contains(document_format)) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
165 |
error("Bad document output format: " + quote(document_format)) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
166 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
167 |
val dir = document_dir getOrElse default_document_dir(document_name) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
168 |
if (!dir.is_dir) error("Bad document output directory " + dir) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
169 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
170 |
val root_name = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
171 |
{ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
172 |
val root1 = "root_" + document_name |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
173 |
if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
174 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
175 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
176 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
177 |
/* bash scripts */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
178 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
179 |
def root_bash(ext: String): String = Bash.string(root_name + "." + ext) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
180 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
181 |
def latex_bash(fmt: String, ext: String = "tex"): String = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
182 |
"isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
183 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
184 |
def bash(script: String): Process_Result = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
185 |
Isabelle_System.bash(script, cwd = dir.file) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
186 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
187 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
188 |
/* prepare document */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
189 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
190 |
File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags)) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
191 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
192 |
val result = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
193 |
if ((dir + Path.explode("build")).is_file) { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
194 |
bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name)) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
195 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
196 |
else { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
197 |
bash( |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
198 |
List( |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
199 |
latex_bash("sty"), |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
200 |
latex_bash(document_format), |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
201 |
"{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
202 |
"{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
203 |
latex_bash(document_format), |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
204 |
latex_bash(document_format)).mkString(" && ")) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
205 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
206 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
207 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
208 |
/* result */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
209 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
210 |
if (!result.ok) { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
211 |
cat_error(cat_lines(Latex.latex_errors(dir, root_name)), |
67180 | 212 |
"Failed to build document in directory " + File.path(dir.absolute_file)) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
213 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
214 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
215 |
bash("[ -f " + root_bash(document_format) + " ] && cp -f " + |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
216 |
root_bash(document_format) + " " + File.bash_path(document_target)).check |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
217 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
218 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
219 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
220 |
/* Isabelle tool wrapper */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
221 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
222 |
val isabelle_tool = |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
223 |
Isabelle_Tool("document", "prepare theory session document", args => |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
224 |
{ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
225 |
var document_dir: Option[Path] = None |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
226 |
var document_name = default_document_name |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
227 |
var document_format = default_document_format |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
228 |
var tags: List[String] = Nil |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
229 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
230 |
val getopts = Getopts(""" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
231 |
Usage: isabelle document [OPTIONS] |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
232 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
233 |
Options are: |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
234 |
-d DIR document output directory (default """ + |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
235 |
default_document_dir(default_document_name) + """) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
236 |
-n NAME document name (default """ + quote(default_document_name) + """) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
237 |
-o FORMAT document format: """ + |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
238 |
commas(document_formats.map(fmt => |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
239 |
fmt + (if (fmt == default_document_format) " (default)" else ""))) + """ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
240 |
-t TAGS markup for tagged regions |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
241 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
242 |
Prepare the theory session document in document directory, producing the |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
243 |
specified output format. |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
244 |
""", |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
245 |
"d:" -> (arg => document_dir = Some(Path.explode(arg))), |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
246 |
"n:" -> (arg => document_name = arg), |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
247 |
"o:" -> (arg => document_format = arg), |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
248 |
"t:" -> (arg => tags = space_explode(',', arg))) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
249 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
250 |
val more_args = getopts(args) |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
251 |
if (more_args.nonEmpty) getopts.usage() |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
252 |
|
67180 | 253 |
try { |
254 |
build_document(document_dir = document_dir, document_name = document_name, |
|
255 |
document_format = document_format, tags = tags) |
|
256 |
} |
|
257 |
catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) } |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
258 |
}) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
259 |
} |