1.1 --- a/src/Tools/isac/KEStore.thy	Fri Jun 06 07:10:26 2014 +0200
     1.2 +++ b/src/Tools/isac/KEStore.thy	Fri Jun 06 14:49:18 2014 +0200
     1.3 @@ -215,5 +215,11 @@
     1.4  fun met_ord ({guh = guh'1, ...} : met, {guh = guh'2, ...} : met) = string_ord (guh'1, guh'2);
     1.5  val sort_kestore_met = sort_kestore_ptyp' met_ord;
     1.6  
     1.7 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' thes2str))) thes
     1.8 +fun write_thes thydata_list =
     1.9 +  thydata_list 
    1.10 +    |> map (fn (id, the) => (theID2str id, the2str the))
    1.11 +    |> map pair2str
    1.12 +    |> map writeln
    1.13  *}
    1.14  end

     2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Jun 06 07:10:26 2014 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Jun 06 14:49:18 2014 +0200
     2.3 @@ -89,13 +89,9 @@
     2.4    (map (collect_isab "Isabelle") rlsthmsNOTisac) @
     2.5    collect_part       "IsacScripts" proglang_parent progthys'
     2.6  : (theID * thydata) list
     2.7 -;
     2.8 -(*thehier := the_hier (get_thes ()) thydata_list;
     2.9 -tracing("----------------------------------\n" ^
    2.10 -	"*** insert: not found ... IS OK : \n" ^
    2.11 -	"comes from fill_parents           \n" ^
    2.12 -	"----------------------------------\n");*)
    2.13 -*} 
    2.14 +*}
    2.15 +(*setup {* KEStore_Elems.add_thes (map swap thydata_list) *}
    2.16 +insert: not found ["IsacKnowledge","Test_Build_Thydata","Theorems","thm111"]*)
    2.17  
    2.18  section {* interface for dialog-authoring *}
    2.19  

     3.1 --- a/src/Tools/isac/calcelems.sml	Fri Jun 06 07:10:26 2014 +0200
     3.2 +++ b/src/Tools/isac/calcelems.sml	Fri Jun 06 14:49:18 2014 +0200
     3.3 @@ -476,6 +476,12 @@
     3.4  			    mathauthors: authors,
     3.5  			    ord: (subst -> (term * term) -> bool)};
     3.6  val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
     3.7 +fun the2str (Html {guh, coursedesign, mathauthors, html}) = guh : string
     3.8 +  | the2str (Hthm {guh, coursedesign, mathauthors, fillpats, thm}) = guh
     3.9 +  | the2str (Hrls {guh, coursedesign, mathauthors, thy_rls}) = guh
    3.10 +  | the2str (Hcal {guh, coursedesign, mathauthors, calc}) = guh
    3.11 +  | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh
    3.12 +fun thes2str thes = map the2str thes |> list2str;
    3.13  
    3.14  type thehier = (thydata ptyp) list;
    3.15  (* required to determine sequence of main nodes of thehier in KEStore.thy *)