--- a/NEWS Sun Jan 25 21:46:21 2015 +0100
+++ b/NEWS Sun Jan 25 22:11:06 2015 +0100
@@ -203,6 +203,9 @@
*** Document preparation ***
+* Discontinued obsolete option "document_graph": session_graph.pdf is
+produced unconditionally.
+
* Document markup commands 'chapter', 'section', 'subsection',
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
context, even before the initial 'theory' command. Obsolete proof
--- a/etc/options Sun Jan 25 21:46:21 2015 +0100
+++ b/etc/options Sun Jan 25 22:11:06 2015 +0100
@@ -11,8 +11,6 @@
-- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
option document_variants : string = "document"
-- "option alternative document variants (separated by colons)"
-option document_graph : bool = false
- -- "generate session graph image for document"
option thy_output_display : bool = false
-- "indicate output as multi-line display-style material"
--- a/src/Doc/System/Sessions.thy Sun Jan 25 21:46:21 2015 +0100
+++ b/src/Doc/System/Sessions.thy Sun Jan 25 22:11:06 2015 +0100
@@ -203,15 +203,6 @@
different document root entries, see also
\secref{sec:tool-document}.
- \item @{system_option_def "document_graph"} tells whether the
- generated document files should include a theory graph (cf.\
- \secref{sec:browse} and \secref{sec:info}). The resulting EPS or
- PDF file can be included as graphics in {\LaTeX}.
-
- Note that this option is usually determined as static parameter of
- some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
- given globally or on the command line of @{tool build}.
-
\item @{system_option_def "threads"} determines the number of worker
threads for parallel checking of theories and proofs. The default
@{text "0"} means that a sensible maximum value is determined by the
--- a/src/HOL/ROOT Sun Jan 25 21:46:21 2015 +0100
+++ b/src/HOL/ROOT Sun Jan 25 22:11:06 2015 +0100
@@ -4,7 +4,6 @@
description {*
Classical Higher-order Logic.
*}
- options [document_graph]
global_theories
Main
Complex_Main
@@ -74,7 +73,6 @@
subspaces (not only one-dimensional subspaces), can be extended to a
continous linearform on the whole vectorspace.
*}
- options [document_graph]
theories Hahn_Banach
document_files "root.bib" "root.tex"
@@ -114,7 +112,7 @@
document_files "root.tex"
session "HOL-IMP" in IMP = HOL +
- options [document_graph, document_variants=document]
+ options [document_variants = document]
theories [document = false]
"~~/src/Tools/Permanent_Interpretation"
"~~/src/HOL/Library/While_Combinator"
@@ -171,7 +169,6 @@
theories EvenOdd
session "HOL-Import" in Import = HOL +
- options [document_graph]
theories HOL_Light_Maps
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
@@ -180,7 +177,6 @@
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
*}
- options [document_graph]
theories [document = false]
"~~/src/HOL/Library/FuncSet"
"~~/src/HOL/Library/Multiset"
@@ -199,7 +195,6 @@
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
Theorem, Wilson's Theorem, Quadratic Reciprocity.
*}
- options [document_graph]
theories [document = false]
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Library/Permutation"
@@ -229,12 +224,11 @@
Verification of shared-variable imperative programs a la Owicki-Gries.
(verification conditions are generated automatically).
*}
- options [document_graph]
theories Hoare_Parallel
document_files "root.bib" "root.tex"
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
- options [document = false, document_graph = false, browser_info = false]
+ options [document = false, browser_info = false]
theories
Generate
Generate_Binary_Nat
@@ -287,7 +281,6 @@
The Isabelle Algebraic Library.
*}
- options [document_graph]
theories [document = false]
(* Preliminaries from set and number theory *)
"~~/src/HOL/Library/FuncSet"
@@ -311,7 +304,6 @@
description {*
A new approach to verifying authentication protocols.
*}
- options [document_graph]
theories
Auth_Shared
Auth_Public
@@ -327,7 +319,6 @@
Verifying security protocols using Chandy and Misra's UNITY formalism.
*}
- options [document_graph]
theories
(*Basic meta-theory*)
"UNITY_Main"
@@ -375,7 +366,7 @@
document_files "root.tex"
session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
- options [document_graph, print_mode = "iff,no_brackets"]
+ options [print_mode = "iff,no_brackets"]
theories [document = false]
"~~/src/HOL/Library/Countable"
"~~/src/HOL/Library/Monad_Syntax"
@@ -425,8 +416,7 @@
The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
*}
- options [document_graph, print_mode = "no_brackets", parallel_proofs = 0,
- quick_and_dirty = false]
+ options [print_mode = "no_brackets", parallel_proofs = 0, quick_and_dirty = false]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Int"
theories
@@ -455,9 +445,10 @@
machine and a specification of its bytecode verifier and a lightweight
bytecode verifier, including proofs of type-safety.
*}
- options [document_graph]
- theories [document = false] "~~/src/HOL/Library/While_Combinator"
- theories MicroJava
+ theories [document = false]
+ "~~/src/HOL/Library/While_Combinator"
+ theories
+ MicroJava
document_files
"introduction.tex"
"root.bib"
@@ -467,12 +458,10 @@
description {*
Hoare Logic for a tiny fragment of Java.
*}
- options [document_graph]
theories Example
document_files "root.bib" "root.tex"
session "HOL-Bali" in Bali = HOL +
- options [document_graph]
theories
AxExample
AxSound
@@ -646,7 +635,6 @@
description {*
Verification of the SET Protocol.
*}
- options [document_graph]
theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
theories SET_Protocol
document_files "root.tex"
@@ -655,7 +643,6 @@
description {*
Two-dimensional matrices and linear programming.
*}
- options [document_graph]
theories Cplex
document_files "root.tex"
@@ -697,7 +684,6 @@
ATP_Problem_Import
session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
- options [document_graph]
theories
Multivariate_Analysis
Determinants
@@ -707,7 +693,6 @@
"root.tex"
session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
- options [document_graph]
theories [document = false]
"~~/src/HOL/Library/Countable"
"~~/src/HOL/Library/Permutation"
@@ -786,7 +771,6 @@
Misc_N2M
session "HOL-Word" (main) in Word = HOL +
- options [document_graph]
theories Word
document_files "root.bib" "root.tex"
@@ -803,7 +787,6 @@
description {*
Nonstandard analysis.
*}
- options [document_graph]
theories Hypercomplex
document_files "root.tex"
@@ -994,7 +977,6 @@
HOLCF -- a semantic extension of HOL by the LCF logic.
*}
- options [document_graph]
theories [document = false]
"~~/src/HOL/Library/Nat_Bijection"
"~~/src/HOL/Library/Countable"
--- a/src/Pure/PIDE/session.ML Sun Jan 25 21:46:21 2015 +0100
+++ b/src/Pure/PIDE/session.ML Sun Jan 25 22:11:06 2015 +0100
@@ -9,7 +9,7 @@
val name: unit -> string
val welcome: unit -> string
val get_keywords: unit -> Keyword.keywords
- val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+ val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
(Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
val shutdown: unit -> unit
val finish: unit -> unit
@@ -42,7 +42,7 @@
(* init *)
-fun init build info info_path doc doc_graph doc_output doc_variants doc_files graph_file
+fun init build info info_path doc doc_output doc_variants doc_files graph_file
parent (chapter, name) verbose =
if #name (! session) <> parent orelse not (! session_finished) then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
@@ -52,7 +52,7 @@
val _ = session_finished := false;
in
Present.init build info info_path (if doc = "false" then "" else doc)
- doc_graph doc_output doc_variants doc_files graph_file (chapter, name)
+ doc_output doc_variants doc_files graph_file (chapter, name)
verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
end;
--- a/src/Pure/Thy/present.ML Sun Jan 25 21:46:21 2015 +0100
+++ b/src/Pure/Thy/present.ML Sun Jan 25 22:11:06 2015 +0100
@@ -9,7 +9,7 @@
val session_name: theory -> string
val document_enabled: string -> bool
val document_variants: string -> (string * string) list
- val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+ val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> theory list -> unit
val finish: unit -> unit
val theory_output: string -> string -> unit
@@ -160,18 +160,16 @@
(* session_info *)
type session_info =
- {name: string, chapter: string, info_path: Path.T, info: bool,
- doc_format: string, doc_graph: 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};
+ {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string,
+ 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};
fun make_session_info
- (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
- doc_files, graph_file, documents, verbose, readme) =
- {name = name, chapter = chapter, info_path = info_path, info = info,
- doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
- doc_files = doc_files, graph_file = graph_file, documents = documents,
- verbose = verbose, readme = readme}: session_info;
+ (name, chapter, info_path, info, doc_format, doc_output, doc_files,
+ graph_file, documents, verbose, readme) =
+ {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format,
+ doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
+ documents = documents, verbose = verbose, readme = readme}: session_info;
(* state *)
@@ -205,7 +203,7 @@
(* init session *)
-fun init build info info_path doc doc_graph document_output doc_variants doc_files graph_file
+fun init build info info_path doc document_output doc_variants doc_files graph_file
(chapter, name) verbose thys =
if not build andalso not info andalso doc = "" then
(Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
@@ -229,7 +227,7 @@
in
session_info :=
SOME (make_session_info (name, chapter, info_path, info, doc,
- doc_graph, doc_output, doc_files, graph_file, documents, verbose, readme));
+ doc_output, doc_files, graph_file, documents, verbose, readme));
Synchronized.change browser_info (K (init_browser_info (chapter, name) thys));
add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
end;
@@ -264,7 +262,7 @@
write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
fun finish () =
- with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
+ with_session_info () (fn {name, chapter, info, info_path, doc_format,
doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
let
val {theories, tex_index, html_index, graph} = Synchronized.value browser_info;
--- a/src/Pure/Tools/build.ML Sun Jan 25 21:46:21 2015 +0100
+++ b/src/Pure/Tools/build.ML Sun Jan 25 22:11:06 2015 +0100
@@ -140,7 +140,6 @@
(Options.bool options "browser_info")
(Path.explode browser_info)
(Options.string options "document")
- (Options.bool options "document_graph")
(Options.string options "document_output")
(Present.document_variants (Options.string options "document_variants"))
(map (apply2 Path.explode) document_files)
--- a/src/ZF/ROOT Sun Jan 25 21:46:21 2015 +0100
+++ b/src/ZF/ROOT Sun Jan 25 22:11:06 2015 +0100
@@ -42,7 +42,6 @@
Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
(North-Holland, 1980)
*}
- options [document_graph]
theories
Main
Main_ZFC
@@ -63,7 +62,6 @@
"Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
development and ZF's theories of cardinals.
*}
- options [document_graph]
theories
WO6_WO1
WO1_WO7
@@ -123,8 +121,10 @@
A paper describing this development is
http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
*}
- options [document_graph]
- theories DPow_absolute AC_in_L Rank_Separation
+ theories
+ DPow_absolute
+ AC_in_L
+ Rank_Separation
document_files "root.tex" "root.bib"
session "ZF-IMP" in IMP = ZF +