author | wenzelm |
Sat, 28 Nov 2020 21:56:24 +0100 | |
changeset 72763 | 3cc73d00553c |
parent 72723 | 3b804e0ffae9 |
child 72847 | 9dda93a753b1 |
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 |
||
72652 | 13 |
object Presentation |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
14 |
{ |
72696 | 15 |
/* document info */ |
72649 | 16 |
|
72696 | 17 |
abstract class Document_Name |
18 |
{ |
|
19 |
def name: String |
|
20 |
def path: Path = Path.basic(name) |
|
21 |
||
22 |
override def toString: String = name |
|
23 |
} |
|
72683 | 24 |
|
72649 | 25 |
object Document_Variant |
26 |
{ |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
27 |
def parse(name: String, tags: String): Document_Variant = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
28 |
Document_Variant(name, Library.space_explode(',', tags)) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
29 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
30 |
def parse(opt: String): Document_Variant = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
31 |
Library.space_explode('=', opt) match { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
32 |
case List(name) => Document_Variant(name, Nil) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
33 |
case List(name, tags) => parse(name, tags) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
34 |
case _ => error("Malformed document variant: " + quote(opt)) |
72649 | 35 |
} |
36 |
} |
|
37 |
||
72696 | 38 |
sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name |
72649 | 39 |
{ |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
40 |
def print_tags: String = tags.mkString(",") |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
41 |
def print: String = if (tags.isEmpty) name else name + "=" + print_tags |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
42 |
|
72649 | 43 |
def latex_sty: String = |
44 |
Library.terminate_lines( |
|
45 |
tags.map(tag => |
|
46 |
tag.toList match { |
|
47 |
case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" |
|
48 |
case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" |
|
49 |
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" |
|
50 |
case cs => "\\isakeeptag{" + cs.mkString + "}" |
|
51 |
})) |
|
72696 | 52 |
} |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
53 |
|
72696 | 54 |
sealed case class Document_Input(name: String, sources: SHA1.Digest) |
55 |
extends Document_Name |
|
56 |
||
57 |
sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) |
|
58 |
extends Document_Name |
|
59 |
{ |
|
60 |
def log: String = log_xz.uncompress().text |
|
72699 | 61 |
def log_lines: List[String] = split_lines(log) |
72700 | 62 |
|
63 |
def write(db: SQL.Database, session_name: String) = |
|
64 |
write_document(db, session_name, this) |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
65 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
66 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
67 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
68 |
/* SQL data model */ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
69 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
70 |
object Data |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
71 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
72 |
val session_name = SQL.Column.string("session_name").make_primary_key |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
73 |
val name = SQL.Column.string("name").make_primary_key |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
74 |
val sources = SQL.Column.string("sources") |
72696 | 75 |
val log_xz = SQL.Column.bytes("log_xz") |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
76 |
val pdf = SQL.Column.bytes("pdf") |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
77 |
|
72696 | 78 |
val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
79 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
80 |
def where_equal(session_name: String, name: String = ""): SQL.Source = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
81 |
"WHERE " + Data.session_name.equal(session_name) + |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
82 |
(if (name == "") "" else " AND " + Data.name.equal(name)) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
83 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
84 |
|
72696 | 85 |
def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
86 |
{ |
72696 | 87 |
val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
88 |
db.using_statement(select)(stmt => |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
89 |
stmt.execute_query().iterator(res => |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
90 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
91 |
val name = res.string(Data.name) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
92 |
val sources = res.string(Data.sources) |
72696 | 93 |
Document_Input(name, SHA1.fake(sources)) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
94 |
}).toList) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
95 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
96 |
|
72696 | 97 |
def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] = |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
98 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
99 |
val select = Data.table.select(sql = Data.where_equal(session_name, name)) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
100 |
db.using_statement(select)(stmt => |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
101 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
102 |
val res = stmt.execute_query() |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
103 |
if (res.next()) { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
104 |
val name = res.string(Data.name) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
105 |
val sources = res.string(Data.sources) |
72696 | 106 |
val log_xz = res.bytes(Data.log_xz) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
107 |
val pdf = res.bytes(Data.pdf) |
72696 | 108 |
Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
109 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
110 |
else None |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
111 |
}) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
112 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
113 |
|
72696 | 114 |
def write_document(db: SQL.Database, session_name: String, doc: Document_Output) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
115 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
116 |
db.using_statement(Data.table.insert())(stmt => |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
117 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
118 |
stmt.string(1) = session_name |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
119 |
stmt.string(2) = doc.name |
72696 | 120 |
stmt.string(3) = doc.sources.toString |
121 |
stmt.bytes(4) = doc.log_xz |
|
122 |
stmt.bytes(5) = doc.pdf |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
123 |
stmt.execute() |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
124 |
}) |
72649 | 125 |
} |
126 |
||
127 |
||
72648 | 128 |
/* presentation context */ |
129 |
||
130 |
object Context |
|
131 |
{ |
|
132 |
val none: Context = new Context { def enabled: Boolean = false } |
|
133 |
val standard: Context = new Context { def enabled: Boolean = true } |
|
134 |
||
135 |
def dir(path: Path): Context = |
|
136 |
new Context { |
|
137 |
def enabled: Boolean = true |
|
138 |
override def dir(store: Sessions.Store): Path = path |
|
139 |
} |
|
140 |
||
141 |
def make(s: String): Context = |
|
142 |
if (s == ":") standard else dir(Path.explode(s)) |
|
143 |
} |
|
144 |
||
145 |
abstract class Context private |
|
146 |
{ |
|
147 |
def enabled: Boolean |
|
148 |
def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info |
|
149 |
def dir(store: Sessions.Store): Path = store.presentation_dir |
|
150 |
def dir(store: Sessions.Store, info: Sessions.Info): Path = |
|
72670 | 151 |
dir(store) + Path.explode(info.chapter_session) |
72648 | 152 |
} |
153 |
||
154 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
155 |
/* maintain chapter index -- NOT thread-safe */ |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
156 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
157 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
158 |
|
51402 | 159 |
private def read_sessions(dir: Path): List[(String, String)] = |
160 |
{ |
|
51416 | 161 |
val path = dir + sessions_path |
162 |
if (path.is_file) { |
|
163 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset
|
164 |
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) |
51416 | 165 |
} |
166 |
else Nil |
|
51402 | 167 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
168 |
|
51402 | 169 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
170 |
{ |
|
171 |
import XML.Encode._ |
|
172 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
173 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
174 |
|
61372 | 175 |
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
|
176 |
{ |
72376 | 177 |
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
|
178 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
179 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
180 |
try { read_sessions(dir) } |
51987 | 181 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
182 |
|
51402 | 183 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
65988 | 184 |
write_sessions(dir, sessions) |
51402 | 185 |
|
65988 | 186 |
val title = "Isabelle/" + chapter + " sessions" |
187 |
HTML.write_document(dir, "index.html", |
|
188 |
List(HTML.title(title + " (" + Distribution.version + ")")), |
|
189 |
HTML.chapter(title) :: |
|
190 |
(if (sessions.isEmpty) Nil |
|
191 |
else |
|
65992 | 192 |
List(HTML.div("sessions", |
193 |
List(HTML.description( |
|
65988 | 194 |
sessions.map({ case (name, description) => |
69318 | 195 |
val descr = Symbol.trim_blank_lines(description) |
65989 | 196 |
(List(HTML.link(name + "/index.html", HTML.text(name))), |
69318 | 197 |
if (descr == "") Nil |
198 |
else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
199 |
} |
61372 | 200 |
|
201 |
def make_global_index(browser_info: Path) |
|
202 |
{ |
|
203 |
if (!(browser_info + Path.explode("index.html")).is_file) { |
|
72375 | 204 |
Isabelle_System.make_directory(browser_info) |
61372 | 205 |
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
206 |
browser_info + Path.explode("isabelle.gif")) |
|
207 |
File.write(browser_info + Path.explode("index.html"), |
|
208 |
File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
|
209 |
File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
|
210 |
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
|
211 |
} |
|
212 |
} |
|
213 |
||
214 |
||
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
215 |
/* present session */ |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
216 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
217 |
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
|
218 |
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
|
219 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
220 |
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
|
221 |
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
|
222 |
|
72669 | 223 |
def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = { |
224 |
if (keywords.is_command(tok, Keyword.theory_end)) |
|
225 |
List(Markup.KEYWORD2, Markup.KEYWORD) |
|
226 |
else if (keywords.is_command(tok, Keyword.proof_asm)) |
|
227 |
List(Markup.KEYWORD3, Markup.COMMAND) |
|
228 |
else if (keywords.is_command(tok, Keyword.improper)) |
|
229 |
List(Markup.KEYWORD1, Markup.IMPROPER, Markup.COMMAND) |
|
230 |
else if (tok.is_command) List(Markup.KEYWORD1, Markup.COMMAND) |
|
231 |
else if (tok.is_delimiter) List(Markup.DELIMITER, Markup.KEYWORD) |
|
232 |
else if (tok.is_keyword) List(Markup.KEYWORD2, Markup.KEYWORD) |
|
233 |
else if (tok.is_comment) List(Markup.COMMENT) |
|
234 |
else { |
|
235 |
tok.kind match { |
|
236 |
case Token.Kind.VAR => List(Markup.VAR) |
|
237 |
case Token.Kind.TYPE_IDENT => List(Markup.TFREE) |
|
238 |
case Token.Kind.TYPE_VAR => List(Markup.TVAR) |
|
239 |
case Token.Kind.STRING => List(Markup.STRING) |
|
240 |
case Token.Kind.ALT_STRING => List(Markup.ALT_STRING) |
|
241 |
case Token.Kind.VERBATIM => List(Markup.VERBATIM) |
|
242 |
case Token.Kind.CARTOUCHE => List(Markup.CARTOUCHE) |
|
243 |
case _ => Nil |
|
244 |
} |
|
245 |
} |
|
246 |
} |
|
61372 | 247 |
|
72648 | 248 |
def session_html( |
249 |
session: String, |
|
250 |
deps: Sessions.Deps, |
|
72683 | 251 |
db_context: Sessions.Database_Context, |
252 |
presentation: Context) |
|
61372 | 253 |
{ |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
254 |
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
|
255 |
val options = info.options |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
256 |
val base = deps(session) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
257 |
|
72683 | 258 |
val session_dir = presentation.dir(db_context.store, info) |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
263 |
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
|
264 |
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
|
265 |
|
72673
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72670
diff
changeset
|
266 |
val documents = |
72683 | 267 |
for { |
268 |
doc <- info.document_variants |
|
72716 | 269 |
document <- db_context.input_database(session)(read_document(_, _, doc.name)) |
72696 | 270 |
} yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc } |
72673
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72670
diff
changeset
|
271 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
272 |
val links = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
273 |
{ |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
274 |
val deps_link = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
275 |
HTML.link(session_graph_path, HTML.text("theory dependencies")) |
61372 | 276 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
277 |
val readme_links = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
278 |
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
|
279 |
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
|
280 |
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
|
281 |
} |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
282 |
else Nil |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
283 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
284 |
val document_links = |
72673
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72670
diff
changeset
|
285 |
documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name))) |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
286 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
287 |
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
|
288 |
(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
|
289 |
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
|
290 |
} |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
291 |
|
72669 | 292 |
def theory_link(name1: Document.Node.Name, body: XML.Body): XML.Tree = |
293 |
{ |
|
294 |
val session1 = base.theory_qualifier(name1) |
|
295 |
val info1 = deps.sessions_structure(session1) |
|
296 |
val prefix = |
|
297 |
if (session == session1) "" |
|
298 |
else if (info.chapter == info1.chapter) "../" + session1 + "/" |
|
72670 | 299 |
else "../../" + info1.chapter_session + "/" |
72669 | 300 |
HTML.link(prefix + html_name(name1), body) |
301 |
} |
|
302 |
||
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
303 |
val theories = |
72669 | 304 |
for (name <- base.session_theories) |
305 |
yield { |
|
306 |
val syntax = base.theory_syntax(name) |
|
307 |
val keywords = syntax.keywords |
|
308 |
val spans = syntax.parse_spans(Symbol.decode(File.read(name.path))) |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
309 |
|
72669 | 310 |
val thy_body = |
311 |
{ |
|
312 |
val imports_offset = base.known_theories(name.theory).header.imports_offset |
|
313 |
var token_offset = 1 |
|
314 |
spans.flatMap(span => |
|
315 |
{ |
|
316 |
val is_init = span.is_kind(keywords, Keyword.theory_begin, false) |
|
317 |
span.content.flatMap(tok => |
|
318 |
{ |
|
319 |
val text = HTML.text(tok.source) |
|
320 |
val item = |
|
321 |
if (is_init && imports_offset.isDefinedAt(token_offset)) { |
|
322 |
List(theory_link(imports_offset(token_offset), text)) |
|
323 |
} |
|
324 |
else text |
|
325 |
||
326 |
token_offset += tok.symbol_length |
|
327 |
||
328 |
(token_markups(keywords, tok) :\ item)( |
|
329 |
{ case (c, body) => List(HTML.span(c, body)) }) |
|
330 |
}) |
|
331 |
}) |
|
332 |
} |
|
333 |
||
334 |
val title = "Theory " + name.theory_base_name |
|
335 |
HTML.write_document(session_dir, html_name(name), |
|
336 |
List(HTML.title(title)), |
|
337 |
HTML.div("head", List(HTML.chapter(title))) :: List(HTML.pre("source", thy_body))) |
|
338 |
||
339 |
List(HTML.link(html_name(name), HTML.text(name.theory_base_name))) |
|
340 |
} |
|
61500 | 341 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
342 |
val title = "Session " + session |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72600
diff
changeset
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
(if (theories.isEmpty) Nil |
72669 | 347 |
else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories)))))) |
61372 | 348 |
} |
66040 | 349 |
|
350 |
||
72682 | 351 |
|
67253 | 352 |
/** preview **/ |
353 |
||
67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
354 |
sealed case class Preview(title: String, content: String) |
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
355 |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
356 |
def preview( |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
357 |
resources: Resources, |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
358 |
snapshot: Document.Snapshot, |
67262 | 359 |
plain_text: Boolean = false, |
67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset
|
360 |
fonts_url: String => String = HTML.fonts_url()): Preview = |
67253 | 361 |
{ |
362 |
require(!snapshot.is_outdated) |
|
363 |
||
67264 | 364 |
def output_document(title: String, body: XML.Body): String = |
365 |
HTML.output_document( |
|
366 |
List( |
|
69362 | 367 |
HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), |
67264 | 368 |
HTML.title(title)), |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
369 |
List(HTML.source(body)), css = "", structural = false) |
67264 | 370 |
|
67253 | 371 |
val name = snapshot.node_name |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
372 |
|
67264 | 373 |
if (plain_text) { |
69366 | 374 |
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
|
375 |
val content = output_document(title, HTML.text(snapshot.node.source)) |
67264 | 376 |
Preview(title, content) |
377 |
} |
|
67253 | 378 |
else { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
379 |
resources.make_preview(snapshot) match { |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
380 |
case Some(preview) => preview |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
381 |
case None => |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
382 |
val title = |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
383 |
if (name.is_theory) "Theory " + quote(name.theory_base_name) |
69366 | 384 |
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
|
385 |
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
|
386 |
Preview(title, content) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69033
diff
changeset
|
387 |
} |
67253 | 388 |
} |
389 |
} |
|
390 |
||
391 |
||
67264 | 392 |
/* PIDE document */ |
66040 | 393 |
|
67336 | 394 |
private val document_elements = |
395 |
Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + |
|
396 |
Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE |
|
397 |
||
398 |
private val div_elements = |
|
399 |
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, |
|
400 |
HTML.descr.name) |
|
401 |
||
402 |
private def html_div(html: XML.Body): Boolean = |
|
403 |
html exists { |
|
404 |
case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) |
|
405 |
case XML.Text(_) => false |
|
406 |
} |
|
407 |
||
408 |
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
|
409 |
if (html.forall(_ == HTML.no_text)) HTML.no_text |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
410 |
else if (html_div(html)) HTML.div(c, html) |
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
67336
diff
changeset
|
411 |
else HTML.span(c, html) |
66040 | 412 |
|
66075 | 413 |
private def make_html(xml: XML.Body): XML.Body = |
66040 | 414 |
xml map { |
67336 | 415 |
case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => |
416 |
html_class(Markup.Language.DOCUMENT, make_html(body)) |
|
417 |
case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) |
|
418 |
case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) |
|
419 |
case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text |
|
420 |
case XML.Elem(Markup.Markdown_List(kind), body) => |
|
421 |
if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) |
|
66040 | 422 |
case XML.Elem(markup, body) => |
66044 | 423 |
val name = markup.name |
424 |
val html = |
|
425 |
markup.properties match { |
|
426 |
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => |
|
67336 | 427 |
List(html_class(kind, make_html(body))) |
66044 | 428 |
case _ => |
429 |
make_html(body) |
|
430 |
} |
|
66075 | 431 |
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { |
67336 | 432 |
case Some(c) => html_class(c.toString, html) |
433 |
case None => html_class(name, html) |
|
66044 | 434 |
} |
66040 | 435 |
case XML.Text(text) => |
436 |
XML.Text(Symbol.decode(text)) |
|
437 |
} |
|
438 |
||
67253 | 439 |
def pide_document(snapshot: Document.Snapshot): XML.Body = |
72723 | 440 |
make_html(snapshot.xml_markup(elements = document_elements)) |
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset
|
441 |
|
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset
|
442 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
443 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
444 |
/** build documents **/ |
72565 | 445 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
446 |
val session_tex_path = Path.explode("session.tex") |
72565 | 447 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
448 |
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
|
449 |
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
|
450 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
451 |
def build_documents( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
452 |
session: String, |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
453 |
deps: Sessions.Deps, |
72683 | 454 |
db_context: Sessions.Database_Context, |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
455 |
progress: Progress = new Progress, |
72675 | 456 |
output_sources: Option[Path] = None, |
457 |
output_pdf: Option[Path] = None, |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
458 |
verbose: Boolean = false, |
72696 | 459 |
verbose_latex: Boolean = false): List[Document_Output] = |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
460 |
{ |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
461 |
/* session info */ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
462 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
463 |
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
|
464 |
val options = info.options |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
465 |
val base = deps(session) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
466 |
val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) |
67177 | 467 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
468 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
469 |
/* prepare document directory */ |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
470 |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72599
diff
changeset
|
471 |
lazy val tex_files = |
72683 | 472 |
for (name <- base.session_theories ::: base.document_theories) |
473 |
yield { |
|
474 |
val entry = db_context.get_export(session, name.theory, document_tex_name(name)) |
|
475 |
Path.basic(tex_name(name)) -> entry.uncompressed(cache = db_context.xz_cache) |
|
476 |
} |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72599
diff
changeset
|
477 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
478 |
def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) = |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
479 |
{ |
72649 | 480 |
val doc_dir = dir + Path.basic(doc.name) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
481 |
Isabelle_System.make_directory(doc_dir) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
482 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
483 |
Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check |
72649 | 484 |
File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
485 |
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
|
486 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
487 |
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
|
488 |
Library.terminate_lines( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
489 |
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
|
490 |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
72599
diff
changeset
|
491 |
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
|
492 |
|
72649 | 493 |
val root1 = "root_" + doc.name |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
494 |
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
|
495 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
496 |
(doc_dir, root) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
497 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
498 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
499 |
def prepare_dir2(dir: Path, doc: Document_Variant): Unit = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
500 |
{ |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
501 |
val doc_dir = dir + Path.basic(doc.name) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
502 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
503 |
// non-deterministic, but irrelevant |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
504 |
Bytes.write(doc_dir + session_graph_path, graph_pdf) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
505 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
506 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
507 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
508 |
/* produce documents */ |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
509 |
|
72649 | 510 |
val documents = |
511 |
for (doc <- info.documents) |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
512 |
yield { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
513 |
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
|
514 |
{ |
72699 | 515 |
progress.echo("Preparing " + session + "/" + doc.name + " ...") |
72665 | 516 |
val start = Time.now() |
517 |
||
518 |
||
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
519 |
// prepare sources |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
520 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
521 |
val (doc_dir, root) = prepare_dir1(tmp_dir, doc) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
522 |
val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) |
72696 | 523 |
val sources = SHA1.digest_set(digests) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
524 |
prepare_dir2(tmp_dir, doc) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
525 |
|
72675 | 526 |
for (dir <- output_sources) { |
527 |
prepare_dir1(dir, doc) |
|
528 |
prepare_dir2(dir, doc) |
|
529 |
} |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
530 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
531 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
532 |
// old document from database |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
533 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
534 |
val old_document = |
72683 | 535 |
for { |
72716 | 536 |
old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) |
72696 | 537 |
if old_doc.sources == sources |
72683 | 538 |
} |
539 |
yield { |
|
72696 | 540 |
Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) |
541 |
old_doc |
|
72683 | 542 |
} |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
543 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
544 |
old_document getOrElse { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
545 |
// bash scripts |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
546 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
547 |
def root_bash(ext: String): String = Bash.string(root + "." + ext) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
548 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
549 |
def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
550 |
"isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
551 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
552 |
def bash(items: String*): Process_Result = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
553 |
progress.bash(items.mkString(" && "), cwd = doc_dir.file, |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
554 |
echo = verbose_latex, watchdog = Time.seconds(0.5)) |
67204 | 555 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
556 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
557 |
// prepare document |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
558 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
559 |
val result = |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
560 |
if ((doc_dir + Path.explode("build")).is_file) { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
561 |
bash("./build pdf " + Bash.string(doc.name)) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
562 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
563 |
else { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
564 |
bash( |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
565 |
latex_bash(), |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
566 |
"{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
567 |
"{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
568 |
latex_bash(), |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
569 |
latex_bash()) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
570 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
571 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
572 |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
573 |
// result |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
574 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
575 |
val root_pdf = Path.basic(root).pdf |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
576 |
val result_path = doc_dir + root_pdf |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
577 |
|
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
578 |
if (!result.ok) { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
579 |
cat_error( |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
580 |
Library.trim_line(result.err), |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
581 |
cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
582 |
"Failed to build document " + quote(doc.name)) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
583 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
584 |
else if (!result_path.is_file) { |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
585 |
error("Bad document result: expected to find " + root_pdf) |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
586 |
} |
72665 | 587 |
else { |
588 |
val stop = Time.now() |
|
589 |
val timing = stop - start |
|
72699 | 590 |
progress.echo("Finished " + session + "/" + doc.name + |
72665 | 591 |
" (" + timing.message_hms + " elapsed time)") |
592 |
||
72696 | 593 |
val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress() |
594 |
val pdf = Bytes.read(result_path) |
|
595 |
Document_Output(doc.name, sources, log_xz, pdf) |
|
72665 | 596 |
} |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
597 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
598 |
}) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
599 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
600 |
|
72696 | 601 |
for (dir <- output_pdf; doc <- documents) { |
72675 | 602 |
Isabelle_System.make_directory(dir) |
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
603 |
val path = dir + doc.path.pdf |
72696 | 604 |
Bytes.write(path, doc.pdf) |
72699 | 605 |
progress.echo("Document at " + path.absolute) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
606 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
607 |
|
72649 | 608 |
documents |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
609 |
} |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
610 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
611 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
612 |
/* Isabelle tool wrapper */ |
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
613 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
614 |
val isabelle_tool = |
72763 | 615 |
Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args => |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
616 |
{ |
72675 | 617 |
var output_sources: Option[Path] = None |
618 |
var output_pdf: Option[Path] = None |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
619 |
var verbose_latex = false |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
620 |
var dirs: List[Path] = Nil |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
621 |
var options = Options.init() |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
622 |
var verbose_build = false |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
623 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
624 |
val getopts = Getopts( |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
625 |
""" |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
626 |
Usage: isabelle document [OPTIONS] SESSION |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
627 |
|
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
628 |
Options are: |
72675 | 629 |
-O DIR output directory for LaTeX sources and resulting PDF |
630 |
-P DIR output directory for resulting PDF |
|
631 |
-S DIR output directory for LaTeX sources |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
632 |
-V verbose latex |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
633 |
-d DIR include session directory |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
634 |
-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
|
635 |
-v verbose build |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
636 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
637 |
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
|
638 |
""", |
72675 | 639 |
"O:" -> (arg => |
640 |
{ |
|
641 |
val dir = Path.explode(arg) |
|
642 |
output_sources = Some(dir) |
|
643 |
output_pdf = Some(dir) |
|
644 |
}), |
|
645 |
"P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), |
|
646 |
"S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
647 |
"V" -> (_ => verbose_latex = true), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
648 |
"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
|
649 |
"o:" -> (arg => options = options + arg), |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
650 |
"v" -> (_ => verbose_build = true)) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
651 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
652 |
val more_args = getopts(args) |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
653 |
val session = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
654 |
more_args match { |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
655 |
case List(a) => a |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
656 |
case _ => getopts.usage() |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
657 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
658 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
659 |
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
|
660 |
val store = Sessions.store(options) |
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset
|
661 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
662 |
progress.interrupt_handler { |
72650
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72649
diff
changeset
|
663 |
val res = |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72649
diff
changeset
|
664 |
Build.build(options, selection = Sessions.Selection.session(session), |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72649
diff
changeset
|
665 |
dirs = dirs, progress = progress, verbose = verbose_build) |
787ba1d19d3a
more robust: ensure coherence wrt. build database;
wenzelm
parents:
72649
diff
changeset
|
666 |
if (!res.ok) error("Failed to build session " + quote(session)) |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
667 |
|
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
668 |
val deps = |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
669 |
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
|
670 |
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
|
671 |
|
72675 | 672 |
if (output_sources.isEmpty && output_pdf.isEmpty) { |
673 |
progress.echo_warning("No output directory") |
|
72653
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
674 |
} |
ea35afdb1366
store documents within session database, instead of browser_info directory;
wenzelm
parents:
72652
diff
changeset
|
675 |
|
72683 | 676 |
using(store.open_database_context(deps.sessions_structure))(db_context => |
677 |
build_documents(session, deps, db_context, progress = progress, |
|
678 |
output_sources = output_sources, output_pdf = output_pdf, |
|
679 |
verbose = true, verbose_latex = verbose_latex)) |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
680 |
} |
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72565
diff
changeset
|
681 |
}) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
682 |
} |