1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Tue Oct 06 09:34:43 2015 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Tue Oct 06 15:51:10 2015 +0200
1.3 @@ -585,13 +585,13 @@
1.4 | scr2xml j (Rfuns _) =
1.5 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
1.6 fun xml_of_src EmptyScr =
1.7 - XML.Elem (("SCRIPT", []), [XML.Text "empty_script"])
1.8 + XML.Elem (("NOCODE", []), [XML.Text "empty"])
1.9 | xml_of_src (Prog term) =
1.10 - XML.Elem (("SCRIPT", []), [
1.11 - if term = e_term then xml_of_src EmptyScr
1.12 - else XML.Elem (("SCRIPT", []), [xml_of_term (inst_abs (assoc_thy "Isac") term)])])
1.13 + XML.Elem (("CODE", []), [
1.14 + if term = e_term then xml_of_src EmptyScr
1.15 + else xml_of_term (inst_abs (assoc_thy "Isac") term)])
1.16 | xml_of_src (Rfuns _) =
1.17 - XML.Elem (("REVERSREWRITE", []), [XML.Text "reverse rewrite functions"])
1.18 + XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
1.19
1.20 fun prepa12xml j (terms, term) =
1.21 indt j ^"<PREPAT>\n"^
2.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Tue Oct 06 09:34:43 2015 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Tue Oct 06 15:51:10 2015 +0200
2.3 @@ -5,7 +5,7 @@
2.4 theory Test_Some imports Build_Thydata begin
2.5 ML {* KEStore_Elems.set_ref_thy @{theory};
2.6 fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
2.7 -ML_file "~~/test/Tools/isac/xmlsrc/protocol.sml"
2.8 +ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
2.9 *)
2.10
2.11 (* NOTE: Protocol.thy still belongs to a different development at