# HG changeset patch
# User wenzelm
# Date 1422220266 -3600
# Node ID 4427f04fca57ea90f7fd8dbc271ac29a9268ec75
# Parent  2c27c3d1fd3bd84386c03b58df378e64e4083ad4
discontinued obsolete option "document_graph";

diff -r 2c27c3d1fd3b -r 4427f04fca57 NEWS
--- 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
diff -r 2c27c3d1fd3b -r 4427f04fca57 etc/options
--- 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"
diff -r 2c27c3d1fd3b -r 4427f04fca57 src/Doc/System/Sessions.thy
--- 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
diff -r 2c27c3d1fd3b -r 4427f04fca57 src/HOL/ROOT
--- 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"
diff -r 2c27c3d1fd3b -r 4427f04fca57 src/Pure/PIDE/session.ML
--- 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;
 
diff -r 2c27c3d1fd3b -r 4427f04fca57 src/Pure/Thy/present.ML
--- 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;
diff -r 2c27c3d1fd3b -r 4427f04fca57 src/Pure/Tools/build.ML
--- 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)
diff -r 2c27c3d1fd3b -r 4427f04fca57 src/ZF/ROOT
--- 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 +