src/Pure/Thy/present.ML

 signature PRESENT =
 sig
   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
   val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
   val display_drafts: Path.T list -> int

 (** global session state **)
 
 (* 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 *)
 
 val session_info = Unsynchronized.ref (NONE: session_info option);

   in variants end;
 
 
 (* 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)
   else
     let

         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
           map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
     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;
 
 

 
 fun write_tex_index tex_index path =
   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;
     val thys = Symtab.dest theories;
     val sorted_graph = Graph_Display.sort_graph graph;