refer to command_timings/last_timing via resources;
authorwenzelm
Tue, 17 Nov 2020 22:57:56 +0100
changeset 72874 2a7fc87495e0
parent 72873 fd68c9c1b90b
child 72875 db5f4572704a
refer to command_timings/last_timing via resources;
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
--- 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);
 
 
--- 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))))))))))
   }
 
 
--- 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 *)
--- 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 ();
--- 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