diff -r e794e1fbe6da -r ba0757da0dc8 src/Tools/isac/BaseDefinitions/Know_Store.thy
--- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 15:51:31 2020 +0200
+++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 16:17:27 2020 +0200
@@ -1,6 +1,11 @@
 (*  Title:      src/Tools/isac/Know_Store.thy
     Author:     Mathias Lehnfeld
 
+Calc work on Problem employing Method; both are collected in a respective Store;
+The collections' structure is independent from the dependency graph of Isabelle's theories
+in Knowledge.
+Store is also used by Thy_Html, required for Isac's Java front end, irrelevant for PIDE.
+
 The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
 they also include minimal code required for other "xxxxx-def.sml" files.
 These files have companion files "xxxxx.sml" with all further code,
@@ -67,7 +72,7 @@
   val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
   val get_mets: theory -> Celem6.mets
   val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
-  val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list
+  val get_thes: theory -> (Celem8.thydata Store.ptyp) list
   val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
   val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
   val get_ref_thy: unit -> theory
@@ -109,34 +114,34 @@
     type T = Celem5.ptyps;
     val empty = [Celem5.e_Ptyp];
     val extend = I;
-    val merge = Celem1.merge_ptyps;
+    val merge = Store.merge_ptyps;
     );
   fun get_ptyps thy = Data.get thy;
   fun add_pbts pbts thy = let
           fun add_pbt (pbt as {guh,...}, pblID) =
                 (* the pblID has the leaf-element as first; better readability achieved *)
                 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
-                  rev pblID |> Celem1.insrt pblID pbt);
+                  rev pblID |> Store.insrt pblID pbt);
         in Data.map (fold add_pbt pbts) thy end;
 
   structure Data = Theory_Data (
     type T = Celem6.mets;
     val empty = [Celem6.e_Mets];
     val extend = I;
-    val merge = Celem1.merge_ptyps;
+    val merge = Store.merge_ptyps;
     );
   val get_mets = Data.get;
   fun add_mets mets thy = let
           fun add_met (met as {guh,...}, metID) =
                 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
-                  Celem1.insrt metID met metID);
+                  Store.insrt metID met metID);
         in Data.map (fold add_met mets) thy end;
 
   structure Data = Theory_Data (
-    type T = (Celem8.thydata Celem1.ptyp) list;
+    type T = (Celem8.thydata Store.ptyp) list;
     val empty = [];
     val extend = I;
-    val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
+    val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
     );                                                              
   fun get_thes thy = Data.get thy
   fun add_thes thes thy = let
@@ -146,11 +151,11 @@
     let
       fun update_elem (theID, fillpats) =
         let
-          val hthm = Celem1.get_py (Data.get thy) theID theID
+          val hthm = Store.get_py (Data.get thy) theID theID
           val hthm' = Celem8.update_hthm hthm fillpats
             handle ERROR _ =>
               error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
-        in Celem1.update_ptyps theID theID hthm' end
+        in Store.update_ptyps theID theID hthm' end
     in Data.map (fold update_elem fis) thy end
 
   val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
@@ -235,21 +240,21 @@
   (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
 
 fun count_kestore_ptyps [] = 0
-  | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
+  | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
       1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
-fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
+fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
       (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
-fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
+fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
 fun sort_kestore_ptyp' _ [] = []
-  | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
-     ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
+  | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
+     ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
        :: sort_kestore_ptyp' ordfun ps');
 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
 
 fun metguh2str ({guh,...} : Celem6.met) = guh : string;
-fun check_kestore_met (mp: Celem6.met Celem1.ptyp) =
+fun check_kestore_met (mp: Celem6.met Store.ptyp) =
       check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
 val sort_kestore_met = sort_kestore_ptyp' met_ord;