# HG changeset patch
# User wenzelm
# Date 1605710462 -3600
# Node ID 787ba1d19d3a57c90e46e8a133ac99a59335e1fe
# Parent  4ba5b1b08dd5d8f5e7029e3fdb872de8c6f99695
more robust: ensure coherence wrt. build database;

diff -r 4ba5b1b08dd5 -r 787ba1d19d3a src/Doc/System/Presentation.thy
--- 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}.
diff -r 4ba5b1b08dd5 -r 787ba1d19d3a src/Pure/Thy/present.scala
--- 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).