wneuper/isa: comparison src/Tools/isac/xmlsrc/datatypes.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 			     (autx j ss)
 in indt j ^ "<"^str^">\n" ^
 autx (j + i) auts ^
 indt j ^ "</"^str^">\n" : xml
 end;
-(* tracing(authors2xml 2 "MATHAUTHORS" []);
+(* writeln(authors2xml 2 "MATHAUTHORS" []);
-tracing(authors2xml 2 "MATHAUTHORS"
+writeln(authors2xml 2 "MATHAUTHORS"
 		       ["isac-team 2001", "Richard Lang 2003"]);
 *)
 fun id2xml j ids =
 let fun id2x _ [] = ""
 	  | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
 			     (id2x j ss)
 in (indt j) ^ "<STRINGLIST>\n" ^
 (id2x (j + indentation) ids) ^
 (indt j) ^ "</STRINGLIST>\n" end;
-(* tracing(id2xml 8 ["linear","univariate","equation"]);
+(* writeln(id2xml 8 ["linear","univariate","equation"]);
 <STRINGLIST>
 <STRING>linear</STRING>
 <STRING>univariate</STRING>
 <STRING>equation</STRING>
 </STRINGLIST>*)
 	  | int2x j (s::ss) = (indt j) ^"<INT> "^ string_of_int s ^" </INT>\n"^
 			     (int2x j ss)
 in (indt j) ^ "<INTLIST>\n" ^
 (int2x (j + i) ids) ^
 (indt j) ^ "</INTLIST>\n" end;
-(* tracing(ints2xml 3 [1,2,3]);
+(* writeln(ints2xml 3 [1,2,3]);
 *)
 (** isac datatypes **)
 fun pos'2xml j (tag, (pos, pos_)) =
 indt     (j) ^ "<" ^ tag ^ ">\n" ^
 ints2xml (j+i) pos ^
 pos_2xml (j+i) pos_ ^
 indt     (j) ^ "</" ^ tag ^ ">\n";
-(* tracing(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
+(* writeln(pos'2xml 3 ("POSITION", ([1,2,3], Pbl)));
 *)
 fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
 indt j ^ "<FORMULA>\n"^
 term2xml j term ^"\n"^
 indt j ^ "</FORMULA>\n" : xml;
-(* tracing(formula2xml 6 (str2term "1+1=2"));
+(* writeln(formula2xml 6 (str2term "1+1=2"));
 *)
 fun formulae2xml j [] = ("":xml)
 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
-(* tracing(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
+(* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
 *)
 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
 fun posform2xml j (p:pos', term) =
 indt j ^     "<POSFORM>\n" ^
 pos'2xml (j+i) ("POSITION", p) ^
 indt     (j+i) ^ "<FORMULA>\n"^
 term2xml (j+i) term ^"\n"^
 indt     (j+i) ^ "</FORMULA>\n"^
 indt j ^     "</POSFORM>\n" : xml;
-(* tracing(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
+(* writeln(posform2xml 6 (([1,2],Frm), str2term "1+1=2"));
 *)
 fun posforms2xml j [] = ("":xml)
 | posforms2xml j (r::rs) = posform2xml j r ^ posforms2xml j rs;
-(* tracing(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
+(* writeln(posforms2xml 6 [(([1],Res), str2term "1+1=2"),(([2],Res), str2term "1+1+1=3")]);
 *)
 fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
 indt j ^ "<CALCREF>\n" ^
 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
 indt j ^ "</CALC>\n" : xml;
 (*.for creating a href for a rule within an rls's rule list;
 the guh points to the thy of definition of the rule, NOT of use in rls.*)
 fun rule2xml j (thyID:thyID) Erule =
-raise error "rule2xml called with 'Erule'"
+error "rule2xml called with 'Erule'"
 (* val (j, thyID, Thm (thmID, thm)) = (j+i, thyID, nth 1 rules);
 val (j, thyID, Thm (thmID, thm)) = (j, thyID,r);
 *)
 | rule2xml j thyID (Thm (thmID, thm)) =
 indt j ^ "<RULE>\n" ^
 | filt ((s, (t1, t2)) :: ps) =
 	  if str = s then (t1 $ t2) :: filt ps else filt ps
 in filt end;
 (*FIXME.WN040831 model2xml <--?--> pattern2xml*)
-(*WN.25.8.03: pattern2xml different output with TextIO | tracing !!!
+(*WN.25.8.03: pattern2xml different output with TextIO | writeln !!!
 the version below is for TextIO: terms2xml makes \n !*)
 (* val (j, p, where_) = (i, ppc, where_);
 *)
 fun pattern2xml j p where_ =
 (case filterpbl "#Given" p of
 (case filterpbl "#Relate" p of
 	 [] =>  (indt j) ^ "<RELATE>  </RELATE>\n"
 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
 		(indt j) ^ "</RELATE>\n");
 (*
-tracing(pattern2xml 3 ((#ppc o get_pbt)
+writeln(pattern2xml 3 ((#ppc o get_pbt)
 			 ["squareroot","univariate","equation","test"]) []);
 *)
 (*see itm_2item*)
 fun itm_2xml j (Cor (dts,_))=
 	     [] =>  (indt (j+i)) ^ "<RELATE>  </RELATE>\n"
 	   | res => (indt (j+i)) ^ "<RELATE>\n" ^ itms2xml (j+2*i) res ^
 		    (indt (j+i)) ^ "</RELATE>\n")^
 	    indt j ^"</MODEL>\n"):xml
 end;
-(* tracing(model2xml 3 itms []);
+(* writeln(model2xml 3 itms []);
 *)
 fun spec2xml j ((dI,pI,mI):spec) =
 (indt j ^"<SPECIFICATION>\n"^
 indt (j+i) ^"<THEORYID> "^ dI ^" </THEORYID>\n"^
 indt (j+i) ^"<BELONGSTO> "^(case p_ of Pbl => "Pbl"
 					  | Met => "Met"
 					  | _ => "Und")^" </BELONGSTO>\n"^
 spec2xml (j+i) spec ^
 indt j ^"</CALCHEAD>\n"):xml;
-(* tracing (modspec2xml 2 e_ocalhd);
+(* writeln (modspec2xml 2 e_ocalhd);
 *)
 fun pos'calchead2xml j (p:pos', (b, p_, head, gfr, pre, spec): ocalhd) =
 (indt j ^"<CALCHEAD status = "^
 quote (if b then "correct" else "incorrect")^">\n"^
 pos'2xml (j+i) ("POSITION", p) ^
 foldl op^ ("", map (sub2xml (j+i))
 			(subs2subst (assoc_thy "Isac.thy") subs)) ^
 indt j ^"</SUBSTITUTION>\n"):xml;
 (* val subs = [(str2term "bdv", str2term "x")];
 val subs = ["(bdv, x)"];
-tracing(subs2xml 0 subs);
+writeln(subs2xml 0 subs);
 *)
 fun subst2xml j (subst:subst) =
 (indt j ^"<SUBSTITUTION>\n"^
 foldl op^ ("", map (sub2xml (j+i)) subst) ^
 indt j ^"</SUBSTITUTION>\n"):xml;
 (* val subst = [(str2term "bdv", str2term "x")];
-tracing(subst2xml 0 subst);
+writeln(subst2xml 0 subst);
 *)
 (* val (j, str) = ((j+i), form);
 *)
 fun thmstr2xml j str = ((((term2xml j) o str2term) str)^"\n"):xml;
 *)
 | tac2xml j (Rewrite thm') =
 (indt j ^"<REWRITETACTIC name=\"Rewrite\">\n"^
 thm'2xml (j+i) thm'^
 indt j ^"</REWRITETACTIC>\n"):xml
-(* tracing (tac2xml 2 (Rewrite ("all_left",
+(* writeln (tac2xml 2 (Rewrite ("all_left",
 				"~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)")));
 val (j, (Rewrite_Inst (subs, thm'))) = (i, tac);
 *)
 | tac2xml j (Rewrite_Inst (subs, thm')) =
 (indt j ^"<REWRITEINSTTACTIC name=\"Rewrite_Inst\">\n"^
 subs2xml (j+i) subs^
 thm'2xml (j+i) thm'^
 indt j ^"</REWRITEINSTTACTIC>\n"):xml
-(* tracing (tac2xml 2 (Rewrite_Inst
+(* writeln (tac2xml 2 (Rewrite_Inst
 			   (["(bdv,x)"],
 			    ("all_left",
 			     "~ ?b =!= 0 ==> (?a = ?b) = (?a - ?b = 0)"))));
 *)
 | tac2xml j (Rewrite_Set rls') =
 | tac2xml j (Check_Postcond pI) =
 (indt j ^"<STRINGLISTTACTIC name=\"Check_Postcond\">\n"^
 id2xml (j+i) pI^
 indt j ^"</STRINGLISTTACTIC>\n"):xml
-| tac2xml j tac = raise error ("tac2xml: not impl. for "^tac2str tac);
+| tac2xml j tac = error ("tac2xml: not impl. for "^tac2str tac);
 fun tacs2xml j [] = "":xml
 | tacs2xml j (t::ts) = tac2xml j t ^ tacs2xml j ts;
 indt j ^ "</EXTREF>\n" : xml;
 (* val (ContThmInst{thyID, thm, bdvs, thminst, applto, applat, reword,
 		    asms, lhs, rhs, result, resasms, asmrls}) =
 (context_thy (pt,pos) tac);
-tracing (contthy2xml 2 (context_thy (pt,pos) tac));
+writeln (contthy2xml 2 (context_thy (pt,pos) tac));
 *)
 fun contthy2xml j EContThy =
-raise error "contthy2xml called with EContThy"
+error "contthy2xml called with EContThy"
 | contthy2xml j (ContThm {thyID, thm, applto, applat, reword,
 				 asms,lhs, rhs, result, resasms, asmrls}) =
 indt j ^ "<GUH> " ^ thm ^ " </GUH>\n" ^
 indt j ^ "<APPLTO>\n" ^

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38015	67ba02dffacc
child 38050	4c52ad406c20