merged

--- a/src/HOL/ROOT	Thu Jul 16 04:52:26 2020 +0000
+++ b/src/HOL/ROOT	Thu Jul 16 20:35:03 2020 +0200
@@ -479,7 +479,7 @@
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   sessions
-    "HOL-Isar_Examples"
+    "HOL-Examples"
   theories
     Hilbert_Classical
     Proof_Terms

--- a/src/Pure/ML/ml_statistics.scala	Thu Jul 16 04:52:26 2020 +0000
+++ b/src/Pure/ML/ml_statistics.scala	Thu Jul 16 20:35:03 2020 +0200
@@ -42,10 +42,10 @@
       if (props.nonEmpty) consume(props)
     }
 
-    Bash.process("exec \"$POLYML_EXE\" -q --use " +
-      File.bash_platform_path(Path.explode("~~/src/Pure/ML/ml_statistics.ML")) +
-      " --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
-          ML_Syntax.print_double(delay.seconds)))
+    Bash.process("exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+        Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
+          ML_Syntax.print_double(delay.seconds)),
+        cwd = Path.explode("~~").file)
       .result(progress_stdout = progress_stdout, strict = false).check
   }
 

--- a/src/Pure/PIDE/resources.ML	Thu Jul 16 04:52:26 2020 +0000
+++ b/src/Pure/PIDE/resources.ML	Thu Jul 16 20:35:03 2020 +0200
@@ -121,8 +121,10 @@
 (
   type T = files;
   val empty = make_files (Path.current, [], []);
-  fun extend _ = empty;
-  fun merge _ = empty;
+  val extend = I;
+  fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
+    let val provided' = Library.merge (op =) (provided1, provided2)
+    in make_files (master_dir, imports, provided') end
 );
 
 fun map_files f =

--- a/src/Pure/Thy/present.ML	Thu Jul 16 04:52:26 2020 +0000
+++ b/src/Pure/Thy/present.ML	Thu Jul 16 20:35:03 2020 +0200
@@ -36,22 +36,32 @@
 
 
 
-(** additional theory data **)
+(** theory data **)
+
+type browser_info = {chapter: string, name: string, bibtex_entries: string list};
+val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []};
 
 structure Browser_Info = Theory_Data
 (
-  type T = {chapter: string, name: string, bibtex_entries: string list};
-  val empty = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}: T;
-  fun extend _ = empty;
-  fun merge _ = empty;
+  type T = browser_info
+  val empty = empty_browser_info;
+  val extend = I;
+  val merge = #1;
 );
 
-val _ = Theory.setup
-  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
+fun reset_browser_info thy =
+  if Browser_Info.get thy = empty_browser_info then NONE
+  else SOME (Browser_Info.put empty_browser_info thy);
+
+val _ =
+  Theory.setup
+   (Theory.at_begin reset_browser_info #>
+    Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
 
 val get_bibtex_entries = #bibtex_entries o Browser_Info.get;
 
 
+
 (** global browser info state **)
 
 (* type theory_info *)

--- a/src/Pure/Tools/generated_files.ML	Thu Jul 16 04:52:26 2020 +0000
+++ b/src/Pure/Tools/generated_files.ML	Thu Jul 16 20:35:03 2020 +0200
@@ -52,39 +52,55 @@
 
 (** context data **)
 
+type file = Path.T * (Position.T * string);
+
 type file_type =
   {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
 
 type antiquotation = Token.src -> Proof.context -> file_type -> string;
 
+fun err_dup_files path pos pos' =
+  error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']);
+
 structure Data = Theory_Data
 (
   type T =
-    (Path.T * (Position.T * string)) list *  (*files for current theory*)
+    file list Symtab.table *  (*files for named theory*)
     file_type Name_Space.table *  (*file types*)
     antiquotation Name_Space.table;  (*antiquotations*)
   val empty =
-    ([],
+    (Symtab.empty,
      Name_Space.empty_table Markup.file_typeN,
      Name_Space.empty_table Markup.antiquotationN);
-  val extend = @{apply 3(1)} (K []);
-  fun merge ((_, types1, antiqs1), (_, types2, antiqs2)) =
-    ([],
-     Name_Space.merge_tables (types1, types2),
-     Name_Space.merge_tables (antiqs1, antiqs2));
+  val extend = I;
+  fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
+    let
+      val files' =
+        (files1, files2) |> Symtab.join (K (Library.merge (fn ((path1, file1), (path2, file2)) =>
+          if path1 <> path2 then false
+          else if file1 = file2 then true
+          else err_dup_files path1 (#1 file1) (#1 file2))));
+      val types' = Name_Space.merge_tables (types1, types2);
+      val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2);
+    in (files', types', antiqs') end;
 );
 
-fun add_files (binding, content) =
+fun lookup_files thy =
+  Symtab.lookup_list (#1 (Data.get thy)) (Context.theory_long_name thy);
+
+fun update_files thy_files' thy =
+  (Data.map o @{apply 3(1)}) (Symtab.update (Context.theory_long_name thy, thy_files')) thy;
+
+fun add_files (binding, content) thy =
   let
     val _ = Path.proper_binding binding;
     val (path, pos) = Path.dest_binding binding;
-  in
-    (Data.map o @{apply 3(1)}) (fn files =>
-      (case AList.lookup (op =) files path of
-        SOME (pos', _) =>
-          error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos'])
-      | NONE => (path, (pos, content)) :: files))
-  end;
+    val thy_files = lookup_files thy;
+    val thy_files' =
+      (case AList.lookup (op =) thy_files path of
+        SOME (pos', _) => err_dup_files path pos pos'
+      | NONE => (path, (pos, content)) :: thy_files);
+  in update_files thy_files' thy end;
 
 
 (* get files *)
@@ -101,7 +117,7 @@
 
 
 fun get_files thy =
-  Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) =>
+  lookup_files thy |> rev |> map (fn (path, (pos, content)) =>
     {path = path, pos = pos, content = content}: file);
 
 fun get_file thy binding =

--- a/src/Pure/more_thm.ML	Thu Jul 16 04:52:26 2020 +0000
+++ b/src/Pure/more_thm.ML	Thu Jul 16 20:35:03 2020 +0200
@@ -654,16 +654,24 @@
 
 structure Proofs = Theory_Data
 (
-  type T = thm list lazy list;
-  val empty = [];
-  fun extend _ = empty;
-  fun merge _ = empty;
+  type T = thm list lazy Inttab.table;
+  val empty = Inttab.empty;
+  val extend = I;
+  val merge = Inttab.merge (K true);
 );
 
-fun register_proofs ths =
-  (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths);
+fun reset_proofs thy =
+  if Inttab.is_empty (Proofs.get thy) then NONE
+  else SOME (Proofs.put Inttab.empty thy);
+
+val _ = Theory.setup (Theory.at_begin reset_proofs);
 
-fun force_proofs thy = rev (Proofs.get thy) |> maps (map (Thm.transfer thy) o Lazy.force);
+fun register_proofs ths thy =
+  let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths)
+  in (Proofs.map o Inttab.update) entry thy end;
+
+fun force_proofs thy =
+  Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2);
 
 val consolidate_theory = Thm.consolidate o force_proofs;