discontinued obsolete option "document_graph";
authorwenzelm
Sun Jan 25 22:11:06 2015 +0100 (2015-01-25)
changeset 594464427f04fca57
parent 59445 2c27c3d1fd3b
child 59447 e7cbfe240078
discontinued obsolete option "document_graph";
NEWS
etc/options
src/Doc/System/Sessions.thy
src/HOL/ROOT
src/Pure/PIDE/session.ML
src/Pure/Thy/present.ML
src/Pure/Tools/build.ML
src/ZF/ROOT
     1.1 --- a/NEWS	Sun Jan 25 21:46:21 2015 +0100
     1.2 +++ b/NEWS	Sun Jan 25 22:11:06 2015 +0100
     1.3 @@ -203,6 +203,9 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 +* Discontinued obsolete option "document_graph": session_graph.pdf is
     1.8 +produced unconditionally.
     1.9 +
    1.10  * Document markup commands 'chapter', 'section', 'subsection',
    1.11  'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
    1.12  context, even before the initial 'theory' command. Obsolete proof
     2.1 --- a/etc/options	Sun Jan 25 21:46:21 2015 +0100
     2.2 +++ b/etc/options	Sun Jan 25 22:11:06 2015 +0100
     2.3 @@ -11,8 +11,6 @@
     2.4    -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
     2.5  option document_variants : string = "document"
     2.6    -- "option alternative document variants (separated by colons)"
     2.7 -option document_graph : bool = false
     2.8 -  -- "generate session graph image for document"
     2.9  
    2.10  option thy_output_display : bool = false
    2.11    -- "indicate output as multi-line display-style material"
     3.1 --- a/src/Doc/System/Sessions.thy	Sun Jan 25 21:46:21 2015 +0100
     3.2 +++ b/src/Doc/System/Sessions.thy	Sun Jan 25 22:11:06 2015 +0100
     3.3 @@ -203,15 +203,6 @@
     3.4    different document root entries, see also
     3.5    \secref{sec:tool-document}.
     3.6  
     3.7 -  \item @{system_option_def "document_graph"} tells whether the
     3.8 -  generated document files should include a theory graph (cf.\
     3.9 -  \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or
    3.10 -  PDF file can be included as graphics in {\LaTeX}.
    3.11 -
    3.12 -  Note that this option is usually determined as static parameter of
    3.13 -  some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
    3.14 -  given globally or on the command line of @{tool build}.
    3.15 -
    3.16    \item @{system_option_def "threads"} determines the number of worker
    3.17    threads for parallel checking of theories and proofs.  The default
    3.18    @{text "0"} means that a sensible maximum value is determined by the
     4.1 --- a/src/HOL/ROOT	Sun Jan 25 21:46:21 2015 +0100
     4.2 +++ b/src/HOL/ROOT	Sun Jan 25 22:11:06 2015 +0100
     4.3 @@ -4,7 +4,6 @@
     4.4    description {*
     4.5      Classical Higher-order Logic.
     4.6    *}
     4.7 -  options [document_graph]
     4.8    global_theories
     4.9      Main
    4.10      Complex_Main
    4.11 @@ -74,7 +73,6 @@
    4.12      subspaces (not only one-dimensional subspaces), can be extended to a
    4.13      continous linearform on the whole vectorspace.
    4.14    *}
    4.15 -  options [document_graph]
    4.16    theories Hahn_Banach
    4.17    document_files "root.bib" "root.tex"
    4.18  
    4.19 @@ -114,7 +112,7 @@
    4.20    document_files "root.tex"
    4.21  
    4.22  session "HOL-IMP" in IMP = HOL +
    4.23 -  options [document_graph, document_variants=document]
    4.24 +  options [document_variants = document]
    4.25    theories [document = false]
    4.26      "~~/src/Tools/Permanent_Interpretation"
    4.27      "~~/src/HOL/Library/While_Combinator"
    4.28 @@ -171,7 +169,6 @@
    4.29    theories EvenOdd
    4.30  
    4.31  session "HOL-Import" in Import = HOL +
    4.32 -  options [document_graph]
    4.33    theories HOL_Light_Maps
    4.34    theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
    4.35  
    4.36 @@ -180,7 +177,6 @@
    4.37      Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    4.38      Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
    4.39    *}
    4.40 -  options [document_graph]
    4.41    theories [document = false]
    4.42      "~~/src/HOL/Library/FuncSet"
    4.43      "~~/src/HOL/Library/Multiset"
    4.44 @@ -199,7 +195,6 @@
    4.45      Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    4.46      Theorem, Wilson's Theorem, Quadratic Reciprocity.
    4.47    *}
    4.48 -  options [document_graph]
    4.49    theories [document = false]
    4.50      "~~/src/HOL/Library/Infinite_Set"
    4.51      "~~/src/HOL/Library/Permutation"
    4.52 @@ -229,12 +224,11 @@
    4.53      Verification of shared-variable imperative programs a la Owicki-Gries.
    4.54      (verification conditions are generated automatically).
    4.55    *}
    4.56 -  options [document_graph]
    4.57    theories Hoare_Parallel
    4.58    document_files "root.bib" "root.tex"
    4.59  
    4.60  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
    4.61 -  options [document = false, document_graph = false, browser_info = false]
    4.62 +  options [document = false, browser_info = false]
    4.63    theories
    4.64      Generate
    4.65      Generate_Binary_Nat
    4.66 @@ -287,7 +281,6 @@
    4.67  
    4.68      The Isabelle Algebraic Library.
    4.69    *}
    4.70 -  options [document_graph]
    4.71    theories [document = false]
    4.72      (* Preliminaries from set and number theory *)
    4.73      "~~/src/HOL/Library/FuncSet"
    4.74 @@ -311,7 +304,6 @@
    4.75    description {*
    4.76      A new approach to verifying authentication protocols.
    4.77    *}
    4.78 -  options [document_graph]
    4.79    theories
    4.80      Auth_Shared
    4.81      Auth_Public
    4.82 @@ -327,7 +319,6 @@
    4.83  
    4.84      Verifying security protocols using Chandy and Misra's UNITY formalism.
    4.85    *}
    4.86 -  options [document_graph]
    4.87    theories
    4.88      (*Basic meta-theory*)
    4.89      "UNITY_Main"
    4.90 @@ -375,7 +366,7 @@
    4.91    document_files "root.tex"
    4.92  
    4.93  session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
    4.94 -  options [document_graph, print_mode = "iff,no_brackets"]
    4.95 +  options [print_mode = "iff,no_brackets"]
    4.96    theories [document = false]
    4.97      "~~/src/HOL/Library/Countable"
    4.98      "~~/src/HOL/Library/Monad_Syntax"
    4.99 @@ -425,8 +416,7 @@
   4.100      The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   4.101      theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   4.102    *}
   4.103 -  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0,
   4.104 -    quick_and_dirty = false]
   4.105 +  options [print_mode = "no_brackets", parallel_proofs = 0, quick_and_dirty = false]
   4.106    theories [document = false]
   4.107      "~~/src/HOL/Library/Code_Target_Int"
   4.108    theories
   4.109 @@ -455,9 +445,10 @@
   4.110      machine and a specification of its bytecode verifier and a lightweight
   4.111      bytecode verifier, including proofs of type-safety.
   4.112    *}
   4.113 -  options [document_graph]
   4.114 -  theories [document = false] "~~/src/HOL/Library/While_Combinator"
   4.115 -  theories MicroJava
   4.116 +  theories [document = false]
   4.117 +    "~~/src/HOL/Library/While_Combinator"
   4.118 +  theories
   4.119 +    MicroJava
   4.120    document_files
   4.121      "introduction.tex"
   4.122      "root.bib"
   4.123 @@ -467,12 +458,10 @@
   4.124    description {*
   4.125      Hoare Logic for a tiny fragment of Java.
   4.126    *}
   4.127 -  options [document_graph]
   4.128    theories Example
   4.129    document_files "root.bib" "root.tex"
   4.130  
   4.131  session "HOL-Bali" in Bali = HOL +
   4.132 -  options [document_graph]
   4.133    theories
   4.134      AxExample
   4.135      AxSound
   4.136 @@ -646,7 +635,6 @@
   4.137    description {*
   4.138      Verification of the SET Protocol.
   4.139    *}
   4.140 -  options [document_graph]
   4.141    theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   4.142    theories SET_Protocol
   4.143    document_files "root.tex"
   4.144 @@ -655,7 +643,6 @@
   4.145    description {*
   4.146      Two-dimensional matrices and linear programming.
   4.147    *}
   4.148 -  options [document_graph]
   4.149    theories Cplex
   4.150    document_files "root.tex"
   4.151  
   4.152 @@ -697,7 +684,6 @@
   4.153      ATP_Problem_Import
   4.154  
   4.155  session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   4.156 -  options [document_graph]
   4.157    theories
   4.158      Multivariate_Analysis
   4.159      Determinants
   4.160 @@ -707,7 +693,6 @@
   4.161      "root.tex"
   4.162  
   4.163  session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   4.164 -  options [document_graph]
   4.165    theories [document = false]
   4.166      "~~/src/HOL/Library/Countable"
   4.167      "~~/src/HOL/Library/Permutation"
   4.168 @@ -786,7 +771,6 @@
   4.169      Misc_N2M
   4.170  
   4.171  session "HOL-Word" (main) in Word = HOL +
   4.172 -  options [document_graph]
   4.173    theories Word
   4.174    document_files "root.bib" "root.tex"
   4.175  
   4.176 @@ -803,7 +787,6 @@
   4.177    description {*
   4.178      Nonstandard analysis.
   4.179    *}
   4.180 -  options [document_graph]
   4.181    theories Hypercomplex
   4.182    document_files "root.tex"
   4.183  
   4.184 @@ -994,7 +977,6 @@
   4.185  
   4.186      HOLCF -- a semantic extension of HOL by the LCF logic.
   4.187    *}
   4.188 -  options [document_graph]
   4.189    theories [document = false]
   4.190      "~~/src/HOL/Library/Nat_Bijection"
   4.191      "~~/src/HOL/Library/Countable"
     5.1 --- a/src/Pure/PIDE/session.ML	Sun Jan 25 21:46:21 2015 +0100
     5.2 +++ b/src/Pure/PIDE/session.ML	Sun Jan 25 22:11:06 2015 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4    val name: unit -> string
     5.5    val welcome: unit -> string
     5.6    val get_keywords: unit -> Keyword.keywords
     5.7 -  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     5.8 +  val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     5.9      (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
    5.10    val shutdown: unit -> unit
    5.11    val finish: unit -> unit
    5.12 @@ -42,7 +42,7 @@
    5.13  
    5.14  (* init *)
    5.15  
    5.16 -fun init build info info_path doc doc_graph doc_output doc_variants doc_files graph_file
    5.17 +fun init build info info_path doc doc_output doc_variants doc_files graph_file
    5.18      parent (chapter, name) verbose =
    5.19    if #name (! session) <> parent orelse not (! session_finished) then
    5.20      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    5.21 @@ -52,7 +52,7 @@
    5.22        val _ = session_finished := false;
    5.23      in
    5.24        Present.init build info info_path (if doc = "false" then "" else doc)
    5.25 -        doc_graph doc_output doc_variants doc_files graph_file (chapter, name)
    5.26 +        doc_output doc_variants doc_files graph_file (chapter, name)
    5.27          verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    5.28      end;
    5.29  
     6.1 --- a/src/Pure/Thy/present.ML	Sun Jan 25 21:46:21 2015 +0100
     6.2 +++ b/src/Pure/Thy/present.ML	Sun Jan 25 22:11:06 2015 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4    val session_name: theory -> string
     6.5    val document_enabled: string -> bool
     6.6    val document_variants: string -> (string * string) list
     6.7 -  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     6.8 +  val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     6.9      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> theory list -> unit
    6.10    val finish: unit -> unit
    6.11    val theory_output: string -> string -> unit
    6.12 @@ -160,18 +160,16 @@
    6.13  (* session_info *)
    6.14  
    6.15  type session_info =
    6.16 -  {name: string, chapter: string, info_path: Path.T, info: bool,
    6.17 -    doc_format: string, doc_graph: bool, doc_output: Path.T option,
    6.18 -    doc_files: (Path.T * Path.T) list, graph_file: Path.T, documents: (string * string) list,
    6.19 -    verbose: bool, readme: Path.T option};
    6.20 +  {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string,
    6.21 +    doc_output: Path.T option, doc_files: (Path.T * Path.T) list, graph_file: Path.T,
    6.22 +    documents: (string * string) list, verbose: bool, readme: Path.T option};
    6.23  
    6.24  fun make_session_info
    6.25 -  (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
    6.26 -    doc_files, graph_file, documents, verbose, readme) =
    6.27 -  {name = name, chapter = chapter, info_path = info_path, info = info,
    6.28 -    doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    6.29 -    doc_files = doc_files, graph_file = graph_file, documents = documents,
    6.30 -    verbose = verbose, readme = readme}: session_info;
    6.31 +  (name, chapter, info_path, info, doc_format, doc_output, doc_files,
    6.32 +    graph_file, documents, verbose, readme) =
    6.33 +  {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format,
    6.34 +    doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
    6.35 +    documents = documents, verbose = verbose, readme = readme}: session_info;
    6.36  
    6.37  
    6.38  (* state *)
    6.39 @@ -205,7 +203,7 @@
    6.40  
    6.41  (* init session *)
    6.42  
    6.43 -fun init build info info_path doc doc_graph document_output doc_variants doc_files graph_file
    6.44 +fun init build info info_path doc document_output doc_variants doc_files graph_file
    6.45      (chapter, name) verbose thys =
    6.46    if not build andalso not info andalso doc = "" then
    6.47      (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
    6.48 @@ -229,7 +227,7 @@
    6.49      in
    6.50        session_info :=
    6.51          SOME (make_session_info (name, chapter, info_path, info, doc,
    6.52 -          doc_graph, doc_output, doc_files, graph_file, documents, verbose, readme));
    6.53 +          doc_output, doc_files, graph_file, documents, verbose, readme));
    6.54        Synchronized.change browser_info (K (init_browser_info (chapter, name) thys));
    6.55        add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
    6.56      end;
    6.57 @@ -264,7 +262,7 @@
    6.58    write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
    6.59  
    6.60  fun finish () =
    6.61 -  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
    6.62 +  with_session_info () (fn {name, chapter, info, info_path, doc_format,
    6.63      doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
    6.64    let
    6.65      val {theories, tex_index, html_index, graph} = Synchronized.value browser_info;
     7.1 --- a/src/Pure/Tools/build.ML	Sun Jan 25 21:46:21 2015 +0100
     7.2 +++ b/src/Pure/Tools/build.ML	Sun Jan 25 22:11:06 2015 +0100
     7.3 @@ -140,7 +140,6 @@
     7.4            (Options.bool options "browser_info")
     7.5            (Path.explode browser_info)
     7.6            (Options.string options "document")
     7.7 -          (Options.bool options "document_graph")
     7.8            (Options.string options "document_output")
     7.9            (Present.document_variants (Options.string options "document_variants"))
    7.10            (map (apply2 Path.explode) document_files)
     8.1 --- a/src/ZF/ROOT	Sun Jan 25 21:46:21 2015 +0100
     8.2 +++ b/src/ZF/ROOT	Sun Jan 25 22:11:06 2015 +0100
     8.3 @@ -42,7 +42,6 @@
     8.4      Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
     8.5      (North-Holland, 1980)
     8.6    *}
     8.7 -  options [document_graph]
     8.8    theories
     8.9      Main
    8.10      Main_ZFC
    8.11 @@ -63,7 +62,6 @@
    8.12      "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
    8.13      development and ZF's theories of cardinals.
    8.14    *}
    8.15 -  options [document_graph]
    8.16    theories
    8.17      WO6_WO1
    8.18      WO1_WO7
    8.19 @@ -123,8 +121,10 @@
    8.20      A paper describing this development is
    8.21      http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
    8.22    *}
    8.23 -  options [document_graph]
    8.24 -  theories DPow_absolute AC_in_L Rank_Separation
    8.25 +  theories
    8.26 +    DPow_absolute
    8.27 +    AC_in_L
    8.28 +    Rank_Separation
    8.29    document_files "root.tex" "root.bib"
    8.30  
    8.31  session "ZF-IMP" in IMP = ZF +