1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Fri Aug 20 17:18:59 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Mon Aug 23 11:05:54 2010 +0200
1.3 @@ -44,10 +44,31 @@
1.4 use "ME/inform.sml"
1.5 use "ME/mathengine.sml"
1.6
1.7 +use "xmlsrc/mathml.sml"
1.8 +use "xmlsrc/datatypes.sml"
1.9 +use "xmlsrc/pbl-met-hierarchy.sml"
1.10 +use "xmlsrc/thy-hierarchy.sml"
1.11 +
1.12 +ML {*
1.13 +@{theory "Script"};
1.14 +(theory "Script");
1.15 +*}
1.16 +
1.17 +use "xmlsrc/interface-xml.sml"
1.18 +
1.19 +ML {*
1.20 +Thm.get_name_hint @{thm refl};
1.21 +Thm.get_kind @{thm refl};
1.22 +*}
1.23 +
1.24 +
1.25 +
1.26 +
1.27 ML {*
1.28 -val thy = @{theory "Script"};
1.29 +Thm.derivation_name @{thm sym};
1.30 +subtract op = [1,2,3] [3,4,5];
1.31 +*}
1.32
1.33 -*}
1.34
1.35 ML {*
1.36 val thy = @{theory "Script"};
1.37 @@ -56,11 +77,6 @@
1.38
1.39 (*
1.40
1.41 -use "xmlsrc/mathml.sml"
1.42 -use "xmlsrc/datatypes.sml"
1.43 -use "xmlsrc/pbl-met-hierarchy.sml"
1.44 -use "xmlsrc/thy-hierarchy.sml"
1.45 -use "xmlsrc/interface-xml.sml"
1.46
1.47 use "FE-interface/messages.sml"
1.48 use "FE-interface/states.sml"
2.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Fri Aug 20 17:18:59 2010 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Aug 23 11:05:54 2010 +0200
2.3 @@ -6,6 +6,7 @@
2.4 use"datatypes.sml";
2.5 *)
2.6
2.7 +
2.8 signature DATATYPES =
2.9 sig
2.10 val authors2xml : int -> string -> string list -> xml
2.11 @@ -62,6 +63,7 @@
2.12
2.13 (*------------------------------------------------------------------*)
2.14 structure datatypes:DATATYPES =
2.15 +(*structure datatypes =*)
2.16 struct
2.17 (*------------------------------------------------------------------*)
2.18
2.19 @@ -401,11 +403,10 @@
2.20 (*WN060627 scope of thy's not considered ?!?*)
2.21 fun thm''2xml j (thm:thm) =
2.22 indt j ^"<THEOREM>\n"^
2.23 - indt (j+i) ^"<ID> "^ (strip_thy o Thm.name_of_thm) thm ^" </ID>\n"^
2.24 + indt (j+i) ^"<ID> "^ (strip_thy o Thm.get_name_hint) thm ^" </ID>\n"^
2.25 term2xml j ((#prop o rep_thm) thm) ^ "\n" ^
2.26 indt j ^"</THEOREM>\n":xml;
2.27
2.28 -
2.29 fun scr2xml j EmptyScr =
2.30 indt j ^"<SCRIPT> </SCRIPT>\n" : xml
2.31 | scr2xml j (Script term) =
2.32 @@ -504,7 +505,6 @@
2.33 indt (j+i) ^" </SCRIPT>\n"^
2.34 indt j ^"</RULESET>\n" : xml;
2.35
2.36 -
2.37 (*.convert a tactic into xml-format
2.38 ATTENTION: WN060513 detected faulty 'cterm2xml's with 'string's as args.*)
2.39 fun tac2xml j (Subproblem (dI, pI)) =
2.40 @@ -593,8 +593,7 @@
2.41 indt j ^"</REWRITESETINSTTACTIC>\n"):xml
2.42
2.43 | tac2xml j (Or_to_List) =
2.44 - (indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> \
2.45 - \</STRINGLISTTACTIC>\n"):xml
2.46 + (indt j ^"<STRINGLISTTACTIC name=\"Or_to_List\"> </STRINGLISTTACTIC>\n"):xml
2.47 | tac2xml j (Check_elementwise ct) =
2.48 (indt j ^"<SIMPLETACTIC name=\"Check_elementwise\">\n"^
2.49 cterm2xml (j+i) ct ^ "\n"^
2.50 @@ -629,7 +628,7 @@
2.51 fun posformheads2xml j [] = ("":xml)
2.52 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
2.53
2.54 -val e_pblterm = (term_of o the o (parse (assoc_thy "Script.thy")))
2.55 +val e_pblterm = (term_of o the o (parse (theory "Script")))
2.56 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
2.57
2.58 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
2.59 @@ -696,7 +695,6 @@
2.60 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
2.61 indt j ^ "</EXTREF>\n" : xml;
2.62
2.63 -
2.64 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
2.65 asms, lhs, rhs, result, resasms, asmrls}) =
2.66 (context_thy (pt,pos) tac);
2.67 @@ -707,6 +705,7 @@
2.68 | contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
2.69 asms,lhs, rhs, result, resasms, asmrls}) =
2.70 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
2.71 +
2.72 indt j ^ "<APPLTO>\n" ^
2.73 term2xml j applto ^ "\n" ^
2.74 indt j ^ "</APPLTO>\n" ^
2.75 @@ -740,7 +739,6 @@
2.76 indt j ^ "<EVALRLS>\n" ^
2.77 theref2xml j thyID "Rulesets" asmrls ^
2.78 indt j ^ "</EVALRLS>\n"
2.79 -
2.80 | contthy2xml j (ContThmInst{thyID, thm, bdvs, thminst, applto, applat,
2.81 reword, asms, lhs, rhs, result, resasms,
2.82 asmrls}) =
2.83 @@ -836,8 +834,9 @@
2.84 term2xml j applto ^ "\n" ^
2.85 indt j ^ "</APPLTO>\n" : xml;
2.86
2.87 -
2.88 (*------------------------------------------------------------------*)
2.89 end
2.90 open datatypes;
2.91 (*------------------------------------------------------------------*)
2.92 +
2.93 +
3.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Fri Aug 20 17:18:59 2010 +0200
3.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Aug 23 11:05:54 2010 +0200
3.3 @@ -45,7 +45,7 @@
3.4
3.5 fun collect_thms' (part, thy') =
3.6 let val thy = assoc_thy (thyID2theory' thy')
3.7 - in map (makeHthm (part, thy')) (thms_of thy) end;
3.8 + in map (makeHthm (part, thy')) (PureThy.all_thms_of thy) end;
3.9
3.10 (*.collect all rulesets defined in in a theory and insert the guh.*)
3.11 fun collect_rlss (part, thy') =
3.12 @@ -91,10 +91,11 @@
3.13 this list is used by 'fun the_hier' to create the hierarchy .*)
3.14 fun collect_thydata () =
3.15 let val isab_thms = map rearrange_inv (!isab_thm_thy)
3.16 - val scri_thys = (map (get_thy o #1) (!script_thys))
3.17 - \\ ["e_domID"]
3.18 - val isac_thys = (map (get_thy o #1)
3.19 - (!theory')) \\ scri_thys \\ ["e_domID"]
3.20 + val scri_thys =
3.21 + subtract op = ["e_domID"] (map (get_thy o #1) (!script_thys))
3.22 + val isac_thys =
3.23 + subtract op = ["e_domID"]
3.24 + (subtract op = scri_thys (map (get_thy o #1) (!theory')))
3.25 in [isabelle_page] @
3.26 (map (collect_isab "Isabelle") isab_thms) @
3.27 ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @