# HG changeset patch # User wenzelm # Date 1605650276 -3600 # Node ID 2a7fc87495e083c9122dfbb185b12d615f62f234 # Parent fd68c9c1b90b8b5a79e8a2080e4be300015987c0 refer to command_timings/last_timing via resources; diff -r fd68c9c1b90b -r 2a7fc87495e0 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Tue Nov 17 22:05:59 2020 +0100 +++ b/src/Pure/PIDE/resources.ML Tue Nov 17 22:57:56 2020 +0100 @@ -13,6 +13,7 @@ session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, + command_timings: Properties.T list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit @@ -24,6 +25,7 @@ val html_symbols: unit -> HTML.symbols val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> string + val last_timing: Toplevel.transition -> Time.time val check_doc: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list @@ -50,6 +52,41 @@ structure Resources: RESOURCES = struct +(* command timings *) + +type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) + +val empty_timings: timings = Symtab.empty; + +fun update_timings props = + (case Markup.parse_command_timing_properties props of + SOME ({file, offset, name}, time) => + Symtab.map_default (file, Inttab.empty) + (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) + | NONE => I); + +fun make_timings command_timings = + fold update_timings command_timings empty_timings; + +fun approximative_id name pos = + (case (Position.file_of pos, Position.offset_of pos) of + (SOME file, SOME offset) => + if name = "" then NONE else SOME {file = file, offset = offset, name = name} + | _ => NONE); + +fun get_timings timings tr = + (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of + SOME {file, offset, name} => + (case Symtab.lookup timings file of + SOME offsets => + (case Inttab.lookup offsets offset of + SOME (name', time) => if name = name' then SOME time else NONE + | NONE => NONE) + | NONE => NONE) + | NONE => NONE) + |> the_default Time.zeroTime; + + (* session base *) val default_qualifier = "Draft"; @@ -65,6 +102,7 @@ session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, + timings = empty_timings, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}; @@ -74,7 +112,7 @@ fun init_session {html_symbols, session_positions, session_directories, session_chapters, - bibtex_entries, docs, global_theories, loaded_theories} = + bibtex_entries, command_timings, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => {html_symbols = HTML.make_symbols html_symbols, @@ -84,6 +122,7 @@ session_directories Symtab.empty, session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, + timings = make_timings command_timings, docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories}); @@ -91,13 +130,14 @@ fun init_session_yxml yxml = let val (html_symbols, (session_positions, (session_directories, (session_chapters, - (bibtex_entries, (docs, (global_theories, loaded_theories))))))) = + (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories)))))))) = YXML.parse_body yxml |> let open XML.Decode in - pair (list (pair string int)) (pair (list (pair string properties)) - (pair (list (pair string string)) (pair (list (pair string string)) - (pair (list (pair string (list string))) (pair (list string) - (pair (list (pair string string)) (list string))))))) + pair (list (pair string int)) + (pair (list (pair string properties)) + (pair (list (pair string string)) (pair (list (pair string string)) + (pair (list (pair string (list string))) (pair (list properties) + (pair (list string) (pair (list (pair string string)) (list string)))))))) end; in init_session @@ -106,6 +146,7 @@ session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, + command_timings = command_timings, docs = docs, global_theories = global_theories, loaded_theories = loaded_theories} @@ -122,6 +163,7 @@ session_directories = Symtab.empty, session_chapters = Symtab.empty, bibtex_entries = Symtab.empty, + timings = empty_timings, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); @@ -145,6 +187,8 @@ fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name); +fun last_timing tr = get_timings (get_session_base #timings) tr; + val check_doc = check_name #docs "documentation" (Markup.doc o #1); diff -r fd68c9c1b90b -r 2a7fc87495e0 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Nov 17 22:05:59 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Tue Nov 17 22:57:56 2020 +0100 @@ -15,7 +15,8 @@ class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, - val log: Logger = No_Logger) + val log: Logger = No_Logger, + command_timings: List[Properties.T] = Nil) { resources => @@ -32,16 +33,18 @@ pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), + pair(list(properties), pair(list(string), - pair(list(pair(string, string)), list(string))))))))( + pair(list(pair(string, string)), list(string)))))))))( (Symbol.codes, (resources.sessions_structure.session_positions, (resources.sessions_structure.dest_session_directories, (resources.sessions_structure.session_chapters, (resources.sessions_structure.bibtex_entries, + (command_timings, (resources.session_base.doc_names, (resources.session_base.global_theories.toList, - resources.session_base.loaded_theories.keys))))))))) + resources.session_base.loaded_theories.keys)))))))))) } diff -r fd68c9c1b90b -r 2a7fc87495e0 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Nov 17 22:05:59 2020 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue Nov 17 22:57:56 2020 +0100 @@ -18,8 +18,7 @@ val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit - type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time} - val use_theories: context -> string -> (string * Position.T) list -> unit + val use_theories: Options.T -> string -> (string * Position.T) list -> unit val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit @@ -180,14 +179,6 @@ fun update_thy deps theory = change_thys (update deps theory); -(* context *) - -type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time}; - -fun default_context (): context = - {options = Options.default (), last_timing = K Time.zeroTime}; - - (* scheduling loader tasks *) datatype result = @@ -272,12 +263,12 @@ (* eval theory *) -fun excursion keywords master_dir last_timing init elements = +fun excursion keywords master_dir init elements = let fun prepare_span st span = Command_Span.content span |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) - |> (fn tr => Toplevel.timing (last_timing tr) tr); + |> (fn tr => Toplevel.timing (Resources.last_timing tr) tr); fun element_result span_elem (st, _) = let @@ -292,9 +283,8 @@ val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; -fun eval_thy (context: context) update_time master_dir header text_pos text parents = +fun eval_thy options update_time master_dir header text_pos text parents = let - val {options, last_timing} = context; val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents @@ -306,7 +296,7 @@ fun init () = Resources.begin_theory master_dir header parents; val (results, thy) = cond_timeit true ("theory " ^ quote name) - (fn () => excursion keywords master_dir last_timing init elements); + (fn () => excursion keywords master_dir init elements); fun present () = let @@ -325,7 +315,7 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy context initiators update_time deps text (name, pos) keywords parents = +fun load_thy options initiators update_time deps text (name, pos) keywords parents = let val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); @@ -348,7 +338,7 @@ val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = - eval_thy context update_time dir header text_pos text + eval_thy options update_time dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; @@ -380,9 +370,9 @@ in -fun require_thys context initiators qualifier dir strs tasks = - fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I -and require_thy context initiators qualifier dir (s, require_pos) tasks = +fun require_thys options initiators qualifier dir strs tasks = + fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I +and require_thy options initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in @@ -403,7 +393,7 @@ val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = - require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; + require_thys options (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = @@ -415,7 +405,7 @@ let val update_time = serial (); val load = - load_thy context initiators update_time + load_thy options initiators update_time dep text (theory_name, theory_pos) keywords; in Task (parents, load) end); @@ -428,12 +418,12 @@ (* use theories *) -fun use_theories context qualifier imports = - let val (_, tasks) = require_thys context [] qualifier Path.current imports String_Graph.empty +fun use_theories options qualifier imports = + let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; fun use_thy name = - use_theories (default_context ()) Resources.default_qualifier [(name, Position.none)]; + use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]; (* toplevel scripting -- without maintaining database *) diff -r fd68c9c1b90b -r 2a7fc87495e0 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Tue Nov 17 22:05:59 2020 +0100 +++ b/src/Pure/Tools/build.ML Tue Nov 17 22:57:56 2020 +0100 @@ -7,38 +7,6 @@ structure Build: sig end = struct -(* command timings *) - -type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) - -val empty_timings: timings = Symtab.empty; - -fun update_timings props = - (case Markup.parse_command_timing_properties props of - SOME ({file, offset, name}, time) => - Symtab.map_default (file, Inttab.empty) - (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) - | NONE => I); - -fun approximative_id name pos = - (case (Position.file_of pos, Position.offset_of pos) of - (SOME file, SOME offset) => - if name = "" then NONE else SOME {file = file, offset = offset, name = name} - | _ => NONE); - -fun get_timings timings tr = - (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of - SOME {file, offset, name} => - (case Symtab.lookup timings file of - SOME offsets => - (case Inttab.lookup offsets offset of - SOME (name', time) => if name = name' then SOME time else NONE - | NONE => NONE) - | NONE => NONE) - | NONE => NONE) - |> the_default Time.zeroTime; - - (* session timing *) fun session_timing f x = @@ -55,9 +23,8 @@ (* build theories *) -fun build_theories last_timing qualifier (options, thys) = +fun build_theories qualifier (options, thys) = let - val context = {options = options, last_timing = last_timing}; val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; in @@ -65,7 +32,7 @@ (Options.set_default options; Isabelle_Process.init_options (); Future.fork I; - (Thy_Info.use_theories context qualifier + (Thy_Info.use_theories options qualifier |> (case Options.string options "profiling" of "" => I @@ -87,25 +54,23 @@ (fn [resources_yxml, args_yxml] => let val _ = Resources.init_session_yxml resources_yxml; - val (command_timings, (parent_name, (chapter, (session_name, theories)))) = + val (parent_name, (chapter, (session_name, theories))) = YXML.parse_body args_yxml |> let open XML.Decode; val position = Position.of_properties o properties; in - pair (list properties) (pair string (pair string - (pair string (list (pair Options.decode (list (pair string position))))))) + pair string (pair string (pair string + (list (pair Options.decode (list (pair string position)))))) end; fun build () = let val _ = Session.init parent_name (chapter, session_name); - val last_timing = get_timings (fold update_timings command_timings empty_timings); - val res1 = theories |> - (List.app (build_theories last_timing session_name) + (List.app (build_theories session_name) |> session_timing |> Exn.capture); val res2 = Exn.capture Session.finish (); diff -r fd68c9c1b90b -r 2a7fc87495e0 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Nov 17 22:05:59 2020 +0100 +++ b/src/Pure/Tools/build.scala Tue Nov 17 22:57:56 2020 +0100 @@ -187,7 +187,7 @@ } else Nil - val resources = new Resources(sessions_structure, base) + val resources = new Resources(sessions_structure, base, command_timings = command_timings0) val session = new Session(options, resources) { override val xml_cache: XML.Cache = store.xml_cache @@ -341,9 +341,9 @@ YXML.string_of_body( { import XML.Encode._ - pair(list(properties), pair(string, pair(string, pair(string, - list(pair(Options.encode, list(pair(string, properties))))))))( - (command_timings0, (parent, (info.chapter, (session_name, info.theories))))) + pair(string, pair(string, pair(string, + list(pair(Options.encode, list(pair(string, properties)))))))( + (parent, (info.chapter, (session_name, info.theories)))) }) session.protocol_command("build_session", resources_yxml, args_yxml) Build_Session_Errors.result