1.1 --- a/src/sml/ROOT.ML Wed Nov 03 15:50:40 2004 +0100
1.2 +++ b/src/sml/ROOT.ML Fri Nov 12 15:30:14 2004 +0100
1.3 @@ -58,12 +58,12 @@
1.4 cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux
1.5 cp HOL-Real HOL-Real-Isac
1.6 /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
1.7 - cd"/home/neuper/develop/sml";
1.8 + cd"/home/neuper/proto2/isac/src/sml";
1.9 use"ROOT.ML";
1.10
1.11 ##############dev-start######################################################
1.12 /usr/local/Isabelle2002/bin/isabelle HOL-Real
1.13 - cd"/home/neuper/develop/sml";
1.14 + cd"/home/neuper/proto2/isac/src/sml";
1.15 use"ROOT.ML";
1.16
1.17 Compiler.Control.Print.printDepth:=9; (*4 default*)
2.1 --- a/src/sml/xmlsrc/datatypes.sml Wed Nov 03 15:50:40 2004 +0100
2.2 +++ b/src/sml/xmlsrc/datatypes.sml Fri Nov 12 15:30:14 2004 +0100
2.3 @@ -205,12 +205,14 @@
2.4 fun pos_2xml j pos_ =
2.5 (indt j) ^ "<POS> " ^ pos_2str pos_ ^ " </POS>\n";
2.6
2.7 -fun pos'2xml j (pos, pos_) =
2.8 - indt j ^ "<POSITION>\n" ^
2.9 +(*.due to specialties of isac/util/parser/XMLParseDigest.java
2.10 + pos' requires different tags.*)
2.11 +fun pos'2xml j (tag, (pos, pos_)) =
2.12 + indt j ^ "<" ^ tag ^ ">\n" ^
2.13 ints2xml (j + i) pos ^
2.14 pos_2xml (j + i) pos_ ^
2.15 - indt j ^ "</POSITION>\n";
2.16 -(* writeln(pos'2xml 3 ([1,2,3], Pbl));
2.17 + indt j ^ "</" ^ tag ^ ">\n";
2.18 +(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
2.19 *)
2.20
2.21
2.22 @@ -318,7 +320,7 @@
2.23 | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
2.24
2.25
2.26 -fun pos'form2xml j ("stepform", p:pos', f) =
2.27 +fun pos'form2xml j ("stepform", p:string * pos', f) =
2.28 indt j ^"<STEPFORMULA>\n"^
2.29 pos'2xml (j+i) p ^
2.30 term2xml j f^"\n"^
3.1 --- a/src/sml/xmlsrc/interface-xml.sml Wed Nov 03 15:50:40 2004 +0100
3.2 +++ b/src/sml/xmlsrc/interface-xml.sml Fri Nov 12 15:30:14 2004 +0100
3.3 @@ -60,7 +60,7 @@
3.4 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.5 \<REFFORMULA>\n\
3.6 \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
3.7 - pos'2xml i p ^
3.8 + pos'2xml i ("POSITION", p) ^
3.9 " <FORMULA>\n"^
3.10 (term2xml i t)^"\n"^
3.11 " </FORMULA>\n\
3.12 @@ -68,11 +68,11 @@
3.13 \@@@@@end@@@@@")
3.14 | refformulaOK2xml (cI:calcID) p (ModSpec modspec) =
3.15 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.16 - \<REFFORMULA>\n\
3.17 + \<REFCALCHEAD>\n\
3.18 \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
3.19 - pos'2xml i p ^
3.20 + pos'2xml i ("POSITION", p) ^
3.21 modspec2xml i modspec^
3.22 - "</REFFORMULA>\n\
3.23 + "</REFCALCHEAD>\n\
3.24 \@@@@@end@@@@@");
3.25
3.26 fun refformulaERROR2xml (cI:calcID) = (*FIXME.WN.29.8.03 unused*)
3.27 @@ -101,17 +101,15 @@
3.28 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.29 \<APPENDFORMULA>\n\
3.30 \ <CALCID> "^string_of_int cI^" </CALCID>\n\
3.31 - \ <UNCHANGED>\n"^
3.32 - pos'2xml (2*i) old ^
3.33 - " </UNCHANGED>\n\
3.34 - \ <DELETED>\n"^
3.35 - pos'2xml (2*i) del ^
3.36 - " </DELETED>\n\
3.37 - \ <GENERATED>\n"^
3.38 - pos'2xml (2*i) new ^
3.39 - " </GENERATED>\n\
3.40 + \ <CALCCHANGED>\n" ^
3.41 + pos'2xml (2*i) ("UNCHANGED", old) ^
3.42 + pos'2xml (2*i) ("DELETED", del) ^
3.43 + pos'2xml (2*i) ("GENERATED", new) ^
3.44 + " </CALCCHANGED>\n\
3.45 \</APPENDFORMULA>\n\
3.46 \@@@@@end@@@@@");
3.47 +(* appendformulaOK2xml 1 ([2],Frm) ([3],Pbl) ([4],Res);
3.48 + *)
3.49 fun appendformulaERROR2xml (cI:calcID) msg =
3.50 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.51 \<APPENDFORMULA>\n\
3.52 @@ -124,15 +122,11 @@
3.53 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.54 \<REPLACEFORMULA>\n\
3.55 \ <CALCID> "^string_of_int cI^" </CALCID>\n\
3.56 - \ <UNCHANGED>\n"^
3.57 - pos'2xml (2*i) old ^
3.58 - " </UNCHANGED>\n\
3.59 - \ <DELETED>\n"^
3.60 - pos'2xml (2*i) del ^
3.61 - " </DELETED>\n\
3.62 - \ <GENERATED>\n"^
3.63 - pos'2xml (2*i) new ^
3.64 - " </GENERATED>\n\
3.65 + \ <CALCCHANGED>\n" ^
3.66 + pos'2xml (2*i) ("UNCHANGED", old) ^
3.67 + pos'2xml (2*i) ("DELETED", del) ^
3.68 + pos'2xml (2*i) ("GENERATED", new) ^
3.69 + " </CALCCHANGED>\n\
3.70 \</REPLACEFORMULA>\n\
3.71 \@@@@@end@@@@@");
3.72 fun replaceformulaERROR2xml (cI:calcID) msg =
3.73 @@ -177,15 +171,11 @@
3.74 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.75 \<AUTOCALC>\n\
3.76 \ <CALCID> "^string_of_int cI^" </CALCID>\n\
3.77 - \ <UNCHANGED>\n"^
3.78 - pos'2xml (2*i) old ^
3.79 - " </UNCHANGED>\n\
3.80 - \ <DELETED>\n"^
3.81 - pos'2xml (2*i) del ^
3.82 - " </DELETED>\n\
3.83 - \ <GENERATED>\n"^
3.84 - pos'2xml (2*i) new ^
3.85 - " </GENERATED>\n\
3.86 + \ <CALCCHANGED>\n" ^
3.87 + pos'2xml (2*i) ("UNCHANGED", old) ^
3.88 + pos'2xml (2*i) ("DELETED", del) ^
3.89 + pos'2xml (2*i) ("GENERATED", new) ^
3.90 + " </CALCCHANGED>\n\
3.91 \</AUTOCALC>\n\
3.92 \@@@@@end@@@@@");
3.93 (* autocalculate2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
3.94 @@ -201,17 +191,12 @@
3.95 fun detailStepOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =
3.96 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
3.97 \<DETAILSTEP>\n\
3.98 - \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
3.99 - (*pos'forms2xml i pos'forms^*)
3.100 - " <UNCHANGED>\n"^
3.101 - pos'2xml (2*i) old ^
3.102 - " </UNCHANGED>\n\
3.103 - \ <DELETED>\n"^
3.104 - pos'2xml (2*i) del ^
3.105 - " </DELETED>\n\
3.106 - \ <GENERATED>\n"^
3.107 - pos'2xml (2*i) new ^
3.108 - " </GENERATED>\n\
3.109 + \ <CALCID> "^string_of_int cI^" </CALCID>\n\
3.110 + \ <CALCCHANGED>\n" ^
3.111 + pos'2xml (2*i) ("UNCHANGED", old) ^
3.112 + pos'2xml (2*i) ("DELETED", del) ^
3.113 + pos'2xml (2*i) ("GENERATED", new) ^
3.114 + " </CALCCHANGED>\n\
3.115 \</DETAILSTEP>\n\
3.116 \@@@@@end@@@@@");
3.117 fun detailStepERROR (cI:calcID) e =