# HG changeset patch # User wenzelm # Date 1585419119 -3600 # Node ID fb6953e77000a6c605b452fbf944bd503c3d1880 # Parent 5730eb952208d969e8f0d07dbc9f75581e6eb478 eliminated pointless flag (see also 6533ceee4cd7); diff -r 5730eb952208 -r fb6953e77000 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Sat Mar 28 18:33:25 2020 +0100 +++ b/src/Pure/PIDE/session.ML Sat Mar 28 19:11:59 2020 +0100 @@ -9,7 +9,7 @@ val get_name: unit -> string val welcome: unit -> string val get_keywords: unit -> Keyword.keywords - val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> + val init: HTML.symbols -> 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 @@ -48,13 +48,13 @@ (* init *) -fun init symbols build info info_path doc doc_output doc_variants doc_files graph_file +fun init symbols info info_path doc doc_output doc_variants doc_files graph_file parent (chapter, name) verbose = (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) => if parent_name <> parent orelse not parent_finished then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else ({chapter = chapter, name = name}, false)); - Present.init symbols build info info_path (if doc = "false" then "" else doc) + Present.init symbols info info_path (if doc = "false" then "" else doc) doc_output doc_variants doc_files graph_file (chapter, name) verbose); diff -r 5730eb952208 -r fb6953e77000 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sat Mar 28 18:33:25 2020 +0100 +++ b/src/Pure/Thy/present.ML Sat Mar 28 19:11:59 2020 +0100 @@ -10,7 +10,7 @@ val theory_qualifier: theory -> string val document_option: Options.T -> {enabled: bool, disabled: bool} val document_variants: Options.T -> (string * string) list - val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> + val init: HTML.symbols -> bool -> Path.T -> string -> string -> (string * string) list -> (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit val finish: unit -> unit val theory_output: theory -> string list -> unit @@ -165,28 +165,25 @@ (* init session *) -fun init symbols build info info_path doc document_output doc_variants doc_files graph_file +fun init symbols info info_path doc document_output doc_variants doc_files graph_file (chapter, name) verbose = - if not build andalso not info andalso doc = "" then - (Synchronized.change browser_info (K empty_browser_info); session_info := NONE) - else - let - val doc_output = - if document_output = "" then NONE else SOME (Path.explode document_output); + let + val doc_output = + if document_output = "" then NONE else SOME (Path.explode document_output); + + 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 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 = - (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 (symbols, name, chapter, info_path, info, doc, - doc_output, doc_files, graph_file, documents, verbose, readme)); - Synchronized.change browser_info (K empty_browser_info); - add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) - end; + val docs = + (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 (symbols, name, chapter, info_path, info, doc, + doc_output, doc_files, graph_file, documents, verbose, readme)); + Synchronized.change browser_info (K empty_browser_info); + add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) + end; (* isabelle tool wrappers *) diff -r 5730eb952208 -r fb6953e77000 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sat Mar 28 18:33:25 2020 +0100 +++ b/src/Pure/Tools/build.ML Sat Mar 28 19:11:59 2020 +0100 @@ -133,7 +133,6 @@ datatype args = Args of {symbol_codes: (string * int) list, command_timings: Properties.T list, - do_output: bool, verbose: bool, browser_info: Path.T, document_files: (Path.T * Path.T) list, @@ -154,20 +153,20 @@ let open XML.Decode; val position = Position.of_properties o properties; - val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, + val (symbol_codes, (command_timings, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, (theories, (session_positions, (session_directories, (doc_names, (global_theories, - (loaded_theories, bibtex_entries))))))))))))))))) = - pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string + (loaded_theories, bibtex_entries)))))))))))))))) = + pair (list (pair string int)) (pair (list properties) (pair bool (pair string (pair (list (pair string string)) (pair string (pair string (pair string (pair string (pair string (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list string) - (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))) + (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) (YXML.parse_body yxml); in - Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, + Args {symbol_codes = symbol_codes, command_timings = command_timings, verbose = verbose, browser_info = Path.explode browser_info, document_files = map (apply2 Path.explode) document_files, graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, @@ -177,7 +176,7 @@ bibtex_entries = bibtex_entries} end; -fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, +fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = let @@ -194,7 +193,6 @@ val _ = Session.init symbols - do_output (Options.default_bool "browser_info") browser_info (Options.default_string "document") diff -r 5730eb952208 -r fb6953e77000 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Mar 28 18:33:25 2020 +0100 +++ b/src/Pure/Tools/build.scala Sat Mar 28 19:11:59 2020 +0100 @@ -214,22 +214,22 @@ YXML.string_of_body( { import XML.Encode._ - pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, + pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), - pair(list(string), list(string))))))))))))))))))( - (Symbol.codes, (command_timings, (do_output, (verbose, + pair(list(string), list(string)))))))))))))))))( + (Symbol.codes, (command_timings, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, - (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))))) + (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env =