1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -80,8 +80,8 @@
1.4 autx (j + i) auts ^
1.5 indt j ^ "</"^str^">\n" : xml
1.6 end;
1.7 -(* tracing(authors2xml 2 "MATHAUTHORS" []);
1.8 - tracing(authors2xml 2 "MATHAUTHORS"
1.9 +(* writeln(authors2xml 2 "MATHAUTHORS" []);
1.10 + writeln(authors2xml 2 "MATHAUTHORS"
1.11 ["isac-team 2001", "Richard Lang 2003"]);
1.12 *)
1.13
1.14 @@ -92,7 +92,7 @@
1.15 in (indt j) ^ "<STRINGLIST>\n" ^
1.16 (id2x (j + indentation) ids) ^
1.17 (indt j) ^ "</STRINGLIST>\n" end;
1.18 -(* tracing(id2xml 8 ["linear","univariate","equation"]);
1.19 +(* writeln(id2xml 8 ["linear","univariate","equation"]);
1.20 <STRINGLIST>
1.21 <STRING>linear</STRING>
1.22 <STRING>univariate</STRING>
1.23 @@ -106,7 +106,7 @@
1.24 in (indt j) ^ "<INTLIST>\n" ^
1.25 (int2x (j + i) ids) ^
1.26 (indt j) ^ "</INTLIST>\n" end;
1.27 -(* tracing(ints2xml 3 [1,2,3]);
1.28 +(* writeln(ints2xml 3 [1,2,3]);
1.29 *)
1.30
1.31
1.32 @@ -122,18 +122,18 @@
1.33 ints2xml (j+i) pos ^
1.34 pos_2xml (j+i) pos_ ^
1.35 indt (j) ^ "</" ^ tag ^ ">\n";
1.36 -(* tracing(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
1.37 +(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
1.38 *)
1.39
1.40 fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
1.41 indt j ^ "<FORMULA>\n"^
1.42 term2xml j term ^"\n"^
1.43 indt j ^ "</FORMULA>\n" : xml;
1.44 -(* tracing(formula2xml 6 (str2term "1+1=2"));
1.45 +(* writeln(formula2xml 6 (str2term "1+1=2"));
1.46 *)
1.47 fun formulae2xml j [] = ("":xml)
1.48 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
1.49 -(* tracing(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
1.50 +(* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
1.51 *)
1.52
1.53 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
1.54 @@ -144,11 +144,11 @@
1.55 term2xml (j+i) term ^"\n"^
1.56 indt (j+i) ^ "</FORMULA>\n"^
1.57 indt j ^ "</POSFORM>\n" : xml;
1.58 -(* tracing(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
1.59 +(* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
1.60 *)
1.61 fun posforms2xml j [] = ("":xml)
1.62 | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;
1.63 -(* tracing(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
1.64 +(* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
1.65 *)
1.66
1.67 fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
1.68 @@ -172,7 +172,7 @@
1.69 (*.for creating a href for a rule within an rls's rule list;
1.70 the guh points to the thy of definition of the rule, NOT of use in rls.*)
1.71 fun rule2xml j (thyID:thyID) Erule =
1.72 - raise error "rule2xml called with 'Erule'"
1.73 + error "rule2xml called with 'Erule'"
1.74 (* val (j, thyID, Thm (thmID, thm)) = (j+i, thyID, nth 1 rules);
1.75 val (j, thyID, Thm (thmID, thm)) = (j, thyID,r);
1.76 *)
1.77 @@ -217,7 +217,7 @@
1.78 in filt end;
1.79
1.80 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
1.81 -(*WN.25.8.03: pattern2xml different output with TextIO | tracing !!!
1.82 +(*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
1.83 the version below is for TextIO: terms2xml makes \n !*)
1.84 (* val (j, p, where_) = (i, ppc, where_);
1.85 *)
1.86 @@ -244,7 +244,7 @@
1.87 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
1.88 (indt j) ^ "</RELATE>\n");
1.89 (*
1.90 -tracing(pattern2xml 3 ((#ppc o get_pbt)
1.91 +writeln(pattern2xml 3 ((#ppc o get_pbt)
1.92 ["squareroot","univariate","equation","test"]) []);
1.93 *)
1.94
1.95 @@ -318,7 +318,7 @@
1.96 (indt (j+i)) ^ "</RELATE>\n")^
1.97 indt j ^"</MODEL>\n"):xml
1.98 end;
1.99 -(* tracing(model2xml 3 itms []);
1.100 +(* writeln(model2xml 3 itms []);
1.101 *)
1.102
1.103 fun spec2xml j ((dI,pI,mI):spec) =
1.104 @@ -344,7 +344,7 @@
1.105 | _ => "Und")^" </BELONGSTO>\n"^
1.106 spec2xml (j+i) spec ^
1.107 indt j ^"</CALCHEAD>\n"):xml;
1.108 -(* tracing (modspec2xml 2 e_ocalhd);
1.109 +(* writeln (modspec2xml 2 e_ocalhd);
1.110 *)
1.111 fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
1.112 (indt j ^"<CALCHEAD status = "^
1.113 @@ -376,14 +376,14 @@
1.114 indt j ^"</SUBSTITUTION>\n"):xml;
1.115 (* val subs = [(str2term "bdv", str2term "x")];
1.116 val subs = ["(bdv, x)"];
1.117 - tracing(subs2xml 0 subs);
1.118 + writeln(subs2xml 0 subs);
1.119 *)
1.120 fun subst2xml j (subst:subst) =
1.121 (indt j ^"<SUBSTITUTION>\n"^
1.122 foldl op^ ("", map (sub2xml (j+i)) subst) ^
1.123 indt j ^"</SUBSTITUTION>\n"):xml;
1.124 (* val subst = [(str2term "bdv", str2term "x")];
1.125 - tracing(subst2xml 0 subst);
1.126 + writeln(subst2xml 0 subst);
1.127 *)
1.128
1.129 (* val (j, str) = ((j+i), form);
1.130 @@ -568,7 +568,7 @@
1.131 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
1.132 thm'2xml (j+i) thm'^
1.133 indt j ^"</REWRITETACTIC>\n"):xml
1.134 -(* tracing (tac2xml 2 (Rewrite ("all_left",
1.135 +(* writeln (tac2xml 2 (Rewrite ("all_left",
1.136 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
1.137 val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);
1.138 *)
1.139 @@ -577,7 +577,7 @@
1.140 subs2xml (j+i) subs^
1.141 thm'2xml (j+i) thm'^
1.142 indt j ^"</REWRITEINSTTACTIC>\n"):xml
1.143 -(* tracing (tac2xml 2 (Rewrite_Inst
1.144 +(* writeln (tac2xml 2 (Rewrite_Inst
1.145 (["(bdv,x)"],
1.146 ("all_left",
1.147 "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
1.148 @@ -609,7 +609,7 @@
1.149 id2xml (j+i) pI^
1.150 indt j ^"</STRINGLISTTACTIC>\n"):xml
1.151
1.152 - | tac2xml j tac = raise error ("tac2xml: not impl. for "^tac2str tac);
1.153 + | tac2xml j tac = error ("tac2xml: not impl. for "^tac2str tac);
1.154
1.155 fun tacs2xml j [] = "":xml
1.156 | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
1.157 @@ -698,10 +698,10 @@
1.158 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
1.159 asms, lhs, rhs, result, resasms, asmrls}) =
1.160 (context_thy (pt,pos) tac);
1.161 -tracing (contthy2xml 2 (context_thy (pt,pos) tac));
1.162 +writeln (contthy2xml 2 (context_thy (pt,pos) tac));
1.163 *)
1.164 fun contthy2xml j EContThy =
1.165 - raise error "contthy2xml called with EContThy"
1.166 + error "contthy2xml called with EContThy"
1.167 | contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
1.168 asms,lhs, rhs, result, resasms, asmrls}) =
1.169 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^