author | wenzelm |
Thu, 12 Nov 2020 16:27:31 +0100 | |
changeset 72599 | 76550282267f |
parent 72595 | c806eeb9138c |
child 72600 | 2fa4f25d9d07 |
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 |
{ |
72376 | 39 |
val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter)) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
40 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
41 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
42 |
try { read_sessions(dir) } |
51987 | 43 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
44 |
|
51402 | 45 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
65988 | 46 |
write_sessions(dir, sessions) |
51402 | 47 |
|
65988 | 48 |
val title = "Isabelle/" + chapter + " sessions" |
49 |
HTML.write_document(dir, "index.html", |
|
50 |
List(HTML.title(title + " (" + Distribution.version + ")")), |
|
51 |
HTML.chapter(title) :: |
|
52 |
(if (sessions.isEmpty) Nil |
|
53 |
else |
|
65992 | 54 |
List(HTML.div("sessions", |
55 |
List(HTML.description( |
|
65988 | 56 |
sessions.map({ case (name, description) => |
69318 | 57 |
val descr = Symbol.trim_blank_lines(description) |
65989 | 58 |
(List(HTML.link(name + "/index.html", HTML.text(name))), |
69318 | 59 |
if (descr == "") Nil |
60 |
else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) |
|
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) { |
|
72375 | 66 |
Isabelle_System.make_directory(browser_info) |
61372 | 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 |
browser_info: Path, |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
81 |
graph_pdf: Bytes, |
62631 | 82 |
info: Sessions.Info, |
61372 | 83 |
name: String) |
84 |
{ |
|
85 |
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) |
|
65089 | 86 |
val session_fonts = session_prefix + Path.explode("fonts") |
61372 | 87 |
|
88 |
if (info.options.bool("browser_info")) { |
|
72375 | 89 |
Isabelle_System.make_directory(session_fonts) |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
90 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
91 |
Bytes.write(session_prefix + session_graph_path, graph_pdf) |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
92 |
|
66000 | 93 |
HTML.write_isabelle_css(session_prefix) |
61500 | 94 |
|
69374 | 95 |
for (entry <- Isabelle_Fonts.fonts(hidden = true)) |
69360 | 96 |
File.copy(entry.path, session_fonts) |
61372 | 97 |
} |
98 |
} |
|
66040 | 99 |
|
100 |
||
67253 | 101 |
/** preview **/ |
102 |
||
67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
103 |
sealed case class Preview(title: String, content: String) |
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
104 |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
105 |
def preview( |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
106 |
resources: Resources, |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
107 |
snapshot: Document.Snapshot, |
67262 | 108 |
plain_text: Boolean = false, |
67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
109 |
fonts_url: String => String = HTML.fonts_url()): Preview = |
67253 | 110 |
{ |
111 |
require(!snapshot.is_outdated) |
|
112 |
||
67264 | 113 |
def output_document(title: String, body: XML.Body): String = |
114 |
HTML.output_document( |
|
115 |
List( |
|
69362 | 116 |
HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), |
67264 | 117 |
HTML.title(title)), |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
118 |
List(HTML.source(body)), css = "", structural = false) |
67264 | 119 |
|
67253 | 120 |
val name = snapshot.node_name |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
121 |
|
67264 | 122 |
if (plain_text) { |
69366 | 123 |
val title = "File " + quote(name.path.file_name) |
67265
f32287c95432
store full blob source for the sake of markup_to_XML;
wenzelm
parents:
67264
diff
changeset
|
124 |
val content = output_document(title, HTML.text(snapshot.node.source)) |
67264 | 125 |
Preview(title, content) |
126 |
} |
|
67253 | 127 |
else { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
128 |
resources.make_preview(snapshot) match { |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
129 |
case Some(preview) => preview |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
130 |
case None => |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
131 |
val title = |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
132 |
if (name.is_theory) "Theory " + quote(name.theory_base_name) |
69366 | 133 |
else "File " + quote(name.path.file_name) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
134 |
val content = output_document(title, pide_document(snapshot)) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
135 |
Preview(title, content) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
136 |
} |
67253 | 137 |
} |
138 |
} |
|
139 |
||
140 |
||
67264 | 141 |
/* PIDE document */ |
66040 | 142 |
|
67336 | 143 |
private val document_elements = |
144 |
Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + |
|
145 |
Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE |
|
146 |
||
147 |
private val div_elements = |
|
148 |
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, |
|
149 |
HTML.descr.name) |
|
150 |
||
151 |
private def html_div(html: XML.Body): Boolean = |
|
152 |
html exists { |
|
153 |
case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) |
|
154 |
case XML.Text(_) => false |
|
155 |
} |
|
156 |
||
157 |
private def html_class(c: String, html: XML.Body): XML.Tree = |
|
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
158 |
if (html.forall(_ == HTML.no_text)) HTML.no_text |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
159 |
else if (html_div(html)) HTML.div(c, html) |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
160 |
else HTML.span(c, html) |
66040 | 161 |
|
66075 | 162 |
private def make_html(xml: XML.Body): XML.Body = |
66040 | 163 |
xml map { |
67336 | 164 |
case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => |
165 |
html_class(Markup.Language.DOCUMENT, make_html(body)) |
|
166 |
case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) |
|
167 |
case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) |
|
168 |
case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text |
|
169 |
case XML.Elem(Markup.Markdown_List(kind), body) => |
|
170 |
if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) |
|
66040 | 171 |
case XML.Elem(markup, body) => |
66044 | 172 |
val name = markup.name |
173 |
val html = |
|
174 |
markup.properties match { |
|
175 |
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => |
|
67336 | 176 |
List(html_class(kind, make_html(body))) |
66044 | 177 |
case _ => |
178 |
make_html(body) |
|
179 |
} |
|
66075 | 180 |
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { |
67336 | 181 |
case Some(c) => html_class(c.toString, html) |
182 |
case None => html_class(name, html) |
|
66044 | 183 |
} |
66040 | 184 |
case XML.Text(text) => |
185 |
XML.Text(Symbol.decode(text)) |
|
186 |
} |
|
187 |
||
67253 | 188 |
def pide_document(snapshot: Document.Snapshot): XML.Body = |
67336 | 189 |
make_html(snapshot.markup_to_XML(Text.Range.full, document_elements)) |
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset
|
190 |
|
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset
|
191 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
192 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
193 |
/** build documents **/ |
72565 | 194 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
195 |
val session_tex_path = Path.explode("session.tex") |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
196 |
val session_graph_path = Path.explode("session_graph.pdf") |
72565 | 197 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
198 |
def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
199 |
def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name) |
72309
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents:
71114
diff
changeset
|
200 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
201 |
def isabelletags(tags: List[String]): String = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
202 |
Library.terminate_lines( |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
203 |
tags.map(tag => |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
204 |
tag.toList match { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
205 |
case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
206 |
case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
207 |
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" |
67201 | 208 |
case cs => "\\isakeeptag{" + cs.mkString + "}" |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
209 |
})) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
210 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
211 |
def build_documents( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
212 |
session: String, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
213 |
deps: Sessions.Deps, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
214 |
store: Sessions.Store, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
215 |
progress: Progress = new Progress, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
216 |
verbose: Boolean = false, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
217 |
verbose_latex: Boolean = false): List[(String, Bytes)] = |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
218 |
{ |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
219 |
/* session info */ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
220 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
221 |
val info = deps.sessions_structure(session) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
222 |
val options = info.options |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
223 |
val base = deps(session) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
224 |
val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) |
67177 | 225 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
226 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
227 |
/* prepare document directory */ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
228 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
229 |
def prepare_dir(dir: Path, doc_name: String, doc_tags: List[String]): (Path, String) = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
230 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
231 |
val doc_dir = dir + Path.basic(doc_name) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
232 |
Isabelle_System.make_directory(doc_dir) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
233 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
234 |
Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
235 |
File.write(doc_dir + Path.explode("isabelletags.sty"), isabelletags(doc_tags)) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
236 |
for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
237 |
Bytes.write(doc_dir + session_graph_path, graph_pdf) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
238 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
239 |
File.write(doc_dir + session_tex_path, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
240 |
Library.terminate_lines( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
241 |
base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
242 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
243 |
using(store.open_database(session))(db => |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
244 |
for (name <- base.session_theories) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
245 |
val tex = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
246 |
Export.read_entry(db, session, name.theory, document_tex_name(name)) match { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
247 |
case Some(entry) => entry.uncompressed(cache = store.xz_cache) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
248 |
case None => Bytes.empty |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
249 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
250 |
Bytes.write(doc_dir + Path.basic(tex_name(name)), tex) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
251 |
}) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
252 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
253 |
val root1 = "root_" + doc_name |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
254 |
val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
255 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
256 |
(doc_dir, root) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
257 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
258 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
259 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
260 |
/* produce documents */ |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
261 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
262 |
val doc_output = info.document_output |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
263 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
264 |
val docs = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
265 |
for ((doc_name, doc_tags) <- info.documents) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
266 |
yield { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
267 |
Isabelle_System.with_tmp_dir("document")(tmp_dir => |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
268 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
269 |
val (doc_dir, root) = prepare_dir(tmp_dir, doc_name, doc_tags) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
270 |
doc_output.foreach(prepare_dir(_, doc_name, doc_tags)) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
271 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
272 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
273 |
// bash scripts |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
274 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
275 |
def root_bash(ext: String): String = Bash.string(root + "." + ext) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
276 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
277 |
def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
278 |
"isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
279 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
280 |
def bash(items: String*): Process_Result = |
72599 | 281 |
progress.bash(items.mkString(" && "), cwd = doc_dir.file, |
282 |
echo = verbose_latex, watchdog = Time.seconds(0.5)) |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
283 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
284 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
285 |
// prepare document |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
286 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
287 |
val result = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
288 |
if ((doc_dir + Path.explode("build")).is_file) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
289 |
bash("./build pdf " + Bash.string(doc_name)) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
290 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
291 |
else { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
292 |
bash( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
293 |
latex_bash(), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
294 |
"{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
295 |
"{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
296 |
latex_bash(), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
297 |
latex_bash()) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
298 |
} |
67204 | 299 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
300 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
301 |
// result |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
302 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
303 |
val root_pdf = Path.basic(root).pdf |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
304 |
val result_path = doc_dir + root_pdf |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
305 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
306 |
if (!result.ok) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
307 |
cat_error( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
308 |
Library.trim_line(result.err), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
309 |
cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
310 |
"Failed to build document " + quote(doc_name)) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
311 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
312 |
else if (!result_path.is_file) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
313 |
error("Bad document result: expected to find " + root_pdf) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
314 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
315 |
else doc_name -> Bytes.read(result_path) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
316 |
}) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
317 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
318 |
|
72595 | 319 |
def output(dir: Path) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
320 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
321 |
Isabelle_System.make_directory(dir) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
322 |
for ((name, pdf) <- docs) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
323 |
val path = dir + Path.basic(name).pdf |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
324 |
Bytes.write(path, pdf) |
72595 | 325 |
progress.echo_document(path) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
326 |
} |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
327 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
328 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
329 |
if (info.options.bool("browser_info") || doc_output.isEmpty) { |
72595 | 330 |
output(store.browser_info + Path.basic(info.chapter) + Path.basic(session)) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
331 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
332 |
|
72595 | 333 |
doc_output.foreach(output) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
334 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
335 |
docs |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
336 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
337 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
338 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
339 |
/* Isabelle tool wrapper */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
340 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
341 |
val isabelle_tool = |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
342 |
Isabelle_Tool("document", "prepare session theory document", args => |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
343 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
344 |
var verbose_latex = false |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
345 |
var dirs: List[Path] = Nil |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
346 |
var no_build = false |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
347 |
var options = Options.init() |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
348 |
var verbose_build = false |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
349 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
350 |
val getopts = Getopts( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
351 |
""" |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
352 |
Usage: isabelle document [OPTIONS] SESSION |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
353 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
354 |
Options are: |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
355 |
-O set option "document_output", relative to current directory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
356 |
-V verbose latex |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
357 |
-d DIR include session directory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
358 |
-n no build of session |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
359 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
360 |
-v verbose build |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
361 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
362 |
Prepare the theory document of a session. |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
363 |
""", |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
364 |
"O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
365 |
"V" -> (_ => verbose_latex = true), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
366 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
367 |
"n" -> (_ => no_build = true), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
368 |
"o:" -> (arg => options = options + arg), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
369 |
"v" -> (_ => verbose_build = true)) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
370 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
371 |
val more_args = getopts(args) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
372 |
val session = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
373 |
more_args match { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
374 |
case List(a) => a |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
375 |
case _ => getopts.usage() |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
376 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
377 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
378 |
val progress = new Console_Progress(verbose = verbose_build) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
379 |
val store = Sessions.store(options) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
380 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
381 |
progress.interrupt_handler { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
382 |
if (!no_build) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
383 |
val res = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
384 |
Build.build(options, selection = Sessions.Selection.session(session), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
385 |
dirs = dirs, progress = progress, verbose = verbose_build) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
386 |
if (!res.ok) error("Failed to build session " + quote(session)) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
387 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
388 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
389 |
val deps = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
390 |
Sessions.load_structure(options + "document=pdf", dirs = dirs). |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
391 |
selection_deps(Sessions.Selection.session(session)) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
392 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
393 |
build_documents(session, deps, store, progress = progress, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
394 |
verbose = true, verbose_latex = verbose_latex) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
395 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
396 |
}) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
397 |
} |