author  wenzelm 
Fri, 22 Dec 2017 17:19:53 +0100  
changeset 67260  ecd607631bc7 
parent 67256  ce7d856680d1 
child 67262  46540a2ead4b 
permissions  rwrr 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

1 
/* Title: Pure/Thy/present.scala 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

3 

5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

4 
Theory presentation: HTML. 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

5 
*/ 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

6 

5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

7 
package isabelle 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

8 

5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

9 

61372  10 
import java.io.{File => JFile} 
11 

51402  12 
import scala.collection.immutable.SortedMap 
13 

14 

50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

15 
object Present 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

16 
{ 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

17 
/* maintain chapter index  NOT threadsafe */ 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

18 

51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

19 
private val sessions_path = Path.basic(".sessions") 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

20 

51402  21 
private def read_sessions(dir: Path): List[(String, String)] = 
22 
{ 

51416  23 
val path = dir + sessions_path 
24 
if (path.is_file) { 

25 
import XML.Decode._ 

65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset

26 
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) 
51416  27 
} 
28 
else Nil 

51402  29 
} 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

30 

51402  31 
private def write_sessions(dir: Path, sessions: List[(String, String)]) 
32 
{ 

33 
import XML.Encode._ 

34 
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) 

35 
} 

50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

36 

61372  37 
def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

38 
{ 
61372  39 
val dir = browser_info + Path.basic(chapter) 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

40 
Isabelle_System.mkdirs(dir) 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

41 

51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

42 
val sessions0 = 
51406
950b897f95bb
proper path  I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset

43 
try { read_sessions(dir) } 
51987  44 
catch { case _: XML.Error => Nil } 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

45 

51402  46 
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList 
65988  47 
write_sessions(dir, sessions) 
51402  48 

65988  49 
val title = "Isabelle/" + chapter + " sessions" 
50 
HTML.write_document(dir, "index.html", 

51 
List(HTML.title(title + " (" + Distribution.version + ")")), 

52 
HTML.chapter(title) :: 

53 
(if (sessions.isEmpty) Nil 

54 
else 

65992  55 
List(HTML.div("sessions", 
56 
List(HTML.description( 

65988  57 
sessions.map({ case (name, description) => 
65989  58 
(List(HTML.link(name + "/index.html", HTML.text(name))), 
59 
if (description == "") Nil 

66038  60 
else HTML.break ::: List(HTML.pre(HTML.text(description)))) }))))))) 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
50707
diff
changeset

61 
} 
61372  62 

63 
def make_global_index(browser_info: Path) 

64 
{ 

65 
if (!(browser_info + Path.explode("index.html")).is_file) { 

66 
Isabelle_System.mkdirs(browser_info) 

67 
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), 

68 
browser_info + Path.explode("isabelle.gif")) 

69 
File.write(browser_info + Path.explode("index.html"), 

70 
File.read(Path.explode("~~/lib/html/library_index_header.template")) + 

71 
File.read(Path.explode("~~/lib/html/library_index_content.template")) + 

72 
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) 

73 
} 

74 
} 

75 

76 

77 
/* finish session */ 

78 

79 
def finish( 

80 
progress: Progress, 

81 
browser_info: Path, 

82 
graph_file: JFile, 

62631  83 
info: Sessions.Info, 
61372  84 
name: String) 
85 
{ 

86 
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) 

65089  87 
val session_fonts = session_prefix + Path.explode("fonts") 
61372  88 

89 
if (info.options.bool("browser_info")) { 

65089  90 
Isabelle_System.mkdirs(session_fonts) 
62971
087e36ce0593
back to exact copy of nontext file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset

91 

087e36ce0593
back to exact copy of nontext file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset

92 
val session_graph = session_prefix + Path.basic("session_graph.pdf") 
087e36ce0593
back to exact copy of nontext file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset

93 
File.copy(graph_file, session_graph.file) 
087e36ce0593
back to exact copy of nontext file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset

94 
Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph)) 
087e36ce0593
back to exact copy of nontext file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset

95 

66000  96 
HTML.write_isabelle_css(session_prefix) 
61500  97 

65083  98 
for (font < Isabelle_System.fonts(html = true)) 
65089  99 
File.copy(font, session_fonts) 
61372  100 
} 
101 
} 

66040  102 

103 

67253  104 
/** preview **/ 
105 

67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

106 
sealed case class Preview(title: String, content: String) 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

107 

ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

108 
def preview(snapshot: Document.Snapshot, 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

109 
plain: Boolean = false, 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

110 
fonts_url: String => String = HTML.fonts_url()): Preview = 
67253  111 
{ 
112 
require(!snapshot.is_outdated) 

113 

114 
val name = snapshot.node_name 

67256  115 
if (name.is_bibtex && !plain) { 
116 
val title = "Bibliography " + quote(name.path.base_name) 

67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

117 
val content = 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

118 
Isabelle_System.with_tmp_file("bib", "bib") { bib => 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

119 
File.write(bib, snapshot.node.source) 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

120 
Bibtex.html_output(List(bib), style = "unsort", title = title) 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

121 
} 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

122 
Preview(title, content) 
67256  123 
} 
67253  124 
else { 
67256  125 
val (title, body) = 
67253  126 
if (name.is_theory && !plain) 
127 
("Theory " + quote(name.theory_base_name), pide_document(snapshot)) 

128 
else ("File " + quote(name.path.base_name), text_document(snapshot)) 

129 

67260
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

130 
val content = 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

131 
HTML.output_document( 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

132 
List(HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)), 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

133 
HTML.title(title)), List(HTML.source(body)), css = "") 
ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

134 

ecd607631bc7
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
67256
diff
changeset

135 
Preview(title, content) 
67253  136 
} 
137 
} 

138 

139 

66040  140 
/* theory document */ 
141 

142 
private val document_span_elements = 

66075  143 
Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT 
66040  144 

66075  145 
private def make_html(xml: XML.Body): XML.Body = 
66040  146 
xml map { 
147 
case XML.Wrapped_Elem(markup, body1, body2) => 

148 
XML.Wrapped_Elem(markup, make_html(body1), make_html(body2)) 

149 
case XML.Elem(markup, body) => 

66044  150 
val name = markup.name 
151 
val html = 

152 
markup.properties match { 

153 
case Markup.Kind(kind) if kind == Markup.COMMAND  kind == Markup.KEYWORD => 

154 
List(HTML.span(kind, make_html(body))) 

155 
case _ => 

156 
make_html(body) 

157 
} 

66075  158 
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { 
159 
case Some(c) => HTML.span(c.toString, html) 

160 
case None => HTML.span(name, html) 

66044  161 
} 
66040  162 
case XML.Text(text) => 
163 
XML.Text(Symbol.decode(text)) 

164 
} 

165 

67253  166 
def pide_document(snapshot: Document.Snapshot): XML.Body = 
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset

167 
make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements)) 
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset

168 

4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset

169 

4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset

170 
/* text document */ 
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset

171 

4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67204
diff
changeset

172 
def text_document(snapshot: Document.Snapshot): XML.Body = 
67251  173 
snapshot.node.source match { 
67247  174 
case "" => Nil 
175 
case txt => List(XML.Text(Symbol.decode(txt))) 

176 
} 

67176
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

177 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

178 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

179 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

180 
/** build document **/ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

181 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

182 
val default_document_name = "document" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

183 
val default_document_format = "pdf" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

184 
val document_formats = List("pdf", "dvi") 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

185 
def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

186 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

187 
def document_tags(tags: List[String]): String = 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

188 
{ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

189 
cat_lines( 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

190 
tags.map(tag => 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

191 
tag.toList match { 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

192 
case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

193 
case '' :: cs => "\\isadroptag{" + cs.mkString + "}" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

194 
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" 
67201  195 
case cs => "\\isakeeptag{" + cs.mkString + "}" 
67176
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

196 
})) + "\n" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

197 
} 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

198 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

199 
def build_document( 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

200 
document_name: String = default_document_name, 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

201 
document_format: String = default_document_format, 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

202 
document_dir: Option[Path] = None, 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

203 
tags: List[String] = Nil) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

204 
{ 
67177  205 
val document_target = Path.parent + Path.explode(document_name).ext(document_format) 
206 

67176
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

207 
if (!document_formats.contains(document_format)) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

208 
error("Bad document output format: " + quote(document_format)) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

209 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

210 
val dir = document_dir getOrElse default_document_dir(document_name) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

211 
if (!dir.is_dir) error("Bad document output directory " + dir) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

212 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

213 
val root_name = 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

214 
{ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

215 
val root1 = "root_" + document_name 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

216 
if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

217 
} 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

218 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

219 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

220 
/* bash scripts */ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

221 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

222 
def root_bash(ext: String): String = Bash.string(root_name + "." + ext) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

223 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

224 
def latex_bash(fmt: String, ext: String = "tex"): String = 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

225 
"isabelle latex o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

226 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

227 
def bash(script: String): Process_Result = 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

228 
Isabelle_System.bash(script, cwd = dir.file) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

229 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

230 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

231 
/* prepare document */ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

232 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

233 
File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags)) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

234 

67204  235 
List("log", "blg").foreach(ext => (dir + Path.explode(root_name).ext(ext)).file.delete) 
236 

67176
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

237 
val result = 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

238 
if ((dir + Path.explode("build")).is_file) { 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

239 
bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name)) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

240 
} 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

241 
else { 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

242 
bash( 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

243 
List( 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

244 
latex_bash("sty"), 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

245 
latex_bash(document_format), 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

246 
"{ [ ! f " + root_bash("bib") + " ]  " + latex_bash("bbl") + "; }", 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

247 
"{ [ ! f " + root_bash("idx") + " ]  " + latex_bash("idx") + "; }", 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

248 
latex_bash(document_format), 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

249 
latex_bash(document_format)).mkString(" && ")) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

250 
} 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

251 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

252 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

253 
/* result */ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

254 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

255 
if (!result.ok) { 
67203  256 
cat_error( 
257 
cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)), 

67187  258 
"Failed to build document in " + File.path(dir.absolute_file)) 
67176
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

259 
} 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

260 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

261 
bash("[ f " + root_bash(document_format) + " ] && cp f " + 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

262 
root_bash(document_format) + " " + File.bash_path(document_target)).check 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

263 
} 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

264 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

265 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

266 
/* Isabelle tool wrapper */ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

267 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

268 
val isabelle_tool = 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

269 
Isabelle_Tool("document", "prepare theory session document", args => 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

270 
{ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

271 
var document_dir: Option[Path] = None 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

272 
var document_name = default_document_name 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

273 
var document_format = default_document_format 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

274 
var tags: List[String] = Nil 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

275 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

276 
val getopts = Getopts(""" 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

277 
Usage: isabelle document [OPTIONS] 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

278 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

279 
Options are: 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

280 
d DIR document output directory (default """ + 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

281 
default_document_dir(default_document_name) + """) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

282 
n NAME document name (default """ + quote(default_document_name) + """) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

283 
o FORMAT document format: """ + 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

284 
commas(document_formats.map(fmt => 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

285 
fmt + (if (fmt == default_document_format) " (default)" else ""))) + """ 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

286 
t TAGS markup for tagged regions 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

287 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

288 
Prepare the theory session document in document directory, producing the 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

289 
specified output format. 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

290 
""", 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

291 
"d:" > (arg => document_dir = Some(Path.explode(arg))), 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

292 
"n:" > (arg => document_name = arg), 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

293 
"o:" > (arg => document_format = arg), 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

294 
"t:" > (arg => tags = space_explode(',', arg))) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

295 

13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

296 
val more_args = getopts(args) 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

297 
if (more_args.nonEmpty) getopts.usage() 
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

298 

67180  299 
try { 
300 
build_document(document_dir = document_dir, document_name = document_name, 

301 
document_format = document_format, tags = tags) 

302 
} 

303 
catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) } 

67176
13b5c3ff1954
reimplemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
66075
diff
changeset

304 
}) 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset

305 
} 