build documents in Isabelle/Scala, based on generated tex files as session exports;
reworked "isabelle document" for quasi-offline document builds: similar functionality included in "isabelle build -o document=pdf";
--- a/NEWS Wed Nov 11 20:58:36 2020 +0100
+++ b/NEWS Wed Nov 11 21:00:14 2020 +0100
@@ -231,6 +231,11 @@
* The command-line tool "isabelle console" now supports interrupts
properly (on Linux and macOS).
+* The command-line tool "isabelle document" generates theory documents
+from the underlying session build database (using its exported {\LaTeX}
+sources). INCOMPATIBILITY, the former "isabelle document" tool was
+rather different and has been discontinued.
+
* The command-line tool "isabelle sessions" explores the structure of
Isabelle sessions and prints result names in topological order (on
stdout).
--- a/src/Doc/System/Presentation.thy Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Doc/System/Presentation.thy Wed Nov 11 21:00:14 2020 +0100
@@ -15,37 +15,15 @@
HOL, and HOL from Pure), and application sessions further on in the
hierarchy.
- The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
- for managing Isabelle sessions, including proper setup for presentation;
- @{tool build} tells the Isabelle process to run any additional stages
- required for document preparation, notably the @{tool_ref document} and
- @{tool_ref latex}. The complete tool chain for managing batch-mode Isabelle
- sessions is illustrated in \figref{fig:session-tools}.
-
- \begin{figure}[htbp]
- \begin{center}
- \begin{tabular}{lp{0.6\textwidth}}
-
- @{tool_ref mkroot} & invoked once by the user to initialize the
- session \<^verbatim>\<open>ROOT\<close> with optional \<^verbatim>\<open>document\<close>
- directory; \\
+ The command-line tools @{tool_ref mkroot} and @{tool_ref build} provide the
+ primary means for managing Isabelle sessions, including options for
+ presentation: ``\<^verbatim>\<open>document=pdf\<close>'' generates PDF output from the theory
+ session, and ``\<^verbatim>\<open>document_output=dir\<close>'' emits a copy of the document sources
+ with the PDF into the given directory (relative to the session directory).
- @{tool_ref build} & invoked repeatedly by the user to keep
- session output up-to-date (HTML, documents etc.); \\
-
- @{tool_ref process} & run through @{tool_ref build}; \\
-
- @{tool_ref document} & run by the Isabelle process if document
- preparation is enabled; \\
-
- @{tool_ref latex} & universal {\LaTeX} tool wrapper invoked
- multiple times by @{tool_ref document}; also useful for manual
- experiments; \\
-
- \end{tabular}
- \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
- \end{center}
- \end{figure}
+ Alternatively, @{tool_ref document} may be used to turn the generated
+ {\LaTeX} sources of a session (exports from its build database) into PDF,
+ using suitable invocations of @{tool_ref latex}.
\<close>
@@ -145,101 +123,56 @@
section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
text \<open>
- The @{tool_def document} tool prepares logic session documents, processing
- the sources as provided by the user and generated by Isabelle. Its usage is:
+ The @{tool_def document} tool prepares logic session documents. Its usage
+ is:
@{verbatim [display]
-\<open>Usage: isabelle document [OPTIONS]
+\<open>Usage: isabelle document [OPTIONS] SESSION
Options are:
- -d DIR document output directory (default "output/document")
- -n NAME document name (default "document")
- -t TAGS markup for tagged regions
-
- Prepare the theory session document in document directory, producing the
- specified output format.
-\<close>}
+ -O set option "document_output", relative to current directory
+ -V verbose latex
+ -d DIR include session directory
+ -n no build of session
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose build
- This tool is usually run automatically as part of the Isabelle build
- process, provided document preparation has been enabled via suitable
- options. It may be manually invoked on the generated browser information
- document output as well, e.g.\ in case of errors encountered in the batch
- run.
-
- \<^medskip>
- Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default
- is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
- will appear in the parent of this directory.
+ Prepare the theory document of a session.\<close>}
- \<^medskip>
- Option \<^verbatim>\<open>-n\<close> specifies the resulting document file name, the default is
- ``\<^verbatim>\<open>document\<close>'' (leading to ``\<^verbatim>\<open>document.pdf\<close>'').
+ Generated {\LaTeX} sources are taken from the session build database:
+ @{tool_ref build} is invoked beforehand to ensure that it is up-to-date, but
+ option \<^verbatim>\<open>-n\<close> suppresses that. Further files are generated on the spot,
+ notably essential Isabelle style files, and \<^verbatim>\<open>session.tex\<close> to input all
+ theory sources from the session (excluding imports from other sessions).
- \<^medskip>
- The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
- regions. Tags are specified as a comma separated list of modifier/name
- pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
- drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
- equivalent to the tag specification
- ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
- see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
- \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
+ \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool build}.
- \<^medskip>
- Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
- sources. This directory is supposed to contain all the files needed to
- produce the final document --- apart from the actual theories which are
- generated by Isabelle.
+ \<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.
- \<^medskip>
- For most practical purposes, @{tool document} is smart enough to create any
- of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
- a starting point. This even includes multiple runs of {\LaTeX} to
- accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
- within the same directory).
+ \<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the @{system_option document_output} option
+ relative to the current directory, while \<^verbatim>\<open>-o document_output=\<close>\<open>dir\<close> is
+ relative to the session directory.
- In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
- sources may be given. It is invoked with command-line arguments for the
- document format and the document variant name. The script needs to produce
- corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
- default variants). The main work can be again delegated to @{tool latex},
- but it is also possible to harvest generated {\LaTeX} sources and copy them
- elsewhere.
-
- \<^medskip>
- When running the session, Isabelle copies the content of the original
- \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
- ISABELLE_BROWSER_INFO}, according to the session path and document variant.
- Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
- there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
- put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
- user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
- theories.
+ For example, for output directory ``\<^verbatim>\<open>output\<close>'' and the default document
+ variant ``\<^verbatim>\<open>document\<close>'', the generated document sources are placed into the
+ subdirectory \<^verbatim>\<open>output/document/\<close> and the resulting PDF into
+ \<^verbatim>\<open>output/document.pdf\<close>.
- The {\LaTeX} versions of the theories require some macros defined in
- \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
- \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
- appropriate path specification for {\TeX} inputs.
-
- If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
- \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
- standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
- \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
- of predefined Isabelle symbols. Users may invent further symbols as well,
- just by providing {\LaTeX} macros in a similar fashion as in
- \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
+ \<^medskip> Isabelle is usually smart enough to create the PDF from the given
+ \<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index)
+ using standard {\LaTeX} tools. Alternatively, \isakeyword{document\_files}
+ in the session \<^verbatim>\<open>ROOT\<close> may include an executable \<^verbatim>\<open>build\<close> script to take
+ care of that. It is invoked with command-line arguments for the document
+ format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs to produce
+ corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default document variants
+ (the main work can be delegated to @{tool latex}). \<close>
- For proper setup of PDF documents (with hyperlinks and bookmarks),
- we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
+subsubsection \<open>Examples\<close>
- \<^medskip>
- As a final step of Isabelle document preparation, @{tool document} is run on
- the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document
- is built and installed in its proper place. The generated sources are
- deleted after successful run of {\LaTeX} and friends.
+text \<open>
+ Produce the document from session \<^verbatim>\<open>FOL\<close> with full verbosity, and a copy in
+ the current directory (subdirectory \<^verbatim>\<open>document\<close> and file \<^verbatim>\<open>document.pdf)\<close>:
- Some care is needed if the document output location is configured
- differently, say within a directory whose content is still required
- afterwards!
+ @{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>}
\<close>
--- a/src/Doc/System/Sessions.thy Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Doc/System/Sessions.thy Wed Nov 11 21:00:14 2020 +0100
@@ -190,10 +190,9 @@
\<^item> @{system_option_def "browser_info"} controls output of HTML browser
info, see also \secref{sec:info}.
- \<^item> @{system_option_def "document"} specifies the document output format,
- see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
- practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
- \<^verbatim>\<open>document=pdf\<close>.
+ \<^item> @{system_option_def "document"} controls document output for a
+ particular session or theory; \<^verbatim>\<open>document=pdf\<close> means enabled,
+ \<^verbatim>\<open>document=false\<close> means disabled (especially for particular theories).
\<^item> @{system_option_def "document_output"} specifies an alternative
directory for generated output of the document preparation system; the
@@ -203,10 +202,19 @@
document.
\<^item> @{system_option_def "document_variants"} specifies document variants as
- a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
- document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
+ a colon-separated list of \<open>name=tags\<close> entries. The default name
+ \<^verbatim>\<open>document\<close>, without additional tags.
- For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
+ Tags are specified as a comma separated list of modifier/name pairs and
+ tell {\LaTeX} how to interpret certain Isabelle command regions:
+ ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop,
+ and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
+ equivalent to the tag specification
+ ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant\<close>'';
+ see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
+ \<^verbatim>\<open>\isafoldtag\<close>, in \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
+
+ In contrast, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
--- a/src/Pure/General/path.scala Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/General/path.scala Wed Nov 11 21:00:14 2020 +0100
@@ -193,6 +193,9 @@
prfx + Path.basic(s + "." + e)
}
+ def tex: Path = ext("tex")
+ def pdf: Path = ext("pdf")
+
def backup: Path =
{
val (prfx, s) = split_path
--- a/src/Pure/PIDE/session.ML Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/PIDE/session.ML Wed Nov 11 21:00:14 2020 +0100
@@ -9,8 +9,7 @@
val get_name: unit -> string
val welcome: unit -> string
val get_keywords: unit -> Keyword.keywords
- val init: HTML.symbols -> bool -> Path.T -> string -> string -> (string * string) list ->
- (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
+ val init: HTML.symbols -> bool -> Path.T -> string list -> string -> string * string -> bool -> unit
val shutdown: unit -> unit
val finish: unit -> unit
end;
@@ -46,18 +45,12 @@
(* init *)
-val document =
- fn "" => false | "false" => false | "pdf" => true
- | doc => error ("Bad document specification " ^ quote doc);
-
-fun init symbols info info_path doc doc_output doc_variants doc_files graph_file
- parent (chapter, name) verbose =
+fun init symbols info info_path documents parent (chapter, name) verbose =
(Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
if parent_name <> parent orelse not parent_finished then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else ({chapter = chapter, name = name}, false));
- Present.init symbols info info_path (document doc)
- doc_output doc_variants doc_files graph_file (chapter, name) verbose);
+ Present.init symbols info info_path documents (chapter, name) verbose);
(* finish *)
--- a/src/Pure/System/progress.scala Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/System/progress.scala Wed Nov 11 21:00:14 2020 +0100
@@ -32,6 +32,7 @@
def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
+ def echo_document(path: Path) { echo("Document at " + path.absolute) }
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
Timing.timeit(message, enabled, echo)(e)
--- a/src/Pure/Thy/present.ML Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Thy/present.ML Wed Nov 11 21:00:14 2020 +0100
@@ -9,12 +9,8 @@
val tex_path: string -> Path.T
val get_bibtex_entries: theory -> string list
val theory_qualifier: theory -> string
- val document_option: Options.T -> {enabled: bool, disabled: bool}
- val document_variants: Options.T -> (string * string) list
- val init: HTML.symbols -> bool -> Path.T -> bool -> string -> (string * string) list ->
- (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
+ val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
val finish: unit -> unit
- val theory_output: theory -> string list -> unit
val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
end;
@@ -30,7 +26,6 @@
val html_path = html_ext o Path.basic;
val index_path = Path.basic "index.html";
val readme_html_path = Path.basic "README.html";
-val doc_indexN = "session";
val session_graph_path = Path.basic "session_graph.pdf";
val document_path = Path.ext "pdf" o Path.basic;
@@ -66,31 +61,19 @@
(** global browser info state **)
-(* type theory_info *)
-
-type theory_info = {tex_source: string list, html_source: string};
-
-fun make_theory_info (tex_source, html_source) =
- {tex_source = tex_source, html_source = html_source}: theory_info;
-
-fun map_theory_info f {tex_source, html_source} =
- make_theory_info (f (tex_source, html_source));
-
-
(* type browser_info *)
type browser_info =
- {theories: theory_info Symtab.table,
- tex_index: (int * string) list,
+ {html_theories: string Symtab.table,
html_index: (int * string) list};
-fun make_browser_info (theories, tex_index, html_index) : browser_info =
- {theories = theories, tex_index = tex_index, html_index = html_index};
+fun make_browser_info (html_theories, html_index) : browser_info =
+ {html_theories = html_theories, html_index = html_index};
-val empty_browser_info = make_browser_info (Symtab.empty, [], []);
+val empty_browser_info = make_browser_info (Symtab.empty, []);
-fun map_browser_info f {theories, tex_index, html_index} =
- make_browser_info (f (theories, tex_index, html_index));
+fun map_browser_info f {html_theories, html_index} =
+ make_browser_info (f (html_theories, html_index));
(* state *)
@@ -98,24 +81,9 @@
val browser_info = Synchronized.var "browser_info" empty_browser_info;
fun change_browser_info f = Synchronized.change browser_info (map_browser_info f);
-fun init_theory_info name info =
- change_browser_info (fn (theories, tex_index, html_index) =>
- (Symtab.update (name, info) theories, tex_index, html_index));
+fun update_html name html = change_browser_info (apfst (Symtab.update (name, html)));
-fun change_theory_info name f =
- change_browser_info (fn (theories, tex_index, html_index) =>
- (case Symtab.lookup theories name of
- NONE => error ("Browser info: cannot access theory document " ^ quote name)
- | SOME info => (Symtab.update (name, map_theory_info f info) theories, tex_index, html_index)));
-
-
-fun add_tex_index txt =
- change_browser_info (fn (theories, tex_index, html_index) =>
- (theories, txt :: tex_index, html_index));
-
-fun add_html_index txt =
- change_browser_info (fn (theories, tex_index, html_index) =>
- (theories, tex_index, txt :: html_index));
+fun add_html_index txt = change_browser_info (apsnd (cons txt));
@@ -125,15 +93,12 @@
type session_info =
{symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
- document: bool, doc_output: Path.T option, doc_files: (Path.T * Path.T) list,
- graph_file: Path.T, documents: (string * string) list, verbose: bool, readme: Path.T option};
+ verbose: bool, readme: Path.T option};
fun make_session_info
- (symbols, name, chapter, info_path, info, document, doc_output, doc_files,
- graph_file, documents, verbose, readme) =
+ (symbols, name, chapter, info_path, info, verbose, readme) =
{symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info,
- document = document, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
- documents = documents, verbose = verbose, readme = readme}: session_info;
+ verbose = verbose, readme = readme}: session_info;
(* state *)
@@ -152,89 +117,35 @@
(** document preparation **)
-(* options *)
-
-fun document_option options =
- (case Options.string options "document" of
- "" => {enabled = false, disabled = false}
- | "false" => {enabled = false, disabled = true}
- | _ => {enabled = true, disabled = false});
-
-fun document_variants options =
- let
- val variants =
- space_explode ":" (Options.string options "document_variants") |> map (fn s =>
- (case space_explode "=" s of
- [name] => (name, "")
- | [name, tags] => (name, tags)
- | _ => error ("Malformed document variant specification: " ^ quote s)));
- val _ =
- (case duplicates (op =) (map #1 variants) of
- [] => ()
- | dups => error ("Duplicate document variants: " ^ commas_quote dups));
- in variants end;
-
-
(* init session *)
-fun init symbols info info_path document document_output doc_variants doc_files graph_file
- (chapter, name) verbose =
+fun init symbols info info_path documents (chapter, name) verbose =
let
- val doc_output =
- if document_output = "" then NONE else SOME (Path.explode document_output);
-
- val documents = if not document orelse null doc_files then [] else doc_variants;
val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
val docs =
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
- map (fn (name, _) => (Url.File (document_path name), name)) documents;
+ map (fn name => (Url.File (document_path name), name)) documents;
in
session_info :=
- SOME (make_session_info (symbols, name, chapter, info_path, info, document,
- doc_output, doc_files, graph_file, documents, verbose, readme));
+ SOME (make_session_info (symbols, name, chapter, info_path, info, verbose, readme));
Synchronized.change browser_info (K empty_browser_info);
add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
end;
-(* isabelle tool wrappers *)
-
-fun isabelle_document {verbose} doc_name tags dir =
- let
- val script =
- "isabelle document -d " ^ File.bash_path dir ^ " -n " ^ Bash.string doc_name ^
- (if tags = "" then "" else " -t " ^ Bash.string tags);
- val doc_path = dir + Path.parent + document_path doc_name;
- val _ = if verbose then writeln script else ();
- val {out, err, rc, ...} = Bash.process script;
- val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
- val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
- in doc_path end;
-
-
(* finish session -- output all generated text *)
fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
-fun write_tex src name path =
- File.write_buffer (path + tex_path name) src;
-
-fun write_tex_index tex_index path =
- write_tex (index_buffer tex_index) doc_indexN path;
-
-fun finish () =
- with_session_info () (fn {name, chapter, info, info_path, doc_output, doc_files, graph_file,
- documents, verbose, readme, ...} =>
+fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} =>
let
- val {theories, tex_index, html_index} = Synchronized.value browser_info;
- val thys = Symtab.dest theories;
+ val {html_theories, html_index} = Synchronized.value browser_info;
val session_prefix = info_path + Path.basic chapter + Path.basic name;
- fun finish_html (a, {html_source, ...}: theory_info) =
- File.write (session_prefix + html_path a) html_source;
+ fun finish_html (a, html) = File.write (session_prefix + html_path a) html;
val _ =
if info then
@@ -242,45 +153,11 @@
File.write_buffer (session_prefix + index_path)
(index_buffer html_index |> Buffer.add HTML.end_document);
(case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
- List.app finish_html thys;
+ Symtab.fold (K o finish_html) html_theories ();
if verbose
then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
else ())
else ();
-
- fun document_job doc_prefix backdrop (doc_name, tags) =
- let
- val doc_dir = doc_prefix + Path.basic doc_name;
- fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
- val _ = purge ();
- val _ = Isabelle_System.make_directory doc_dir;
- val _ =
- Isabelle_System.bash ("isabelle latex -o sty " ^
- File.bash_path (doc_dir + Path.basic "root.tex"));
- val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
- val _ = Isabelle_System.copy_file graph_file (doc_dir + session_graph_path);
- val _ = write_tex_index tex_index doc_dir;
- val _ =
- List.app (fn (a, {tex_source, ...}) =>
- write_tex (fold Buffer.add tex_source Buffer.empty) a doc_dir) thys;
- in
- fn () =>
- (isabelle_document {verbose = true} doc_name tags doc_dir before purge (),
- fn doc =>
- if verbose orelse not backdrop then
- Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
- else ())
- end;
-
- val jobs =
- (if info orelse is_none doc_output then
- map (document_job session_prefix true) documents
- else []) @
- (case doc_output of
- NONE => []
- | SOME path => map (document_job path false) documents);
-
- val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>);
in
Synchronized.change browser_info (K empty_browser_info);
session_info := NONE
@@ -289,12 +166,6 @@
(* theory elements *)
-fun theory_output thy output =
- with_session_info () (fn _ =>
- if is_session_theory thy then
- (change_theory_info (Context.theory_name thy) o apfst) (K output)
- else ());
-
fun theory_link (curr_chapter, curr_session) thy =
let
val {chapter, name = session, ...} = Browser_Info.get thy;
@@ -316,13 +187,12 @@
Theory.parents_of thy |> map (fn parent =>
(Option.map Url.File (theory_link (chapter, session_name) parent),
(Context.theory_name parent)));
- val html_source = HTML.theory symbols name parent_specs (mk_text ());
- val _ = init_theory_info name (make_theory_info ([], html_source));
+
+ val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ()));
val bibtex_entries' =
if is_session_theory thy then
(add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
- add_tex_index (update_time, Latex.theory_entry name);
bibtex_entries)
else [];
in
--- a/src/Pure/Thy/present.scala Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Thy/present.scala Wed Nov 11 21:00:14 2020 +0100
@@ -77,9 +77,8 @@
/* finish session */
def finish(
- progress: Progress,
browser_info: Path,
- graph_file: JFile,
+ graph_pdf: Bytes,
info: Sessions.Info,
name: String)
{
@@ -89,9 +88,7 @@
if (info.options.bool("browser_info")) {
Isabelle_System.make_directory(session_fonts)
- val session_graph = session_prefix + Path.basic("session_graph.pdf")
- File.copy(graph_file, session_graph.file)
- Isabelle_System.chmod("a+r", session_graph)
+ Bytes.write(session_prefix + session_graph_path, graph_pdf)
HTML.write_isabelle_css(session_prefix)
@@ -193,131 +190,210 @@
- /** make document source **/
+ /** build documents **/
- def write_tex_index(dir: Path, names: List[Document.Node.Name])
- {
- val path = dir + Path.explode("session.tex")
- val text = names.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString
- File.write(path, text)
- }
-
-
+ val session_tex_path = Path.explode("session.tex")
+ val session_graph_path = Path.explode("session_graph.pdf")
- /** build document **/
-
- val document_format = "pdf"
+ def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
+ def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
- val default_document_name = "document"
- def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name)
-
- def document_tags(tags: List[String]): String =
- {
- cat_lines(
+ def isabelletags(tags: List[String]): String =
+ Library.terminate_lines(
tags.map(tag =>
tag.toList match {
case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
case cs => "\\isakeeptag{" + cs.mkString + "}"
- })) + "\n"
- }
+ }))
- def build_document(
- document_name: String = default_document_name,
- document_dir: Option[Path] = None,
- tags: List[String] = Nil)
+ def build_documents(
+ session: String,
+ deps: Sessions.Deps,
+ store: Sessions.Store,
+ progress: Progress = new Progress,
+ verbose: Boolean = false,
+ verbose_latex: Boolean = false): List[(String, Bytes)] =
{
- val document_target = Path.parent + Path.explode(document_name).ext(document_format)
+ /* session info */
+
+ val info = deps.sessions_structure(session)
+ val options = info.options
+ val base = deps(session)
+ val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
- val dir = document_dir getOrElse default_document_dir(document_name)
- if (!dir.is_dir) error("Bad document output directory " + dir)
+
+ /* prepare document directory */
+
+ def prepare_dir(dir: Path, doc_name: String, doc_tags: List[String]): (Path, String) =
+ {
+ val doc_dir = dir + Path.basic(doc_name)
+ Isabelle_System.make_directory(doc_dir)
- val root_name =
- {
- val root1 = "root_" + document_name
- if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root"
+ Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
+ File.write(doc_dir + Path.explode("isabelletags.sty"), isabelletags(doc_tags))
+ for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir)
+ Bytes.write(doc_dir + session_graph_path, graph_pdf)
+
+ File.write(doc_dir + session_tex_path,
+ Library.terminate_lines(
+ base.session_theories.map(name => "\\input{" + tex_name(name) + "}")))
+
+ using(store.open_database(session))(db =>
+ for (name <- base.session_theories) {
+ val tex =
+ Export.read_entry(db, session, name.theory, document_tex_name(name)) match {
+ case Some(entry) => entry.uncompressed(cache = store.xz_cache)
+ case None => Bytes.empty
+ }
+ Bytes.write(doc_dir + Path.basic(tex_name(name)), tex)
+ })
+
+ val root1 = "root_" + doc_name
+ val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root"
+
+ (doc_dir, root)
}
- /* bash scripts */
+ /* produce documents */
- def root_bash(ext: String): String = Bash.string(root_name + "." + ext)
+ val doc_output = info.document_output
- def latex_bash(fmt: String, ext: String = "tex"): String =
- "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
+ val docs =
+ for ((doc_name, doc_tags) <- info.documents)
+ yield {
+ Isabelle_System.with_tmp_dir("document")(tmp_dir =>
+ {
+ val (doc_dir, root) = prepare_dir(tmp_dir, doc_name, doc_tags)
+ doc_output.foreach(prepare_dir(_, doc_name, doc_tags))
+
- def bash(script: String): Process_Result =
- Isabelle_System.bash(script, cwd = dir.file)
+ // bash scripts
+
+ def root_bash(ext: String): String = Bash.string(root + "." + ext)
+
+ def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
+ "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
+
+ def bash(items: String*): Process_Result =
+ progress.bash(items.mkString(" && "), cwd = doc_dir.file, echo = verbose_latex)
- /* prepare document */
+ // prepare document
+
+ List("log", "blg").foreach(ext => (doc_dir + Path.explode(root).ext(ext)).file.delete)
- File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
-
- List("log", "blg").foreach(ext => (dir + Path.explode(root_name).ext(ext)).file.delete)
+ val result =
+ if ((doc_dir + Path.explode("build")).is_file) {
+ bash("./build pdf " + Bash.string(doc_name))
+ }
+ else {
+ bash(
+ latex_bash("sty"),
+ latex_bash(),
+ "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
+ "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
+ latex_bash(),
+ latex_bash())
+ }
- val result =
- if ((dir + Path.explode("build")).is_file) {
- bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name))
- }
- else {
- bash(
- List(
- latex_bash("sty"),
- latex_bash(document_format),
- "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
- "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
- latex_bash(document_format),
- latex_bash(document_format)).mkString(" && "))
+
+ // result
+
+ val root_pdf = Path.basic(root).pdf
+ val result_path = doc_dir + root_pdf
+
+ if (!result.ok) {
+ cat_error(
+ Library.trim_line(result.err),
+ cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
+ "Failed to build document " + quote(doc_name))
+ }
+ else if (!result_path.is_file) {
+ error("Bad document result: expected to find " + root_pdf)
+ }
+ else doc_name -> Bytes.read(result_path)
+ })
}
-
- /* result */
-
- if (!result.ok) {
- cat_error(
- Library.trim_line(result.err),
- cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)),
- "Failed to build document in " + File.path(dir.absolute_file))
+ def output(echo: Boolean, dir: Path)
+ {
+ Isabelle_System.make_directory(dir)
+ for ((name, pdf) <- docs) {
+ val path = dir + Path.basic(name).pdf
+ Bytes.write(path, pdf)
+ if (echo) progress.echo_document(path)
+ }
}
- bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " +
- root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check
+ if (info.options.bool("browser_info") || doc_output.isEmpty) {
+ output(verbose, store.browser_info + Path.basic(info.chapter) + Path.basic(session))
+ }
+
+ doc_output.foreach(output(true, _))
+
+ docs
}
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("document", "prepare theory session document", args =>
- {
- var document_dir: Option[Path] = None
- var document_name = default_document_name
- var tags: List[String] = Nil
+ Isabelle_Tool("document", "prepare session theory document", args =>
+ {
+ var verbose_latex = false
+ var dirs: List[Path] = Nil
+ var no_build = false
+ var options = Options.init()
+ var verbose_build = false
- val getopts = Getopts("""
-Usage: isabelle document [OPTIONS]
+ val getopts = Getopts(
+ """
+Usage: isabelle document [OPTIONS] SESSION
Options are:
- -d DIR document output directory (default """ +
- default_document_dir(default_document_name) + """)
- -n NAME document name (default """ + quote(default_document_name) + """)
- -t TAGS markup for tagged regions
+ -O set option "document_output", relative to current directory
+ -V verbose latex
+ -d DIR include session directory
+ -n no build of session
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose build
- Prepare the theory session document in document directory, producing the
- specified output format.
+ Prepare the theory document of a session.
""",
- "d:" -> (arg => document_dir = Some(Path.explode(arg))),
- "n:" -> (arg => document_name = arg),
- "t:" -> (arg => tags = space_explode(',', arg)))
+ "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
+ "V" -> (_ => verbose_latex = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "n" -> (_ => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose_build = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ val session =
+ more_args match {
+ case List(a) => a
+ case _ => getopts.usage()
+ }
+
+ val progress = new Console_Progress(verbose = verbose_build)
+ val store = Sessions.store(options)
- try {
- build_document(document_dir = document_dir, document_name = document_name, tags = tags)
- }
- catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) }
- })
+ progress.interrupt_handler {
+ if (!no_build) {
+ val res =
+ Build.build(options, selection = Sessions.Selection.session(session),
+ dirs = dirs, progress = progress, verbose = verbose_build)
+ if (!res.ok) error("Failed to build session " + quote(session))
+ }
+
+ val deps =
+ Sessions.load_structure(options + "document=pdf", dirs = dirs).
+ selection_deps(Sessions.Selection.session(session))
+
+ build_documents(session, deps, store, progress = progress,
+ verbose = true, verbose_latex = verbose_latex)
+ }
+ })
}
--- a/src/Pure/Thy/sessions.scala Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Nov 11 21:00:14 2020 +0100
@@ -452,6 +452,36 @@
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
+ def document_enabled: Boolean =
+ options.string("document") match {
+ case "" | "false" => false
+ case "pdf" => true
+ case doc => error("Bad document specification " + quote(doc))
+ }
+
+ def documents: List[(String, List[String])] =
+ {
+ val variants =
+ for (s <- Library.space_explode(':', options.string("document_variants")))
+ yield {
+ Library.space_explode('=', s) match {
+ case List(name) => (name, Nil)
+ case List(name, tags) => (name, Library.space_explode(',', tags))
+ case _ => error("Malformed document_variants: " + quote(s))
+ }
+ }
+ val dups = Library.duplicates(variants.map(_._1))
+ if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
+
+ if (!document_enabled || document_files.isEmpty) Nil else variants
+ }
+
+ def document_output: Option[Path] =
+ options.string("document_output") match {
+ case "" => None
+ case s => Some(dir + Path.explode(s))
+ }
+
def bibtex_entries: List[Text.Info[String]] =
(for {
(document_dir, file) <- document_files.iterator
@@ -714,7 +744,6 @@
def selection(session: String): Structure = selection(Selection.session(session))
def selection_deps(
- options: Options,
selection: Selection,
progress: Progress = new Progress,
loading_sessions: Boolean = false,
--- a/src/Pure/Thy/thy_info.ML Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Nov 11 21:00:14 2020 +0100
@@ -61,9 +61,8 @@
else
let
val body = Thy_Output.present_thy options thy segments;
- val option = Present.document_option options;
in
- if #disabled option then ()
+ if Options.string options "document" = "false" then ()
else
let
val thy_name = Context.theory_name thy;
@@ -71,9 +70,7 @@
val latex = Latex.isabelle_body thy_name body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
- val _ = Export.export thy (Path.binding0 document_path) (XML.blob output);
- val _ = if #enabled option then Present.theory_output thy output else ();
- in () end
+ in Export.export thy (Path.binding0 document_path) (XML.blob output) end
end));
--- a/src/Pure/Tools/build.ML Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Tools/build.ML Wed Nov 11 21:00:14 2020 +0100
@@ -89,9 +89,9 @@
(fn [args_yxml] =>
let
val (symbol_codes, (command_timings, (verbose, (browser_info,
- (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir,
+ (documents, (parent_name, (chapter, (session_name, (master_dir,
(theories, (session_positions, (session_directories, (doc_names, (global_theories,
- (loaded_theories, bibtex_entries)))))))))))))))) =
+ (loaded_theories, bibtex_entries))))))))))))))) =
YXML.parse_body args_yxml |>
let
open XML.Decode;
@@ -99,12 +99,12 @@
val path = Path.explode o string;
in
pair (list (pair string int)) (pair (list properties) (pair bool (pair path
- (pair (list (pair path path)) (pair path (pair string (pair string (pair string
+ (pair (list string) (pair string (pair string (pair string
(pair path
(pair (((list (pair Options.decode (list (pair string position))))))
(pair (list (pair string properties))
(pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
+ (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))
end;
val symbols = HTML.make_symbols symbol_codes;
@@ -124,11 +124,7 @@
symbols
(Options.default_bool "browser_info")
browser_info
- (Options.default_string "document")
- (Options.default_string "document_output")
- (Present.document_variants (Options.default ()))
- document_files
- graph_file
+ documents
parent_name
(chapter, session_name)
verbose;
--- a/src/Pure/Tools/build.scala Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 11 21:00:14 2020 +0100
@@ -165,12 +165,7 @@
val options: Options = NUMA.policy_options(info.options, numa_node)
private val sessions_structure = deps.sessions_structure
-
- private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
- graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
-
- private val export_consumer =
- Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
+ private val documents = info.documents.map(_._1)
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
@@ -180,22 +175,20 @@
YXML.string_of_body(
{
import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(bool,
- pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
- pair(string, pair(string, pair(string, pair(Path.encode,
+ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode,
+ pair(list(string), pair(string, pair(string, pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(pair(string, properties)))),
pair(list(pair(string, properties)),
pair(list(pair(string, string)),
pair(list(string), pair(list(pair(string, string)),
- pair(list(string), list(string)))))))))))))))))(
- (Symbol.codes, (command_timings0, (verbose,
- (store.browser_info, (info.document_files, (File.standard_path(graph_file),
- (parent, (info.chapter, (session_name, (Path.current,
+ pair(list(string), list(string))))))))))))))))(
+ (Symbol.codes, (command_timings0, (verbose, (store.browser_info,
+ (documents, (parent, (info.chapter, (session_name, (Path.current,
(info.theories,
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(base.doc_names, (base.global_theories.toList,
- (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))))
+ (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))
})
val env =
@@ -234,6 +227,9 @@
}
}
+ val export_consumer =
+ Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
+
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
val messages = new mutable.ListBuffer[XML.Elem]
@@ -242,6 +238,7 @@
val session_timings = new mutable.ListBuffer[Properties.T]
val runtime_statistics = new mutable.ListBuffer[Properties.T]
val task_statistics = new mutable.ListBuffer[Properties.T]
+ val document_output = new mutable.ListBuffer[String]
def fun(
name: String,
@@ -355,7 +352,7 @@
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
- val errors =
+ val build_errors =
Isabelle_Thread.interrupt_handler(_ => process.terminate) {
Exn.capture { process.await_startup } match {
case Exn.Res(_) =>
@@ -367,25 +364,58 @@
val process_result =
Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
- val process_output =
- stdout.toString ::
- messages.toList.map(message =>
- Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
- command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
- theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
- session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
- runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
- task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
+
+ val export_errors =
+ export_consumer.shutdown(close = true).map(Output.error_message_text)
+
+ val document_errors =
+ try {
+ if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && documents.nonEmpty) {
+ val document_progress =
+ new Progress {
+ override def echo(msg: String): Unit =
+ document_output.synchronized { document_output += msg }
+ override def echo_document(path: Path): Unit =
+ progress.echo_document(path)
+ }
+ Present.build_documents(session_name, deps, store, verbose = verbose,
+ verbose_latex = true, progress = document_progress)
+ }
+ val graph_pdf =
+ graphview.Graph_File.make_pdf(options, deps(session_name).session_graph_display)
+ Present.finish(store.browser_info, graph_pdf, info, session_name)
+ Nil
+ }
+ catch { case ERROR(msg) => List(msg) case e@Exn.Interrupt() => List(Exn.message(e)) }
val result =
- process_result.output(process_output).error(Library.trim_line(stderr.toString))
+ {
+ val more_output =
+ Library.trim_line(stdout.toString) ::
+ messages.toList.map(message =>
+ Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
+ command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
+ theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
+ session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
+ runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
+ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
+ document_output.toList
- errors match {
- case Exn.Res(Nil) => result
- case Exn.Res(errs) =>
- result.error_rc.output(
- errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
- errs.map(Protocol.Error_Message_Marker.apply))
+ val more_errors =
+ Library.trim_line(stderr.toString) :: export_errors ::: document_errors
+
+ process_result.output(more_output).errors(more_errors)
+ }
+
+ build_errors match {
+ case Exn.Res(build_errs) =>
+ val errs = build_errs ::: document_errors
+ if (errs.isEmpty) result
+ else {
+ result.error_rc.output(
+ errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
+ errs.map(Protocol.Error_Message_Marker.apply))
+ }
case Exn.Exn(Exn.Interrupt()) =>
if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
case Exn.Exn(exn) => throw exn
@@ -404,23 +434,7 @@
def join: (Process_Result, Option[String]) =
{
- val result0 = future_result.join
- val result1 =
- export_consumer.shutdown(close = true).map(Output.error_message_text) match {
- case Nil => result0
- case errs => result0.errors(errs).error_rc
- }
-
- if (result1.ok) {
- for (document_output <- proper_string(options.string("document_output"))) {
- val document_output_dir =
- Isabelle_System.make_directory(info.dir + Path.explode(document_output))
- Present.write_tex_index(document_output_dir, deps(session_name).session_theories)
- }
- Present.finish(progress, store.browser_info, graph_file, info, session_name)
- }
-
- graph_file.delete
+ val result1 = future_result.join
val was_timeout =
timeout_request match {