Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/xmlsrc/datatypes.sml
changeset 59250 727dff4f6b2c
parent 59249 12dffe6c0a8b
child 59252 7d3dbc1171ff
equal deleted inserted replaced
59249:12dffe6c0a8b 59250:727dff4f6b2c 
     1 (* convert sml-datatypes to xml
 
     1 (* convert sml-datatypes to xml for libisabelle and for kbase.
 
     2    authors: Walther Neuper 2003
 
     2    authors: Walther Neuper 2003, 2016
 
     3    (c) due to copyright terms
 
     3    (c) due to copyright terms
 
     4 
       
     5 use"xmlsrc/datatypes.sml";
 
       
     6 use"datatypes.sml";
 
       
     7 *)
 
     4 *)
 
     8 
       
     9 
     5 
    10 signature DATATYPES = (*TODO: redo with xml_of/to *)
 
     6 signature DATATYPES = (*TODO: redo with xml_of/to *)
 
    11   sig
 
     7   sig
 
    12     val authors2xml : int -> string -> string list -> xml
 
     8     val authors2xml : int -> string -> string list -> xml
 
    13     val calc2xml : int -> thyID * calc -> xml
 
     9     val calc2xml : int -> thyID * calc -> xml
 
    57     val thm'2xml : int -> thm' -> xml
 
    53     val thm'2xml : int -> thm' -> xml
 
    58     val thm''2xml : int -> thm -> xml
 
    54     val thm''2xml : int -> thm -> xml
 
    59     val thmstr2xml : int -> string -> xml
 
    55     val thmstr2xml : int -> string -> xml
 
    60   end
 
    56   end
 
    61 
    57 
    62 
       
    63 
       
    64 (*------------------------------------------------------------------
 
    58 (*------------------------------------------------------------------
 
    65 structure datatypes:DATATYPES =
 
    59 structure datatypes:DATATYPES =
 
    66 (*structure datatypes =*)
 
    60 (*structure datatypes =*)
 
    67 struct
 
    61 struct
 
    68 ------------------------------------------------------------------*)
 
    62 ------------------------------------------------------------------*)
 
    69 
    63 
       
    64 (*** convert sml-datatypes to xml for kbase ***)
 
       
    65 (* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)
 
       
    66 
       
    67 val i = indentation;
 
       
    68 
       
    69 fun id2xml j ids =
 
       
    70     let fun id2x _ [] = ""
 
       
    71 	  | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ 
       
    72 			     (id2x j ss)
 
       
    73     in (indt j) ^ "<STRINGLIST>\n" ^ 
       
    74        (id2x (j + indentation) ids) ^ 
       
    75        (indt j) ^ "</STRINGLIST>\n" end;
 
       
    76 (* writeln(id2xml 8 ["linear","univariate","equation"]);
 
       
    77         <STRINGLIST>
 
       
    78           <STRING>linear</STRING>
 
       
    79           <STRING>univariate</STRING>
 
       
    80           <STRING>equation</STRING>
 
       
    81         </STRINGLIST>*)
 
       
    82 fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
 
       
    83     indt j ^ "<CALC>\n" ^
 
       
    84     indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
 
       
    85     indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge", 
       
    86 				      thyID) scrop  ^ "</GUH>\n" ^
 
       
    87     indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
 
       
    88     indt j ^ "</CALC>\n" : xml;
 
       
    89 (*replace by 'fun calc2xml' as developed for thy in 0607*)
 
       
    90 fun calc2xmlOLD _ ((scr_op, (isa_op, _)):calc) =
 
       
    91     indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
 
       
    92 fun calcs2xmlOLD _ [] = ("":xml) (*TODO replace with 'strs2xml'*)
 
       
    93   | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
 
       
    94 
       
    95 (*.for creating a href for a rule within an rls's rule list;
 
       
    96    the guh points to the thy of definition of the rule, NOT of use in rls.*)
 
       
    97 fun rule2xml _ (_ : thyID) Erule =
 
       
    98       error "rule2xml called with 'Erule'"
 
       
    99   | rule2xml j _ (Thm (thmDeriv, _)) =
 
       
   100       indt j ^ "<RULE>\n" ^
 
       
   101       indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
 
       
   102       indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
 
       
   103       indt (j+i) ^ "<GUH> " ^ 
       
   104         thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
 
       
   105         indt j ^ "</RULE>\n" : xml
 
       
   106   | rule2xml _ _ (Calc (_(*termop*), _)) = ""
 
       
   107 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
 
       
   108   see smltest/../datatypes.sml !
 
       
   109     indt j ^ "<RULE>\n" ^
 
       
   110     indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
 
       
   111     indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop) 
       
   112 				    termop ^ " </GUH>\n" ^
 
       
   113     indt j ^ "</RULE>\n"
 
       
   114 *)
 
       
   115   | rule2xml _ _ (Cal1 (_(*termop*), _)) = ""
 
       
   116   | rule2xml j thyID (Rls_ rls) =
 
       
   117       let val rls' = (#id o rep_rls) rls
 
       
   118       in
 
       
   119         indt j ^ "<RULE>\n" ^
 
       
   120         indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
 
       
   121         indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
 
       
   122         indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
 
       
   123         indt j ^ "</RULE>\n"
 
       
   124       end;
 
       
   125 fun rules2xml _ _ [] = ("":xml)                    
       
   126   | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
 
       
   127 
       
   128 fun filterpbl str =
 
       
   129   let fun filt [] = []
 
       
   130         | filt ((s, (t1, t2)) :: ps) = 
       
   131 	  if str = s then (t1 $ t2) :: filt ps else filt ps
 
       
   132   in filt end;
 
       
   133 fun pattern2xml j p where_ =
 
       
   134     (case filterpbl "#Given" p of
 
       
   135 	[] =>  (indt j) ^ "<GIVEN>  </GIVEN>\n"
 
       
   136 (* val gis = filterpbl "#Given" p;
 
       
   137    *)
 
       
   138       | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
 
       
   139 	       (indt j) ^ "</GIVEN>\n")
 
       
   140     ^ 
       
   141     (case where_ of
 
       
   142 	 [] =>  (indt j) ^ "<WHERE>  </WHERE>\n"
 
       
   143        | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
 
       
   144 		(indt j) ^ "</WHERE>\n")
 
       
   145     ^ 
       
   146     (case filterpbl "#Find" p of
 
       
   147 	 [] =>  (indt j) ^ "<FIND>  </FIND>\n"
 
       
   148        | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
 
       
   149 		(indt j) ^ "</FIND>\n")
 
       
   150     ^ 
       
   151     (case filterpbl "#Relate" p of
 
       
   152 	 [] =>  (indt j) ^ "<RELATE>  </RELATE>\n"
 
       
   153        | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
 
       
   154 		(indt j) ^ "</RELATE>\n");
 
       
   155 (*
 
       
   156 writeln(pattern2xml 3 ((#ppc o get_pbt)
 
       
   157 			 ["squareroot","univariate","equation","test"]) []);
 
       
   158   *)
 
       
   159 
       
   160 (*url to a source external to isac*)
 
       
   161 fun extref2xml j linktext url =
 
       
   162     indt j ^ "<EXTREF>\n" ^
 
       
   163     indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
 
       
   164     indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
 
       
   165     indt j ^ "</EXTREF>\n" : xml;
 
       
   166 fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
 
       
   167     let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
 
       
   168 	val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
 
       
   169     in indt j ^ "<KESTOREREF>\n" ^
 
       
   170        indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
 
       
   171        indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
 
       
   172        indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
 
       
   173        indt j ^ "</KESTOREREF>\n" : xml
 
       
   174     end;
 
       
   175 fun keref2xml j typ (kestoreID:kestoreID) =
 
       
   176     let val id = strs2str' kestoreID
 
       
   177 	val guh = kestoreID2guh typ kestoreID
 
       
   178     in indt j ^ "<KESTOREREF>\n" ^
 
       
   179        indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
 
       
   180        indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
 
       
   181        indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
 
       
   182        indt j ^ "</KESTOREREF>\n" : xml
 
       
   183     end;
 
       
   184 fun authors2xml j str auts = 
       
   185     let fun autx _ [] = ""
 
       
   186 	  | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^ 
       
   187 			     (autx j ss)
 
       
   188     in indt j ^ "<"^str^">\n" ^
 
       
   189        autx (j + i) auts ^ 
       
   190        indt j ^ "</"^str^">\n" : xml
 
       
   191     end;
 
       
   192 (* writeln(authors2xml 2 "MATHAUTHORS" []);
 
       
   193    writeln(authors2xml 2 "MATHAUTHORS" 
       
   194 		       ["isac-team 2001", "Richard Lang 2003"]);
 
       
   195    *)
 
       
   196 fun scr2xml j EmptyScr =
 
       
   197     indt j ^"<SCRIPT>  </SCRIPT>\n" : xml
 
       
   198   | scr2xml j (Prog term) =
 
       
   199     if term = e_term 
       
   200     then indt j ^"<SCRIPT>  </SCRIPT>\n"
 
       
   201     else indt j ^"<SCRIPT>\n"^ 
       
   202 	 term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
 
       
   203 	 indt j ^"</SCRIPT>\n"
 
       
   204   | scr2xml j (Rfuns _) =
 
       
   205     indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
 
       
   206 
       
   207 fun calcref2xml j (thyID:thyID, (scrop, (_(*rewop*), _)):calc) =
 
       
   208     indt j ^ "<CALCREF>\n" ^
 
       
   209     indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
 
       
   210     indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge", 
       
   211 				      thyID) scrop  ^ " </GUH>\n" ^
 
       
   212     indt j ^ "</CALCREF>\n" : xml;
 
       
   213 fun calcrefs2xml _ (_,[]) = "":xml
 
       
   214   | calcrefs2xml j (thyID, cal::cs) = 
       
   215     calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
 
       
   216 
       
   217 fun prepa12xml j (terms, term) =
 
       
   218     indt j ^"<PREPAT>\n"^
 
       
   219     indt (j+i) ^"<PRECONDS>\n"^
 
       
   220     terms2xml (j+2*i) terms ^
 
       
   221     indt (j+i) ^"</PRECONDS>\n"^
 
       
   222     indt (j+i) ^"<PATTERN>\n"^
 
       
   223     term2xml (j+2*i) term ^
 
       
   224     indt (j+i) ^"</PATTERN>\n"^
 
       
   225     indt j ^"</PREPAT>\n" : xml;
 
       
   226 fun prepat2xml _ [] = ""
 
       
   227   | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
 
       
   228 
       
   229 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
 
       
   230 		      srls, calc, rules, errpatts, scr}) =
 
       
   231     indt j ^"<RULESET>\n"^
 
       
   232     indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
 
       
   233     indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
 
       
   234     indt (j+i) ^"<RULES>\n" ^
 
       
   235     rules2xml (j+2*i) thyID rules ^
 
       
   236     indt (j+i) ^"</RULES>\n" ^
 
       
   237     indt (j+i) ^"<PRECONDS> " ^
 
       
   238     terms2xml' (j+2*i) preconds ^
 
       
   239     indt (j+i) ^"</PRECONDS>\n" ^
 
       
   240     indt (j+i) ^"<ORDER>\n" ^
 
       
   241     indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
 
       
   242 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
 
       
   243     indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", 
       
   244 				      thyID) ord ^ " </GUH>\n" ^
 
       
   245 ..................................................................*)
 
       
   246     indt (j+i) ^"</ORDER>\n" ^
 
       
   247     indt (j+i) ^"<ERLS>\n" ^
 
       
   248     indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
 
       
   249     indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
 
       
   250     indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) 
       
   251 				     (id_rls erls) ^ " </GUH>\n" ^
 
       
   252     indt (j+i) ^"</ERLS>\n" ^
 
       
   253     indt (j+i) ^"<SRLS>\n" ^
 
       
   254     indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
 
       
   255     indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
 
       
   256     indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) 
       
   257 				     (id_rls srls) ^ " </GUH>\n" ^
 
       
   258     indt (j+i) ^"</SRLS>\n" ^
 
       
   259     calcrefs2xml (j+i) (thyID, calc) ^
 
       
   260     scr2xml (j+i) scr ^
 
       
   261     indt j ^"</RULESET>\n" : xml;
 
       
   262 fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
 
       
   263   | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
 
       
   264   | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
 
       
   265   | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) = 
       
   266     indt j ^"<RULESET>\n"^
 
       
   267     indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
 
       
   268     indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
 
       
   269     prepat2xml (j+i) prepat ^
 
       
   270     indt (j+i) ^"<ORDER> " ^
 
       
   271     indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
 
       
   272     indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
 
       
   273 (*WN060714 thy_isac_*-ord-*.xml not yet generated ................
 
       
   274     indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge", 
       
   275 				      thyID) ord ^ " </GUH>\n" ^
 
       
   276 .................................................................*)
 
       
   277     indt (j+i) ^"</ORDER>\n" ^
 
       
   278     indt (j+i) ^"<ERLS> " ^
 
       
   279     indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
 
       
   280     indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
 
       
   281     indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
 
       
   282     indt (j+i) ^"</ERLS>\n" ^
 
       
   283     calcrefs2xml (j+i) (thyID, calc) ^
 
       
   284     indt (j+i) ^"<SCRIPT>\n"^ 
       
   285     scr2xml (j+2*i) scr ^
 
       
   286     indt (j+i) ^" </SCRIPT>\n"^
 
       
   287     indt j ^"</RULESET>\n" : xml;
 
       
   288 
       
   289 (*** convert sml-datatypes to xml for libisabelle ***)
 
       
   290 
    70 (** general types: lists,  **)
 
   291 (** general types: lists,  **)
 
    71 
   292 
    72 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
 
   293 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
 
    73 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
 
   294 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
 
    74   | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
 
   295   | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
 
    83   | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
 
   304   | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
 
    84 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
 
   305 fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
 
    85   | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
 
   306   | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
 
    86 
   307 
    87 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
 
   308 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
 
    88 fun xml_of_ints is = (*xml/datatypes.sml: fun ints2xml*)
 
   309 fun xml_of_ints is =
 
    89   XML.Elem (("INTLIST", []), map xml_of_int is)
 
   310   XML.Elem (("INTLIST", []), map xml_of_int is)
 
    90 
   311 
    91 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) = 
   312 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) = 
    92       (case int_of_str i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
 
   313       (case int_of_str i of SOME i => i | _ => error "xml_to_int: int_of_str \<Rightarrow> NONE")
 
    93   | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
 
   314   | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
 
    94 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
 
   315 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
 
    95   | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
 
   316   | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
 
    96 
       
    97 
   317 
    98 (** isac datatypes **)
 
   318 (** isac datatypes **)
 
    99 fun xml_of_pos tag (is, pp) =
 
   319 fun xml_of_pos tag (is, pp) =
 
   100   XML.Elem ((tag, []), [
 
   320   XML.Elem ((tag, []), [
 
   101     xml_of_ints is,
 
   321     xml_of_ints is,
 
   138     XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (comp_dts' dts)])
 
   358     XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (comp_dts' dts)])
 
   139   | xml_of_itm_ (Sup dts) = 
   359   | xml_of_itm_ (Sup dts) = 
   140     XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
 
   360     XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
 
   141   | xml_of_itm_ (Mis (d, pid)) = 
   361   | xml_of_itm_ (Mis (d, pid)) = 
   142     XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
 
   362     XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
 
   143 
   363   | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
 
   144 fun xml_of_itms itms =
 
   364 fun xml_of_itms itms =
 
   145   let 
   365   let 
   146     fun extract (_, _, _, _, itm_) = itm_
 
   366     fun extract (_, _, _, _, itm_) = itm_
 
   147       | extract _ = error "xml_of_itms.extract: wrong argument" 
   367       | extract _ = error "xml_of_itms.extract: wrong argument" 
   148   in map (xml_of_itm_ o extract) itms end
 
   368   in map (xml_of_itm_ o extract) itms end
 
   245 fun xml_to_sube
 
   465 fun xml_to_sube
 
   246     (XML.Elem (("SUBSTITUTION", []), 
   466     (XML.Elem (("SUBSTITUTION", []), 
   247       xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
 
   467       xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
 
   248   | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
 
   468   | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
 
   249 
   469 
       
   470 fun thm''2xml j (thm : thm) =
 
       
   471     indt j ^ "<THEOREM>\n" ^
 
       
   472     indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
 
       
   473     term2xml j (Thm.prop_of thm) ^ "\n" ^
 
       
   474     indt j ^ "</THEOREM>\n" : xml;
 
   250 fun xml_of_thm' ((ID, form) : thm') =
 
   475 fun xml_of_thm' ((ID, form) : thm') =
 
   251   XML.Elem (("THEOREM", []), [
 
   476   XML.Elem (("THEOREM", []), [
 
   252     XML.Elem (("ID", []), [XML.Text ID]),
 
   477     XML.Elem (("ID", []), [XML.Text ID]),
 
   253     XML.Elem (("FORMULA", []), [
 
   478     XML.Elem (("FORMULA", []), [
 
   254       XML.Text form])])           (* repair for MathML: use term instead String *)
 
   479       XML.Text form])])           (* repair for MathML: use term instead String *)
 
       
   480 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
 
       
   481 fun xml_of_thm'' ((ID, term) : thm'') =
 
       
   482   XML.Elem (("THEOREM", []), [
 
       
   483     XML.Elem (("ID", []), [XML.Text ID]),
 
       
   484     xml_of_term_NEW term])
 
   255 fun xml_to_thm'
 
   485 fun xml_to_thm'
 
   256     (XML.Elem (("THEOREM", []), [
 
   486     (XML.Elem (("THEOREM", []), [
 
   257       XML.Elem (("ID", []), [XML.Text ID]),
 
   487       XML.Elem (("ID", []), [XML.Text ID]),
 
   258       XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
 
   488       XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
 
   259         XML.Text form])])) = ((ID, form) : thm')
 
   489         XML.Text form])])) = ((ID, form) : thm')
 
   260   | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
 
   490   | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
 
   261 
   491 (* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
 
   262 fun xml_of_thm (thm : thm) =
 
   492 fun xml_to_thm''
 
   263   XML.Elem (("THEOREM", []), [
 
   493     (XML.Elem (("THEOREM", []), [
 
   264     XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
 
   494       XML.Elem (("ID", []), [XML.Text ID])])) =
 
   265     xml_of_term (Thm.prop_of thm)])
 
   495     (ID, Thm.prop_of (Global_Theory.get_thm (Isac ()) ID)) : thm''
 
       
   496   | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:" ^ xmlstr 0 x)
 
   266 
   497 
   267 fun xml_of_src EmptyScr =
 
   498 fun xml_of_src EmptyScr =
 
   268     XML.Elem (("NOCODE", []), [XML.Text "empty"])
 
   499     XML.Elem (("NOCODE", []), [XML.Text "empty"])
 
   269   | xml_of_src (Prog term) =
 
   500   | xml_of_src (Prog term) =
 
   270     XML.Elem (("CODE", []), [
 
   501     XML.Elem (("CODE", []), [
 
   280       XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
 
   511       XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
 
   281   | xml_of_tac (Substitute cterms) =
 
   512   | xml_of_tac (Substitute cterms) =
 
   282     (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
 
   513     (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
 
   283     XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
 
   514     XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
 
   284     (*----- Rewrite* -----------------------------------------------------*)
 
   515     (*----- Rewrite* -----------------------------------------------------*)
 
   285   | xml_of_tac (Rewrite thm') =
 
   516   | xml_of_tac (Rewrite thm'') =
 
   286     XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
 
   517     XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
 
   287   | xml_of_tac (Rewrite_Inst (subs, thm')) =
 
   518   | xml_of_tac (Rewrite_Inst (subs, thm'')) =
 
   288     XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
 
   519     XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
 
   289       xml_of_subs subs ::
 
   520       xml_of_subs subs ::
 
   290       xml_of_thm' thm' :: []))
 
   521       xml_of_thm'' thm'' :: []))
 
   291   | xml_of_tac (Rewrite_Set rls') =
 
   522   | xml_of_tac (Rewrite_Set rls') =
 
   292     XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
 
   523     XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
 
   293   | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
 
   524   | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
 
   294     XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
 
   525     XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
 
   295       xml_of_subs subs,
 
   526       xml_of_subs subs,
 
   336     (XML.Elem (("STRINGLISTTACTIC", [
 
   567     (XML.Elem (("STRINGLISTTACTIC", [
 
   337       ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
 
   568       ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
 
   338     (*----- Rewrite* -----------------------------------------------------*)
 
   569     (*----- Rewrite* -----------------------------------------------------*)
 
   339   | xml_to_tac
 
   570   | xml_to_tac
 
   340     (XML.Elem (("REWRITETACTIC", [
 
   571     (XML.Elem (("REWRITETACTIC", [
 
   341       ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
 
   572       ("name", "Rewrite")]), [thm])) = Rewrite (xml_to_thm'' thm)
 
   342   | xml_to_tac
 
   573   | xml_to_tac
 
   343     (XML.Elem (("REWRITEINSTTACTIC", [
 
   574     (XML.Elem (("REWRITEINSTTACTIC", [
 
   344       ("name", "Rewrite_Inst")]), [
 
   575       ("name", "Rewrite_Inst")]), [
 
   345         subs, thm'])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm' thm')
 
   576         subs, thm])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
 
   346   | xml_to_tac
 
   577   | xml_to_tac
 
   347     (XML.Elem (("REWRITESETTACTIC", [
 
   578     (XML.Elem (("REWRITESETTACTIC", [
 
   348       ("name", "Rewrite_Set")]), [XML.Text rls'])) = Rewrite_Set (rls')
 
   579       ("name", "Rewrite_Set")]), [XML.Text rls'])) = Rewrite_Set (rls')
 
   349   | xml_to_tac
 
   580   | xml_to_tac
 
   350     (XML.Elem (("REWRITESETINSTTACTIC", [
 
   581     (XML.Elem (("REWRITESETINSTTACTIC", [
wneuper/isa