--- a/NEWS Mon Oct 30 17:20:56 2017 +0000
+++ b/NEWS Mon Oct 30 20:27:25 2017 +0100
@@ -69,6 +69,10 @@
*** System ***
+* Session ROOT entry: empty 'document_files' means there is no document
+for this session. There is no need to specify options [document = false]
+anymore.
+
* Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
support has been discontinued.
--- a/lib/Tools/mkroot Mon Oct 30 17:20:56 2017 +0000
+++ b/lib/Tools/mkroot Mon Oct 30 20:27:25 2017 +0100
@@ -101,7 +101,6 @@
else
cat > "$DIR/ROOT" <<EOF
session "$NAME" = "$ISABELLE_LOGIC" +
- options [document = false]
theories
(* Foo *)
(* Bar *)
--- a/src/Benchmarks/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Benchmarks/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -4,7 +4,6 @@
description {*
Big (co)datatypes.
*}
- options [document = false]
theories
Brackin
IsaFoR
@@ -21,6 +20,5 @@
description {*
Big records.
*}
- options [document = false]
theories
Record_Benchmark
--- a/src/CCL/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/CCL/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -10,7 +10,6 @@
A computational logic for an untyped functional language with
evaluation to weak head-normal form.
*}
- options [document = false]
sessions
FOL
theories
@@ -22,4 +21,3 @@
"ex/List"
"ex/Stream"
"ex/Flag"
-
--- a/src/Cube/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Cube/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -13,6 +13,4 @@
For more information about the Lambda-Cube, see H. Barendregt, Introduction
to Generalised Type Systems, J. Functional Programming.
*}
- options [document = false]
theories Example
-
--- a/src/Doc/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Doc/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -17,7 +17,6 @@
"style.sty"
session Codegen_Basics in "Codegen" = "HOL-Library" +
- options [document = false]
theories
Setup
@@ -505,6 +504,5 @@
"style.sty"
session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
- options [document = false]
theories
Setup
--- a/src/Doc/System/Environment.thy Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Doc/System/Environment.thy Mon Oct 30 20:27:25 2017 +0100
@@ -255,8 +255,8 @@
"$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
\<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
- directory). For example: @{verbatim [display] \<open>init_component
- "$HOME/screwdriver-2.0"\<close>}
+ directory). For example:
+ @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
This is tolerant wrt.\ missing component directories, but might produce a
warning.
--- a/src/FOLP/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/FOLP/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -9,7 +9,6 @@
Presence of unknown proof term means that matching does not behave as expected.
*}
- options [document = false]
theories
IFOLP (global)
FOLP (global)
@@ -21,7 +20,6 @@
Examples for First-Order Logic.
*}
- options [document = false]
theories
Intro
Nat
@@ -33,4 +31,3 @@
Quantifiers_Int
Propositional_Cla
Quantifiers_Cla
-
--- a/src/HOL/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/HOL/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -15,7 +15,7 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
+ options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
sessions
"HOL-Library"
theories
@@ -177,7 +177,6 @@
procedures. For documentation see "Hoare Logic for Mutual Recursion and
Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
*}
- options [document = false]
theories EvenOdd
session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
@@ -233,7 +232,7 @@
document_files "root.bib" "root.tex"
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
- options [document = false, browser_info = false]
+ options [browser_info = false]
sessions
"HOL-Data_Structures"
"HOL-ex"
@@ -261,7 +260,6 @@
Testing Metis and Sledgehammer.
*}
- options [document = false]
sessions
"HOL-Decision_Procs"
theories
@@ -280,7 +278,6 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
*}
- options [document = false]
theories [quick_and_dirty] Nitpick_Examples
session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
@@ -384,12 +381,10 @@
description {*
Various decision procedures, typically involving reflection.
*}
- options [document = false]
theories
Decision_Procs
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
- options [document = false]
sessions
"HOL-Isar_Examples"
theories
@@ -443,7 +438,6 @@
including some minimal examples (in Test.thy) and a more typical example of
a little functional language and its type system.
*}
- options [document = false]
theories Test Type
session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
@@ -505,7 +499,6 @@
year=1995}
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
*}
- options [document = false]
theories Solve
session "HOL-Lattice" in Lattice = HOL +
@@ -521,7 +514,6 @@
description {*
Miscellaneous examples for Higher-Order Logic.
*}
- options [document = false]
theories
Adhoc_Overloading_Examples
Antiquote
@@ -667,19 +659,15 @@
description {*
Lamport's Temporal Logic of Actions.
*}
- options [document = false]
theories TLA
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
- options [document = false]
theories Inc
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
- options [document = false]
theories DBuffer
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
- options [document = false]
theories MemoryImplementation
session "HOL-TPTP" in TPTP = "HOL-Library" +
@@ -690,7 +678,6 @@
TPTP-related extensions.
*}
- options [document = false]
theories
ATP_Theory_Export
MaSh_Eval
@@ -712,12 +699,10 @@
Measure_Not_CCC
session "HOL-Nominal" in Nominal = "HOL-Library" +
- options [document = false]
theories
Nominal
session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
- options [document = false]
theories
Class3
CK_Machine
@@ -758,7 +743,6 @@
description {*
(Co)datatype Examples.
*}
- options [document = false]
theories
Compat
Lambda_Term
@@ -779,7 +763,6 @@
description {*
Corecursion Examples.
*}
- options [document = false]
theories
LFilter
Paper_Examples
@@ -807,7 +790,6 @@
document_files "root.bib" "root.tex"
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
- options [document = false]
theories WordExamples
session "HOL-Statespace" in Statespace = HOL +
@@ -824,20 +806,18 @@
document_files "root.tex"
session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
- options [document = false]
theories
NSPrimes
session "HOL-Mirabelle" in Mirabelle = HOL +
- options [document = false]
theories Mirabelle_Test
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
- options [document = false, timeout = 60]
+ options [timeout = 60]
theories Ex
session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
- options [document = false, quick_and_dirty]
+ options [quick_and_dirty]
theories
Boogie
SMT_Examples
@@ -845,12 +825,11 @@
SMT_Tests
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
- options [document = false]
theories
SPARK (global)
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
- options [document = false, spark_prv = false]
+ options [spark_prv = false]
theories
"Gcd/Greatest_Common_Divisor"
"Liseq/Longest_Increasing_Subsequence"
@@ -889,11 +868,9 @@
"Simple_Gcd.ads"
session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
- options [document = false]
theories MutabelleExtra
session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
- options [document = false]
theories
Quickcheck_Examples
Quickcheck_Lattice_Examples
@@ -908,7 +885,6 @@
description {*
Author: Cezary Kaliszyk and Christian Urban
*}
- options [document = false]
theories
DList
Quotient_FSet
@@ -923,7 +899,6 @@
Lifting_Code_Dt_Test
session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
- options [document = false]
theories
Examples
Predicate_Compile_Tests
@@ -948,7 +923,6 @@
description {*
Experimental extension of Higher-Order Logic to allow translation of types to sets.
*}
- options [document = false]
theories
Types_To_Sets
"Examples/Prerequisites"
@@ -974,7 +948,6 @@
document_files "root.tex"
session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
- options [document = false]
theories
HOLCF_Library
HOL_Cpo
@@ -985,18 +958,19 @@
This is the HOLCF-based denotational semantics of a simple WHILE-language.
*}
- options [document = false]
sessions
"HOL-IMP"
theories
HoareEx
- document_files "root.tex"
+ document_files
+ "isaverbatimwrite.sty"
+ "root.tex"
+ "root.bib"
session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
description {*
Miscellaneous examples for HOLCF.
*}
- options [document = false]
theories
Dnat
Dagstuhl
@@ -1025,7 +999,6 @@
"Specification and Development of Interactive Systems: Focus on Streams,
Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
*}
- options [document = false]
theories
Fstreams
FOCUS
@@ -1042,7 +1015,6 @@
abstraction theory. Everything is based upon a domain-theoretic model of
finite and infinite sequences.
*}
- options [document = false]
theories Abstraction
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
@@ -1051,7 +1023,6 @@
The Alternating Bit Protocol performed in I/O-Automata.
*}
- options [document = false]
theories
Correctness
Spec
@@ -1063,7 +1034,6 @@
A network transmission protocol, performed in the
I/O automata formalization by Olaf Mueller.
*}
- options [document = false]
theories Correctness
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
@@ -1072,14 +1042,12 @@
Memory storage case study.
*}
- options [document = false]
theories Correctness
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
description {*
Author: Olaf Mueller
*}
- options [document = false]
theories
TrivEx
TrivEx2
--- a/src/LCF/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/LCF/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -10,7 +10,6 @@
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
*}
- options [document = false]
sessions
FOL
theories
@@ -21,4 +20,3 @@
"ex/Ex2"
"ex/Ex3"
"ex/Ex4"
-
--- a/src/Pure/Admin/build_log.scala Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Pure/Admin/build_log.scala Mon Oct 30 20:27:25 2017 +0100
@@ -649,6 +649,10 @@
ml_statistics: List[Properties.T],
task_statistics: List[Properties.T],
errors: List[String])
+ {
+ def error(s: String): Session_Info =
+ copy(errors = errors ::: List(s))
+ }
private def parse_session_info(
log_file: Log_File,
--- a/src/Pure/PIDE/markup.scala Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Pure/PIDE/markup.scala Mon Oct 30 20:27:25 2017 +0100
@@ -392,13 +392,6 @@
}
- /* protocol functions */
-
- val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
-
- val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
-
-
/* command indentation */
object Command_Indent
@@ -506,6 +499,9 @@
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
+ val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
+ val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
+
val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
--- a/src/Pure/Thy/present.ML Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Pure/Thy/present.ML Mon Oct 30 20:27:25 2017 +0100
@@ -171,13 +171,7 @@
val doc_output =
if document_output = "" then NONE else SOME (Path.explode document_output);
- val documents =
- if doc = "" then []
- else if null doc_files andalso not (can File.check_dir document_path) then
- (if verbose then Output.physical_stderr "Warning: missing document directory\n"
- else (); [])
- else doc_variants;
-
+ val documents = if doc = "" 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 =
--- a/src/Pure/Tools/build.scala Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Pure/Tools/build.scala Mon Oct 30 20:27:25 2017 +0100
@@ -298,11 +298,10 @@
def terminate: Unit = future_result.cancel
def is_finished: Boolean = future_result.is_finished
- @volatile private var was_timeout = false
private val timeout_request: Option[Event_Timer.Request] =
{
if (info.timeout > Time.zero)
- Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
+ Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
else None
}
@@ -314,7 +313,12 @@
Present.finish(progress, store.browser_info, graph_file, info, name)
graph_file.delete
- timeout_request.foreach(_.cancel)
+
+ val was_timeout =
+ timeout_request match {
+ case None => false
+ case Some(request) => !request.cancel
+ }
if (result.interrupted) {
if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
@@ -532,15 +536,18 @@
val database = store.output_dir + store.database(name)
database.file.delete
+ val build_log =
+ Build_Log.Log_File(name, process_result.out_lines).
+ parse_session_info(
+ command_timings = true,
+ theory_timings = true,
+ ml_statistics = true,
+ task_statistics = true)
+
using(SQLite.open_database(database))(db =>
store.write_session_info(db, name,
build_log =
- Build_Log.Log_File(name, process_result.out_lines).
- parse_session_info(
- command_timings = true,
- theory_timings = true,
- ml_statistics = true,
- task_statistics = true),
+ if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
process_result.rc)))
--- a/src/Sequents/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/Sequents/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -37,7 +37,6 @@
S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
of Cambridge Computer Lab, 1995, ed L. Paulson)
*}
- options [document = false]
theories
LK
ILL
@@ -53,4 +52,3 @@
"LK/Quantifiers"
"LK/Hard_Quantifiers"
"LK/Nat"
-
--- a/src/ZF/ROOT Mon Oct 30 17:20:56 2017 +0000
+++ b/src/ZF/ROOT Mon Oct 30 20:27:25 2017 +0100
@@ -100,7 +100,6 @@
Report, Computer Lab, University of Cambridge (1995).
http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
*}
- options [document = false]
theories ECR
session "ZF-Constructible" in Constructible = ZF +
@@ -198,7 +197,6 @@
Porting Experiment.
http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
*}
- options [document = false]
theories Confluence
session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
@@ -208,7 +206,6 @@
ZF/UNITY proofs.
*}
- options [document = false]
theories
(*Simple examples: no composition*)
Mutex
@@ -235,7 +232,6 @@
href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
describes the package that automates their declaration.
*}
- options [document = false]
theories
misc
Ring (*abstract algebra*)