# HG changeset patch # User wenzelm # Date 1397146424 -7200 # Node ID 5c178501cf784ea478aa12dd06181dcf22fc729e # Parent a13c2ccc160b7622642b0e0e38dd9bc4699df0e3 removed obsolete doc_dump option (see also 892061142ba6); diff -r a13c2ccc160b -r 5c178501cf78 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Thu Apr 10 15:14:38 2014 +0200 +++ b/src/Pure/PIDE/session.ML Thu Apr 10 18:13:44 2014 +0200 @@ -9,7 +9,7 @@ val name: unit -> string val welcome: unit -> string val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> - string -> string * string -> bool * string -> bool -> unit + string -> string * string -> bool -> unit val finish: unit -> unit val protocol_handler: string -> unit val init_protocol_handlers: unit -> unit @@ -34,7 +34,7 @@ (* init *) fun init build info info_path doc doc_graph doc_output doc_variants - parent (chapter, name) doc_dump verbose = + parent (chapter, name) verbose = if #name (! session) <> parent orelse not (! session_finished) then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else @@ -44,7 +44,7 @@ in Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output doc_variants (chapter, name) - doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) + verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) end; diff -r a13c2ccc160b -r 5c178501cf78 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Apr 10 15:14:38 2014 +0200 +++ b/src/Pure/Thy/present.ML Thu Apr 10 18:13:44 2014 +0200 @@ -9,7 +9,7 @@ val session_name: theory -> string val read_variant: string -> string * string val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> - string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*) + string * string -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val theory_output: string -> string -> unit val begin_theory: int -> (unit -> HTML.text) -> theory -> theory @@ -168,17 +168,17 @@ (* 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, - documents: (string * string) list, doc_dump: (bool * string), verbose: bool, + {name: string, chapter: string, info_path: Path.T, info: bool, + doc_format: string, doc_graph: bool, doc_output: Path.T option, + 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, - documents, doc_dump, verbose, readme) = + 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, - documents = documents, doc_dump = doc_dump, verbose = verbose, + documents = documents, verbose = verbose, readme = readme}: session_info; @@ -204,8 +204,8 @@ (* init session *) fun init build info info_path doc doc_graph document_output doc_variants - (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys = - if not build andalso not info andalso doc = "" andalso dump_prefix = "" then + (chapter, name) verbose thys = + if not build andalso not info andalso doc = "" then (browser_info := empty_browser_info; session_info := NONE) else let @@ -227,7 +227,7 @@ in session_info := SOME (make_session_info (name, chapter, info_path, info, doc, - doc_graph, doc_output, documents, doc_dump, verbose, readme)); + doc_graph, doc_output, documents, verbose, readme)); browser_info := init_browser_info (chapter, name) thys; add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html")) end; @@ -278,7 +278,7 @@ fun finish () = with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output, - documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} => + documents, verbose, readme, ...} => let val {theories, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; @@ -291,7 +291,7 @@ val sorted_graph = sorted_index graph; val opt_graphs = - if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then + if doc_graph andalso not (null documents) then SOME (isabelle_browser sorted_graph) else NONE; @@ -325,18 +325,6 @@ List.app (fn (a, {tex_source, ...}) => write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys); - val _ = - if dump_prefix = "" then () - else - let - val path = Path.explode dump_prefix; - val _ = prepare_sources dump_copy path; - in - if verbose then - Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") - else () - end; - fun document_job doc_prefix backdrop (name, tags) = let val _ = diff -r a13c2ccc160b -r 5c178501cf78 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu Apr 10 15:14:38 2014 +0200 +++ b/src/Pure/Tools/build.ML Thu Apr 10 18:13:44 2014 +0200 @@ -157,7 +157,6 @@ (Options.string options "document_output") document_variants parent_name (chapter, name) - (false, "") verbose; val last_timing = lookup_timings (fold update_timings command_timings empty_timings);