author | wenzelm |
Tue, 17 Nov 2020 16:34:01 +0100 | |
changeset 72634 | 5cea0993ee4f |
parent 72623 | e788488b0607 |
child 72648 | 1cbac4ae934d |
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 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
4 |
Theory presentation: HTML and LaTeX documents. |
50707
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 |
|
51402 | 10 |
import scala.collection.immutable.SortedMap |
11 |
||
12 |
||
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
13 |
object Present |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
14 |
{ |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
15 |
/* maintain chapter index -- NOT thread-safe */ |
50707
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 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
18 |
|
51402 | 19 |
private def read_sessions(dir: Path): List[(String, String)] = |
20 |
{ |
|
51416 | 21 |
val path = dir + sessions_path |
22 |
if (path.is_file) { |
|
23 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset
|
24 |
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) |
51416 | 25 |
} |
26 |
else Nil |
|
51402 | 27 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
28 |
|
51402 | 29 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
30 |
{ |
|
31 |
import XML.Encode._ |
|
32 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
33 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
34 |
|
61372 | 35 |
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
|
36 |
{ |
72376 | 37 |
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
|
38 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
39 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
40 |
try { read_sessions(dir) } |
51987 | 41 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
42 |
|
51402 | 43 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
65988 | 44 |
write_sessions(dir, sessions) |
51402 | 45 |
|
65988 | 46 |
val title = "Isabelle/" + chapter + " sessions" |
47 |
HTML.write_document(dir, "index.html", |
|
48 |
List(HTML.title(title + " (" + Distribution.version + ")")), |
|
49 |
HTML.chapter(title) :: |
|
50 |
(if (sessions.isEmpty) Nil |
|
51 |
else |
|
65992 | 52 |
List(HTML.div("sessions", |
53 |
List(HTML.description( |
|
65988 | 54 |
sessions.map({ case (name, description) => |
69318 | 55 |
val descr = Symbol.trim_blank_lines(description) |
65989 | 56 |
(List(HTML.link(name + "/index.html", HTML.text(name))), |
69318 | 57 |
if (descr == "") Nil |
58 |
else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
59 |
} |
61372 | 60 |
|
61 |
def make_global_index(browser_info: Path) |
|
62 |
{ |
|
63 |
if (!(browser_info + Path.explode("index.html")).is_file) { |
|
72375 | 64 |
Isabelle_System.make_directory(browser_info) |
61372 | 65 |
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
66 |
browser_info + Path.explode("isabelle.gif")) |
|
67 |
File.write(browser_info + Path.explode("index.html"), |
|
68 |
File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
|
69 |
File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
|
70 |
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
|
71 |
} |
|
72 |
} |
|
73 |
||
74 |
||
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
75 |
/* present session */ |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
76 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
77 |
val session_graph_path = Path.explode("session_graph.pdf") |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
78 |
val readme_path = Path.basic("README.html") |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
79 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
80 |
def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html" |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
81 |
def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
82 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
83 |
def theory_link(name: Document.Node.Name): XML.Tree = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
84 |
HTML.link(html_name(name), HTML.text(name.theory_base_name)) |
61372 | 85 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
86 |
def session_html(session: String, deps: Sessions.Deps, store: Sessions.Store): Path = |
61372 | 87 |
{ |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
88 |
val info = deps.sessions_structure(session) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
89 |
val options = info.options |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
90 |
val base = deps(session) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
91 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
92 |
val session_dir = store.browser_info + info.chapter_session |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
93 |
val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts")) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
94 |
for (entry <- Isabelle_Fonts.fonts(hidden = true)) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
95 |
File.copy(entry.path, session_fonts) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
96 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
97 |
Bytes.write(session_dir + session_graph_path, |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
98 |
graphview.Graph_File.make_pdf(options, base.session_graph_display)) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
99 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
100 |
val links = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
101 |
{ |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
102 |
val deps_link = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
103 |
HTML.link(session_graph_path, HTML.text("theory dependencies")) |
61372 | 104 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
105 |
val readme_links = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
106 |
if ((info.dir + readme_path).is_file) { |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
107 |
File.copy(info.dir + readme_path, session_dir + readme_path) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
108 |
List(HTML.link(readme_path, HTML.text("README"))) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
109 |
} |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
110 |
else Nil |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
111 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
112 |
val document_links = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
113 |
for ((name, _) <- info.documents) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
114 |
yield HTML.link(Path.basic(name).pdf, HTML.text(name)) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
115 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
116 |
Library.separate(HTML.break ::: HTML.nl, |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
117 |
(deps_link :: readme_links ::: document_links). |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
118 |
map(link => HTML.text("View ") ::: List(link))).flatten |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
119 |
} |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
120 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
121 |
val theories = |
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
122 |
using(Export.open_database_context(deps.sessions_structure, store))(context => |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
123 |
for { |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
124 |
name <- base.session_theories |
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
125 |
entry <- context.try_entry(session, name.theory, document_html_name(name)) |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
126 |
} yield name -> entry.uncompressed(cache = store.xz_cache)) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
127 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
128 |
val theories_body = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
129 |
HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name))) |
61500 | 130 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
131 |
val title = "Session " + session |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
132 |
HTML.write_document(session_dir, "index.html", |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
133 |
List(HTML.title(title + " (" + Distribution.version + ")")), |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
134 |
HTML.div("head", List(HTML.chapter(title), HTML.par(links))) :: |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
135 |
(if (theories.isEmpty) Nil |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
136 |
else List(HTML.div("theories", List(HTML.section("Theories"), theories_body))))) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
137 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
138 |
for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
139 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
140 |
session_dir |
61372 | 141 |
} |
66040 | 142 |
|
143 |
||
67253 | 144 |
/** preview **/ |
145 |
||
67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
146 |
sealed case class Preview(title: String, content: String) |
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
147 |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
148 |
def preview( |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
149 |
resources: Resources, |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
150 |
snapshot: Document.Snapshot, |
67262 | 151 |
plain_text: Boolean = false, |
67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
152 |
fonts_url: String => String = HTML.fonts_url()): Preview = |
67253 | 153 |
{ |
154 |
require(!snapshot.is_outdated) |
|
155 |
||
67264 | 156 |
def output_document(title: String, body: XML.Body): String = |
157 |
HTML.output_document( |
|
158 |
List( |
|
69362 | 159 |
HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), |
67264 | 160 |
HTML.title(title)), |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
161 |
List(HTML.source(body)), css = "", structural = false) |
67264 | 162 |
|
67253 | 163 |
val name = snapshot.node_name |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
164 |
|
67264 | 165 |
if (plain_text) { |
69366 | 166 |
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
|
167 |
val content = output_document(title, HTML.text(snapshot.node.source)) |
67264 | 168 |
Preview(title, content) |
169 |
} |
|
67253 | 170 |
else { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
171 |
resources.make_preview(snapshot) match { |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
172 |
case Some(preview) => preview |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
173 |
case None => |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
174 |
val title = |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
175 |
if (name.is_theory) "Theory " + quote(name.theory_base_name) |
69366 | 176 |
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
|
177 |
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
|
178 |
Preview(title, content) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
179 |
} |
67253 | 180 |
} |
181 |
} |
|
182 |
||
183 |
||
67264 | 184 |
/* PIDE document */ |
66040 | 185 |
|
67336 | 186 |
private val document_elements = |
187 |
Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + |
|
188 |
Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE |
|
189 |
||
190 |
private val div_elements = |
|
191 |
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, |
|
192 |
HTML.descr.name) |
|
193 |
||
194 |
private def html_div(html: XML.Body): Boolean = |
|
195 |
html exists { |
|
196 |
case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) |
|
197 |
case XML.Text(_) => false |
|
198 |
} |
|
199 |
||
200 |
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
|
201 |
if (html.forall(_ == HTML.no_text)) HTML.no_text |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
202 |
else if (html_div(html)) HTML.div(c, html) |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
203 |
else HTML.span(c, html) |
66040 | 204 |
|
66075 | 205 |
private def make_html(xml: XML.Body): XML.Body = |
66040 | 206 |
xml map { |
67336 | 207 |
case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => |
208 |
html_class(Markup.Language.DOCUMENT, make_html(body)) |
|
209 |
case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) |
|
210 |
case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) |
|
211 |
case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text |
|
212 |
case XML.Elem(Markup.Markdown_List(kind), body) => |
|
213 |
if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) |
|
66040 | 214 |
case XML.Elem(markup, body) => |
66044 | 215 |
val name = markup.name |
216 |
val html = |
|
217 |
markup.properties match { |
|
218 |
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => |
|
67336 | 219 |
List(html_class(kind, make_html(body))) |
66044 | 220 |
case _ => |
221 |
make_html(body) |
|
222 |
} |
|
66075 | 223 |
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { |
67336 | 224 |
case Some(c) => html_class(c.toString, html) |
225 |
case None => html_class(name, html) |
|
66044 | 226 |
} |
66040 | 227 |
case XML.Text(text) => |
228 |
XML.Text(Symbol.decode(text)) |
|
229 |
} |
|
230 |
||
67253 | 231 |
def pide_document(snapshot: Document.Snapshot): XML.Body = |
67336 | 232 |
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
|
233 |
|
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset
|
234 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
235 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
236 |
/** build documents **/ |
72565 | 237 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
238 |
val session_tex_path = Path.explode("session.tex") |
72565 | 239 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
240 |
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
|
241 |
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
|
242 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
243 |
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
|
244 |
Library.terminate_lines( |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
245 |
tags.map(tag => |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
246 |
tag.toList match { |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
247 |
case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
248 |
case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
249 |
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" |
67201 | 250 |
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
|
251 |
})) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
252 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
253 |
def build_documents( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
254 |
session: String, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
255 |
deps: Sessions.Deps, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
256 |
store: Sessions.Store, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
257 |
progress: Progress = new Progress, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
258 |
verbose: Boolean = false, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
259 |
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
|
260 |
{ |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
261 |
/* session info */ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
262 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
263 |
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
|
264 |
val options = info.options |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
265 |
val base = deps(session) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
266 |
val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) |
67177 | 267 |
|
72574
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 |
/* prepare document directory */ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
270 |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72599
diff
changeset
|
271 |
lazy val tex_files = |
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
272 |
using(Export.open_database_context(deps.sessions_structure, store))(context => |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
273 |
for (name <- base.session_theories ::: base.document_theories) |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
274 |
yield { |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
275 |
val entry = context.entry(session, name.theory, document_tex_name(name)) |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
276 |
Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache) |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
277 |
} |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72623
diff
changeset
|
278 |
) |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72599
diff
changeset
|
279 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
280 |
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
|
281 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
282 |
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
|
283 |
Isabelle_System.make_directory(doc_dir) |
67176
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 |
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
|
286 |
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
|
287 |
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
|
288 |
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
|
289 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
290 |
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
|
291 |
Library.terminate_lines( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
292 |
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
|
293 |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72599
diff
changeset
|
294 |
for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
295 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
296 |
val root1 = "root_" + doc_name |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
297 |
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
|
298 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
299 |
(doc_dir, root) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
300 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
301 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
302 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
303 |
/* produce documents */ |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
304 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
305 |
val doc_output = info.document_output |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
306 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
307 |
val docs = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
308 |
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
|
309 |
yield { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
310 |
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
|
311 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
312 |
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
|
313 |
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
|
314 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
315 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
316 |
// bash scripts |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
317 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
318 |
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
|
319 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
320 |
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
|
321 |
"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
|
322 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
323 |
def bash(items: String*): Process_Result = |
72599 | 324 |
progress.bash(items.mkString(" && "), cwd = doc_dir.file, |
325 |
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
|
326 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
327 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
328 |
// prepare document |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
329 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
330 |
val result = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
331 |
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
|
332 |
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
|
333 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
334 |
else { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
335 |
bash( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
336 |
latex_bash(), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
337 |
"{ [ ! -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
|
338 |
"{ [ ! -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
|
339 |
latex_bash(), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
340 |
latex_bash()) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
341 |
} |
67204 | 342 |
|
72574
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 |
// result |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
345 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
346 |
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
|
347 |
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
|
348 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
349 |
if (!result.ok) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
350 |
cat_error( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
351 |
Library.trim_line(result.err), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
352 |
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
|
353 |
"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
|
354 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
355 |
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
|
356 |
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
|
357 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
358 |
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
|
359 |
}) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
360 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
361 |
|
72595 | 362 |
def output(dir: Path) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
363 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
364 |
Isabelle_System.make_directory(dir) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
365 |
for ((name, pdf) <- docs) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
366 |
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
|
367 |
Bytes.write(path, pdf) |
72595 | 368 |
progress.echo_document(path) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
369 |
} |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
370 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
371 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
372 |
if (info.options.bool("browser_info") || doc_output.isEmpty) { |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
373 |
output(store.browser_info + info.chapter_session) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
374 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
375 |
|
72595 | 376 |
doc_output.foreach(output) |
72574
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 |
docs |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
379 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
380 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
381 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
382 |
/* Isabelle tool wrapper */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
383 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
384 |
val isabelle_tool = |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
385 |
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
|
386 |
{ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
387 |
var verbose_latex = false |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
388 |
var dirs: List[Path] = Nil |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
389 |
var no_build = false |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
390 |
var options = Options.init() |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
391 |
var verbose_build = false |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
392 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
393 |
val getopts = Getopts( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
394 |
""" |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
395 |
Usage: isabelle document [OPTIONS] SESSION |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
396 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
397 |
Options are: |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
398 |
-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
|
399 |
-V verbose latex |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
400 |
-d DIR include session directory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
401 |
-n no build of session |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
402 |
-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
|
403 |
-v verbose build |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
404 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
405 |
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
|
406 |
""", |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
407 |
"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
|
408 |
"V" -> (_ => verbose_latex = true), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
409 |
"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
|
410 |
"n" -> (_ => no_build = true), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
411 |
"o:" -> (arg => options = options + arg), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
412 |
"v" -> (_ => verbose_build = true)) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
413 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
414 |
val more_args = getopts(args) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
415 |
val session = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
416 |
more_args match { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
417 |
case List(a) => a |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
418 |
case _ => getopts.usage() |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
419 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
420 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
421 |
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
|
422 |
val store = Sessions.store(options) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
423 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
424 |
progress.interrupt_handler { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
425 |
if (!no_build) { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
426 |
val res = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
427 |
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
|
428 |
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
|
429 |
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
|
430 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
431 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
432 |
val deps = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
433 |
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
|
434 |
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
|
435 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
436 |
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
|
437 |
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
|
438 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
439 |
}) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
440 |
} |