1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Fri Jul 28 17:30:20 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Fri Jul 28 18:54:58 2006 +0200
1.3 @@ -22,19 +22,19 @@
1.4 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.5 store_isa ["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"]
1.6 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.7 -store_thm Biegelinie.thy Belastung_Querkraft
1.8 +store_thm Biegelinie.thy ("Belastung_Querkraft", Belastung_Querkraft)
1.9 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.10 -store_thm Biegelinie.thy Moment_Neigung
1.11 +store_thm Biegelinie.thy ("Moment_Neigung", Moment_Neigung)
1.12 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.13 -store_thm Biegelinie.thy Moment_Querkraft
1.14 +store_thm Biegelinie.thy ("Moment_Querkraft", Moment_Querkraft)
1.15 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.16 -store_thm Biegelinie.thy Neigung_Moment
1.17 +store_thm Biegelinie.thy ("Neigung_Moment", Neigung_Moment)
1.18 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.19 -store_thm Biegelinie.thy Querkraft_Belastung
1.20 +store_thm Biegelinie.thy ("Querkraft_Belastung", Querkraft_Belastung)
1.21 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.22 -store_thm Biegelinie.thy Querkraft_Moment
1.23 +store_thm Biegelinie.thy ("Querkraft_Moment", Querkraft_Moment)
1.24 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.25 -store_thm Biegelinie.thy make_fun_explicit
1.26 +store_thm Biegelinie.thy ("make_fun_explicit", make_fun_explicit)
1.27 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.28
1.29
2.1 --- a/src/sml/IsacKnowledge/Isac.ML Fri Jul 28 17:30:20 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Isac.ML Fri Jul 28 18:54:58 2006 +0200
2.3 @@ -27,12 +27,10 @@
2.4
2.5
2.6 (*.create the hierarchy of theory elements from IsacKnowledge
2.7 - (including thms used in rls).*)
2.8 -(*TODO.WN060711 (1) re-engineer this creation and build elements in resp.thy
2.9 - TODO.WN060711 (2) ad [Isabelle,...] from thms collected from rls*)
2.10 + including thms from Isabelle used in rls;
2.11 + elements store_*d in any *.ML are not overwritten.*)
2.12
2.13 -thehier := the_hier [] (collect_thydata ());
2.14 -writeln"";
2.15 +thehier := the_hier (!thehier) (collect_thydata ());
2.16 writeln("----------------------------------\n\
2.17 \*** insert: not found ... IS OK : \n\
2.18 \comes from fill_parents \n\
3.1 --- a/src/sml/xmlsrc/thy-hierarchy.sml Fri Jul 28 17:30:20 2006 +0200
3.2 +++ b/src/sml/xmlsrc/thy-hierarchy.sml Fri Jul 28 18:54:58 2006 +0200
3.3 @@ -155,30 +155,22 @@
3.4
3.5 (*.create the hierarchy from a list (generated automatically);
3.6 thus, missing parents of list-elems are inserted
3.7 - (causing msgs '*** insert: not found') .*)
3.8 -(*TODO.WN060712 insert only if the position is empty !!!*)
3.9 + (causing msgs '*** insert: not found');
3.10 + elemes already store_*d in some *.ML are NOT overwritten.*)
3.11 fun the_hier th ([]: (theID * thydata) list) = th
3.12 - | the_hier th ((theID, thydata)::ths) =
3.13 - if can_insert theID th
3.14 - then let val th' = insrt theID thydata theID th
3.15 - val _ = writeln ("*** insert: perserved " ^ strs2str theID);
3.16 - in the_hier th' ths end
3.17 - else let val th' = fill_parents th theID theID (*..*** insert: not found*)
3.18 - val th' = insrt theID thydata theID th'
3.19 - in the_hier th' ths end;
3.20 -
3.21 -fun the_hier th ([]: (theID * thydata) list) = th
3.22 +(* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ());
3.23 + *)
3.24 | the_hier th ((theID, thydata)::ths) =
3.25 if can_insert theID th
3.26 then let val th' = if exist_the theID th
3.27 - then th (*preserve elements from 'store_thy' in *.ML*)
3.28 + then (writeln ("*** insert: preserved "^strs2str theID);
3.29 + th)
3.30 else insrt theID thydata theID th
3.31 in the_hier th' ths end
3.32 else let val th' = fill_parents th theID theID (*..*** insert: not found*)
3.33 val th' = insrt theID thydata theID th'
3.34 in the_hier th' ths end;
3.35
3.36 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.37
3.38 (*these files shall contain 'invisible' html
3.39 val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)
3.40 @@ -324,9 +316,8 @@
3.41 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.42 thehier := insrt theID the theID (!thehier) end;
3.43
3.44 -fun store_thm thy thm (mathauthors : authors) =
3.45 - let val guh = thm2guh ("IsacKnowledge", theory2thyID thy)
3.46 - (string_of_thm thm)
3.47 +fun store_thm thy (thmID : thmID, thm) (mathauthors : authors) =
3.48 + let val guh = thm2guh ("IsacKnowledge", theory2thyID thy) thmID
3.49 val theID = guh2theID guh
3.50 val the = Hthm {guh = guh,
3.51 coursedesign = [], (*done at xml exported from here*)
4.1 --- a/src/smltest/xmlsrc/thy-hierarchy.sml Fri Jul 28 17:30:20 2006 +0200
4.2 +++ b/src/smltest/xmlsrc/thy-hierarchy.sml Fri Jul 28 18:54:58 2006 +0200
4.3 @@ -17,6 +17,7 @@
4.4 "----------- thm_hier --------------------------------------------";
4.5 "----------- fun thydata2xml -------------------------------------";
4.6 "----------- write xml to tmp ------------------------------------";
4.7 +"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -173,4 +174,63 @@
4.12
4.13 thy_hierarchy2file (path ^ "thy/");
4.14 thes2file (path ^ "thy/");
4.15 -*)
4.16 \ No newline at end of file
4.17 +*)
4.18 +
4.19 +
4.20 +"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
4.21 +"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
4.22 +"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
4.23 +(*
4.24 +store_isa ["Isabelle"] ["THIS SHOULD not BE OBERWRITTEN below"];
4.25 +print_depth 99; get_the ["Isabelle"]; print_depth 3;
4.26 +print_depth 5; thehier; print_depth 3;
4.27 +
4.28 +thehier := the_hier (!thehier) (collect_thydata ());
4.29 +print_depth 99; get_the ["Isabelle"]; print_depth 3;
4.30 +print_depth 5; thehier; print_depth 3;
4.31 +*)
4.32 +
4.33 +case get_the ["IsacKnowledge", "Biegelinie", "Theorems"] of
4.34 + Html {mathauthors =
4.35 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()
4.36 + | _ => raise error "thy-hierarchy.sml: store_isa overwritten";
4.37 +
4.38 +case get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"] of
4.39 + Hthm {mathauthors =
4.40 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()
4.41 + | _ => raise error "thy-hierarchy.sml: store_isa overwritten";
4.42 +
4.43 +(*
4.44 +print_depth 7;
4.45 +get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"];
4.46 +print_depth 3;
4.47 +*)
4.48 +
4.49 +(*WN060728 strange behaviour:
4.50 +### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ...
4.51 +
4.52 +val it = () : unit
4.53 +*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
4.54 +*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
4.55 +*** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]
4.56 +*** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]
4.57 +*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
4.58 +*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]
4.59 +*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
4.60 +*** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]
4.61 +*** insert: preserved ["IsacScripts","ListG","Theorems","induct"]
4.62 +*** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]
4.63 +*** insert: preserved ["IsacScripts","ListG","Theorems","simps_2"]
4.64 +val it = () : unit
4.65 +
4.66 +### but those store_*d in Biegelinie.ML are NOT reported !?!?!?!?!?!?!
4.67 +### however, '*** insert: not found' is NOT reported below, too....
4.68 +
4.69 +----------------------------------
4.70 +*** insert: not found ... IS OK :
4.71 +comes from fill_parents
4.72 +----------------------------------
4.73 +
4.74 +val it = () : unit
4.75 +*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]
4.76 +*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]*)