more robust: ensure coherence wrt. build database;
--- a/src/Doc/System/Presentation.thy Wed Nov 18 15:36:41 2020 +0100
+++ b/src/Doc/System/Presentation.thy Wed Nov 18 15:41:02 2020 +0100
@@ -133,17 +133,16 @@
-P DIR enable HTML/PDF presentation in directory (":" for default)
-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 document of a session.\<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).
+ @{tool_ref build} is invoked beforehand to ensure that it is up-to-date.
+ 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> Options \<^verbatim>\<open>-P\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool
build}.
--- a/src/Pure/Thy/present.scala Wed Nov 18 15:36:41 2020 +0100
+++ b/src/Pure/Thy/present.scala Wed Nov 18 15:41:02 2020 +0100
@@ -437,7 +437,6 @@
var presentation = Present.Context.none
var verbose_latex = false
var dirs: List[Path] = Nil
- var no_build = false
var options = Options.init()
var verbose_build = false
@@ -450,7 +449,6 @@
-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
@@ -460,7 +458,6 @@
"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))
@@ -475,12 +472,10 @@
val store = Sessions.store(options)
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 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).