--- 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);
--- 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 *)
--- 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")
--- 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 =