1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 28 16:51:36 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Tue Apr 28 17:50:18 2020 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  Calc work on Problem employing Method; both are collected in a respective Store;
     1.5  The collections' structure is independent from the dependency graph of Isabelle's theories
     1.6  in Knowledge.
     1.7 -Store is also used by Thy_Html, required for Isac's Java front end, irrelevant for PIDE.
     1.8 +Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
     1.9  
    1.10  The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
    1.11  they also include minimal code required for other "xxxxx-def.sml" files.
    1.12 @@ -36,7 +36,7 @@
    1.13  ML_file "problem-def.sml"
    1.14  ML_file "method-def.sml"
    1.15  ML_file "cas-def.sml"
    1.16 -ML_file "thy-html.sml"
    1.17 +ML_file "thy-write.sml"
    1.18  
    1.19  ML \<open>
    1.20  \<close> ML \<open>
    1.21 @@ -69,9 +69,9 @@
    1.22    val add_pbts: (Probl_Def.T * Spec.id) list -> theory -> theory
    1.23    val get_mets: theory -> Meth_Def.store
    1.24    val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
    1.25 -  val get_thes: theory -> (Thy_Html.thydata Store.node) list
    1.26 -  val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.27 -  val insert_fillpats: (Thy_Html.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.28 +  val get_thes: theory -> (Thy_Write.thydata Store.node) list
    1.29 +  val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.30 +  val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.31    val get_ref_thy: unit -> theory
    1.32    val set_ref_thy: theory -> unit
    1.33  end;                               
    1.34 @@ -135,21 +135,21 @@
    1.35          in Data.map (fold add_met mets) thy end;
    1.36  
    1.37    structure Data = Theory_Data (
    1.38 -    type T = (Thy_Html.thydata Store.node) list;
    1.39 +    type T = (Thy_Write.thydata Store.node) list;
    1.40      val empty = [];
    1.41      val extend = I;
    1.42      val merge = Store.merge; (* relevant for store_thm, store_rls *)
    1.43      );                                                              
    1.44    fun get_thes thy = Data.get thy
    1.45    fun add_thes thes thy = let
    1.46 -    fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata
    1.47 +    fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
    1.48    in Data.map (fold add_the thes) thy end;
    1.49    fun insert_fillpats fis thy =
    1.50      let
    1.51        fun update_elem (theID, fillpats) =
    1.52          let
    1.53            val hthm = Store.get (Data.get thy) theID theID
    1.54 -          val hthm' = Thy_Html.update_hthm hthm fillpats
    1.55 +          val hthm' = Thy_Write.update_hthm hthm fillpats
    1.56              handle ERROR _ =>
    1.57                error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
    1.58          in Store.update theID theID hthm' end
    1.59 @@ -208,11 +208,11 @@
    1.60  section \<open>determine sequence of main parts in thehier\<close>
    1.61  setup \<open>
    1.62  KEStore_Elems.add_thes
    1.63 -  [(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacKnowledge"], html = "",
    1.64 +  [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
    1.65      mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
    1.66 -  (Thy_Html.Html {guh = Thy_Html.part2guh ["Isabelle"], html = "",
    1.67 +  (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
    1.68      mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
    1.69 -  (Thy_Html.Html {guh = Thy_Html.part2guh ["IsacScripts"], html = "",
    1.70 +  (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
    1.71      mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
    1.72  \<close>
    1.73  
    1.74 @@ -256,10 +256,10 @@
    1.75  fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
    1.76  val sort_kestore_met = sort_kestore_ptyp' met_ord;
    1.77  
    1.78 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
    1.79 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
    1.80  fun write_thes thydata_list =
    1.81    thydata_list 
    1.82 -    |> map (fn (id, the) => (Thy_Html.theID2str id, Thy_Html.the2str the))
    1.83 +    |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
    1.84      |> map pair2str
    1.85      |> map writeln
    1.86  \<close>