PIDE: (Knowledge-)Context works also for met FINALLY
authorWalther Neuper <wneuper@ist.tugraz.at>
Tue, 06 Oct 2015 15:51:10 +0200
changeset 591768532cda27fbf
parent 59175 3d1000bbd475
child 59177 1ff126aa8445
PIDE: (Knowledge-)Context works also for met FINALLY

There was another error lurking behind the first one,
c.f. isac-java b1c943da612b
src/Tools/isac/xmlsrc/datatypes.sml
test/Tools/isac/ADDTESTS/libisabelle/protocol.sml
     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