PIDE-phase 2c: Protocol is stable with minimal changes
authorWalther Neuper <wneuper@ist.tugraz.at>
Tue, 18 Aug 2015 17:39:47 +0200
changeset 59163636013c7949f
parent 59162 6a69fb432973
child 59164 9c50384e9804
PIDE-phase 2c: Protocol is stable with minimal changes

cf. https://github.com/wneuper/libisabelle/commit/c17860fb3a549bd4e8e97f2d757b410157c8487a
and few predecessors.
src/Tools/isac/xmlsrc/interface-xml.sml
src/Tools/isac/xmlsrc/mathml.sml
     1.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml	Sat Aug 15 16:03:53 2015 +0200
     1.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml	Tue Aug 18 17:39:47 2015 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4  	     "</GETASSUMPTIONS>\n" ^
     1.5  	     "@@@@@end@@@@@");
     1.6  fun getasmsOK2xml (calcid : calcID) terms = 
     1.7 -  XML.Elem (("APPLICABLETACTICS", []), [
     1.8 +  XML.Elem (("ASSUMPTIONS", []), [
     1.9      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.10      XML.Elem (("ASMLIST", []), (map xml_of_formula terms))])
    1.11  
    1.12 @@ -290,9 +290,8 @@
    1.13  	     "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
    1.14  	     "@@@@@end@@@@@");
    1.15  fun appendformulaERROR2xml (calcid : calcID) e = 
    1.16 -  XML.Elem (("CALCMESSAGE", []), [
    1.17 -    (*XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.18 -      WN150530: before change to PIDE worked without cI ?!? FIXXME*)
    1.19 +  XML.Elem (("APPENDFORMULA", []), [
    1.20 +    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.21      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
    1.22  
    1.23  fun replaceformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
    1.24 @@ -313,9 +312,8 @@
    1.25  	     "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
    1.26  	     "@@@@@end@@@@@");
    1.27  fun replaceformulaERROR2xml (calcid : calcID) e = 
    1.28 -  XML.Elem (("CALCMESSAGE", []), [
    1.29 -    (*XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.30 -      WN150530: before change to PIDE worked without cI ?!? FIXXME*)
    1.31 +  XML.Elem (("REPLACEFORMULA", []), [
    1.32 +    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.33      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
    1.34  
    1.35  fun message2xml (cI:calcID) e = 
    1.36 @@ -402,9 +400,8 @@
    1.37  	     "<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
    1.38  	     "@@@@@end@@@@@");
    1.39  fun autocalculateERROR2xml (calcid : calcID) e = 
    1.40 -  XML.Elem (("CALCMESSAGE", []), [
    1.41 -    (*XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.42 -      WN150530: before change to PIDE worked without cI ?!? FIXXME*)
    1.43 +  XML.Elem (("AUTOCALC", []), [
    1.44 +    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.45      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
    1.46  
    1.47  fun interStepsOK (cI:calcID) (old:pos') (del:pos') (new:pos') =
    1.48 @@ -425,9 +422,8 @@
    1.49  	     "  <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
    1.50  	     "@@@@@end@@@@@");
    1.51  fun interStepsERROR (calcid : calcID) e = 
    1.52 -  XML.Elem (("CALCMESSAGE", []), [
    1.53 -    (*XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.54 -      WN150530: before change to PIDE worked without cI ?!? FIXXME*)
    1.55 +  XML.Elem (("INTERSTEPS", []), [
    1.56 +    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.57      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
    1.58  
    1.59  fun calcMessage2xml (cI:calcID) e =
     2.1 --- a/src/Tools/isac/xmlsrc/mathml.sml	Sat Aug 15 16:03:53 2015 +0200
     2.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml	Tue Aug 18 17:39:47 2015 +0200
     2.3 @@ -35,13 +35,13 @@
     2.4  in
     2.5  fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
     2.6    | xmlstr i (XML.Elem ((str, []), trees)) = 
     2.7 -    indent i ^ "<" ^ str ^ ">" ^ "\n" ^
     2.8 +    indent i ^ "(" ^ str ^ ")" ^ "\n" ^
     2.9        List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
    2.10 -    indent i ^ "</" ^ str ^ ">" ^ "\n"
    2.11 +    indent i ^ "(/" ^ str ^ ")" ^ "\n"
    2.12    | xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) = 
    2.13 -    indent i ^ "<" ^ str ^ " " ^ flag ^ "=" ^ value  ^ ">" ^ "\n" ^
    2.14 +    indent i ^ "(" ^ str ^ " " ^ flag ^ "=" ^ value  ^ ")" ^ "\n" ^
    2.15        List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
    2.16 -    indent i ^ "</" ^ str ^ ">" ^ "\n"
    2.17 +    indent i ^ "(/" ^ str ^ ")" ^ "\n"
    2.18    | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) = 
    2.19      error "xmlstr: TODO review attribute \"status\" etc";
    2.20  end