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

equal deleted inserted replaced

-:6a2753b8d70c
+:49d7d410b83c
 (c) due to copyright terms
 *)
 signature DATATYPES = (*TODO: redo with xml_of/to *)
 sig
-val authors2xml : int -> string -> string list -> xml
+val authors2xml : int -> string -> string list -> Celem.xml
-val calc2xml : int -> thyID * calc -> xml
+val calc2xml : int -> Celem.thyID * Celem.calc -> Celem.xml
-val calcrefs2xml : int -> thyID * calc list -> xml
+val calcrefs2xml : int -> Celem.thyID * Celem.calc list -> Celem.xml
-val contthy2xml : int -> Rtools.contthy -> xml
+val contthy2xml : int -> Rtools.contthy -> Celem.xml
-val extref2xml : int -> string -> string -> xml
+val extref2xml : int -> string -> string -> Celem.xml
 val filterpbl :
 ''a -> (''a * (Term.term * Term.term)) list -> Term.term list
-val formula2xml : int -> Term.term -> xml
+val formula2xml : int -> Term.term -> Celem.xml
-val formulae2xml : int -> Term.term list -> xml
+val formulae2xml : int -> Term.term list -> Celem.xml
 val i : int
 val id2xml : int -> string list -> string
 val ints2xml : int -> int list -> string
-val itm_2xml : int -> Model.itm_ -> xml
+val itm_2xml : int -> Model.itm_ -> Celem.xml
 val itms2xml : int -> (int * Model.vats * bool * string * Model.itm_) list ->
 string
-val keref2xml : int -> ketype -> kestoreID -> xml
+val keref2xml : int -> Celem.ketype -> Celem.kestoreID -> Celem.xml
 val model2xml :
-int -> Model.itm list -> (bool * Term.term) list -> xml
+int -> Model.itm list -> (bool * Term.term) list -> Celem.xml
-val modspec2xml : int -> Ctree.ocalhd -> xml
+val modspec2xml : int -> Ctree.ocalhd -> Celem.xml
 val pattern2xml :
 int ->
 (string * (Term.term * Term.term)) list -> Term.term list -> string
 val pos'2xml : int -> string * (int list * Ctree.pos_) -> string
-val pos'calchead2xml : int -> Ctree.pos' * Ctree.ocalhd -> xml
+val pos'calchead2xml : int -> Ctree.pos' * Ctree.ocalhd -> Celem.xml
 val pos_2xml : int -> Ctree.pos_ -> string
-val posform2xml : int -> Ctree.pos' * Term.term -> xml
+val posform2xml : int -> Ctree.pos' * Term.term -> Celem.xml
 val posformhead2xml : int -> Ctree.pos' * Ctree.ptform -> string
-val posformheads2xml : int -> (Ctree.pos' * Ctree.ptform) list -> xml
+val posformheads2xml : int -> (Ctree.pos' * Ctree.ptform) list -> Celem.xml
-val posforms2xml : int -> (Ctree.pos' * Term.term) list -> xml
+val posforms2xml : int -> (Ctree.pos' * Term.term) list -> Celem.xml
-val posterms2xml : int -> (Ctree.pos' * term) list -> xml
+val posterms2xml : int -> (Ctree.pos' * term) list -> Celem.xml
-val precond2xml : int -> bool * Term.term -> xml
+val precond2xml : int -> bool * Term.term -> Celem.xml
-val preconds2xml : int -> (bool * Term.term) list -> xml
+val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
-val rls2xml : int -> thyID * rls -> xml
+val rls2xml : int -> Celem.thyID * rls -> Celem.xml
-val rule2xml : int -> guh -> rule -> xml
+val rule2xml : int -> Celem.guh -> rule -> Celem.xml
-val rules2xml : int -> guh -> rule list -> xml
+val rules2xml : int -> Celem.guh -> rule list -> Celem.xml
-val scr2xml : int -> scr -> xml
+val scr2xml : int -> Celem.scr -> Celem.xml
-val spec2xml : int -> spec -> xml
+val spec2xml : int -> Celem.spec -> Celem.xml
-val sub2xml : int -> Term.term * Term.term -> xml
+val sub2xml : int -> Term.term * Term.term -> Celem.xml
-val subs2xml : int -> Selem.subs -> xml
+val subs2xml : int -> Selem.subs -> Celem.xml
-val subst2xml : int -> subst -> xml
+val subst2xml : int -> Celem.subst -> Celem.xml
-val tac2xml : int -> Tac.tac -> xml
+val tac2xml : int -> Tac.tac -> Celem.xml
-val tacs2xml : int -> Tac.tac list -> xml
+val tacs2xml : int -> Tac.tac list -> Celem.xml
-val theref2xml : int -> thyID -> string -> xstring -> string
+val theref2xml : int -> Celem.thyID -> string -> xstring -> string
-val thm'2xml : int -> thm' -> xml
+val thm'2xml : int -> Celem.thm' -> Celem.xml
-val thm''2xml : int -> thm -> xml
+val thm''2xml : int -> thm -> Celem.xml
-val thmstr2xml : int -> string -> xml
+val thmstr2xml : int -> string -> Celem.xml
 end
 (*------------------------------------------------------------------
 structure datatypes:DATATYPES =
 (*structure datatypes =*)
 <STRINGLIST>
 <STRING>linear</STRING>
 <STRING>univariate</STRING>
 <STRING>equation</STRING>
 </STRINGLIST>*)
-fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
+fun calc2xml j (thyID, (scrop, (rewop, _))) =
 indt j ^ "<CALC>\n" ^
 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
-indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
+indt (j+i) ^ "<GUH>\n" ^ Celem.cal2guh ("IsacKnowledge",
 				      thyID) scrop  ^ "</GUH>\n" ^
 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
-indt j ^ "</CALC>\n" : xml;
+indt j ^ "</CALC>\n";
 (*replace by 'fun calc2xml' as developed for thy in 0607*)
-fun calc2xmlOLD _ ((scr_op, (isa_op, _)):calc) =
+fun calc2xmlOLD _ (scr_op, (isa_op, _)) =
 indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
-fun calcs2xmlOLD _ [] = ("":xml) (*TODO replace with 'strs2xml'*)
+fun calcs2xmlOLD _ [] = "" (*TODO replace with 'strs2xml'*)
 | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
 (*.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 _ (_ : thyID) Erule =
+fun rule2xml _ _  Celem.Erule =
 error "rule2xml called with 'Erule'"
-| rule2xml j _ (Thm (thmDeriv, _)) =
+| rule2xml j _ (Celem.Thm (thmDeriv, _)) =
 indt j ^ "<RULE>\n" ^
 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
-indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
+indt (j+i) ^ "<STRING> " ^ Celem.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
 indt (j+i) ^ "<GUH> " ^
-thm2guh (Rtools.thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
+Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (Celem.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
-indt j ^ "</RULE>\n" : xml
+indt j ^ "</RULE>\n"
-| rule2xml _ _ (Calc (_(*termop*), _)) = ""
+| rule2xml _ _ (Celem.Calc (_(*termop*), _)) = ""
 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
 see smltest/../datatypes.sml !
 indt j ^ "<RULE>\n" ^
 indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
 indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
 				    termop ^ " </GUH>\n" ^
 indt j ^ "</RULE>\n"
 *)
-| rule2xml _ _ (Cal1 (_(*termop*), _)) = ""
+| rule2xml _ _ (Celem.Cal1 (_(*termop*), _)) = ""
-| rule2xml j thyID (Rls_ rls) =
+| rule2xml j thyID (Celem.Rls_ rls) =
-let val rls' = (#id o rep_rls) rls
+let val rls' = (#id o Celem.rep_rls) rls
 in
 indt j ^ "<RULE>\n" ^
 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
-indt (j+i) ^ "<GUH> " ^ rls2guh (Rtools.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
+indt (j+i) ^ "<GUH> " ^ Celem.rls2guh (Rtools.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
 indt j ^ "</RULE>\n"
 end;
-fun rules2xml _ _ [] = ("":xml)
+fun rules2xml _ _ [] = ""
 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
 fun filterpbl str =
 let fun filt [] = []
 | filt ((s, (t1, t2)) :: ps) =
 (*url to a source external to isac*)
 fun extref2xml j linktext url =
 indt j ^ "<EXTREF>\n" ^
 indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
-indt j ^ "</EXTREF>\n" : xml;
+indt j ^ "</EXTREF>\n";
-fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
+fun theref2xml j thyID typ xstring =
-let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
+let val guh = Celem.theID2guh ["IsacKnowledge", thyID, typ, xstring]
 	val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
 in indt j ^ "<KESTOREREF>\n" ^
 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
-indt j ^ "</KESTOREREF>\n" : xml
+indt j ^ "</KESTOREREF>\n"
 end;
-fun keref2xml j typ (kestoreID:kestoreID) =
+fun keref2xml j typ kestoreID =
 let val id = strs2str' kestoreID
 	val guh = Specify.kestoreID2guh typ kestoreID
 in indt j ^ "<KESTOREREF>\n" ^
-indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
+indt (j+i) ^ "<TAG> " ^ Celem.ketype2str' typ ^ "</TAG>\n" ^
 indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
-indt j ^ "</KESTOREREF>\n" : xml
+indt j ^ "</KESTOREREF>\n"
 end;
 fun authors2xml j str auts =
 let fun autx _ [] = ""
 	  | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
 			     (autx j ss)
 in indt j ^ "<"^str^">\n" ^
 autx (j + i) auts ^
-indt j ^ "</"^str^">\n" : xml
+indt j ^ "</"^str^">\n"
 end;
 (* writeln(authors2xml 2 "MATHAUTHORS" []);
 writeln(authors2xml 2 "MATHAUTHORS"
 		       ["isac-team 2001", "Richard Lang 2003"]);
 *)
 fun scr2xml j EmptyScr =
-indt j ^"<SCRIPT>  </SCRIPT>\n" : xml
+indt j ^"<SCRIPT>  </SCRIPT>\n"
-| scr2xml j (Prog term) =
+| scr2xml j (Celem.Prog term) =
-if term = e_term
+if term = Celem.e_term
 then indt j ^"<SCRIPT>  </SCRIPT>\n"
 else indt j ^"<SCRIPT>\n"^
 	 term2xml j (TermC.inst_abs term) ^ "\n" ^
 	 indt j ^"</SCRIPT>\n"
-| scr2xml j (Rfuns _) =
+| scr2xml j (Celem.Rfuns _) =
 indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
-fun calcref2xml j (thyID:thyID, (scrop, (_(*rewop*), _)):calc) =
+fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
 indt j ^ "<CALCREF>\n" ^
 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
-indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
+indt (j+i) ^ "<GUH> " ^ Celem.cal2guh ("IsacKnowledge",
 				      thyID) scrop  ^ " </GUH>\n" ^
-indt j ^ "</CALCREF>\n" : xml;
+indt j ^ "</CALCREF>\n";
-fun calcrefs2xml _ (_,[]) = "":xml
+fun calcrefs2xml _ (_,[]) = ""
 | calcrefs2xml j (thyID, cal::cs) =
 calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
 fun prepa12xml j (terms, term) =
 indt j ^"<PREPAT>\n"^
 terms2xml (j+2*i) terms ^
 indt (j+i) ^"</PRECONDS>\n"^
 indt (j+i) ^"<PATTERN>\n"^
 term2xml (j+2*i) term ^
 indt (j+i) ^"</PATTERN>\n"^
-indt j ^"</PREPAT>\n" : xml;
+indt j ^"</PREPAT>\n";
 fun prepat2xml _ [] = ""
-| prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
+| prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;
 fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
 		      srls, calc, rules, errpatts, scr}) =
 indt j ^"<RULESET>\n"^
 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
 				      thyID) ord ^ " </GUH>\n" ^
 ..................................................................*)
 indt (j+i) ^"</ORDER>\n" ^
 indt (j+i) ^"<ERLS>\n" ^
 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
-indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
+indt (j+2*i) ^ "<STRING> " ^ Celem.id_rls erls ^ " </STRING>\n" ^
-indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
+indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
-				     (id_rls erls) ^ " </GUH>\n" ^
+				     (Celem.id_rls erls) ^ " </GUH>\n" ^
 indt (j+i) ^"</ERLS>\n" ^
 indt (j+i) ^"<SRLS>\n" ^
 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
-indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
+indt (j+2*i) ^ "<STRING> " ^ Celem.id_rls erls ^ " </STRING>\n" ^
-indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
+indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID)
-				     (id_rls srls) ^ " </GUH>\n" ^
+				     (Celem.id_rls srls) ^ " </GUH>\n" ^
 indt (j+i) ^"</SRLS>\n" ^
 calcrefs2xml (j+i) (thyID, calc) ^
 scr2xml (j+i) scr ^
-indt j ^"</RULESET>\n" : xml;
+indt j ^"</RULESET>\n";
-fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
+fun rls2xml j (thyID, Celem.Erls) = rls2xml j (thyID, Celem.e_rls)
-| rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
+| rls2xml j (thyID, Celem.Rls data) = rls2xm j (thyID, "Rls", data)
-| rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
+| rls2xml j (thyID, Celem.Seq data) = rls2xm j (thyID, "Seq", data)
-| rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
+| rls2xml j (thyID, Celem.Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
 indt j ^"<RULESET>\n"^
 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
 indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
 prepat2xml (j+i) prepat ^
 indt (j+i) ^"<ORDER> " ^
 				      thyID) ord ^ " </GUH>\n" ^
 .................................................................*)
 indt (j+i) ^"</ORDER>\n" ^
 indt (j+i) ^"<ERLS> " ^
 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
-indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
+indt (j+2*i) ^ "<STRING> " ^ Celem.id_rls erls ^ " </STRING>\n" ^
-indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
+indt (j+2*i) ^ "<GUH> " ^ Celem.rls2guh ("IsacKnowledge", thyID) (Celem.id_rls erls) ^ " </GUH>\n" ^
 indt (j+i) ^"</ERLS>\n" ^
 calcrefs2xml (j+i) (thyID, calc) ^
 indt (j+i) ^"<SCRIPT>\n"^
 scr2xml (j+2*i) scr ^
 indt (j+i) ^" </SCRIPT>\n"^
-indt j ^"</RULESET>\n" : xml;
+indt j ^"</RULESET>\n";
 (*** convert sml-datatypes to xml for libisabelle ***)
 (** general types: lists,  **)
 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
-fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = str2ketype' str
+fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = Celem.str2ketype' str
 | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
 pos as XML.Elem ((   "POSITION", []), _),
 XML.Elem ((          "HEAD", []), [form]),
 imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)
 XML.Elem ((          "POS", []), [XML.Text belongsto]),
 spec as XML.Elem ((  "SPECIFICATION", []), _)])) =
-(xml_to_pos pos, xml_to_term_NEW form |> term2str, xml_to_imodel imodel,
+(xml_to_pos pos, xml_to_term_NEW form |> Celem.term2str, xml_to_imodel imodel,
 Ctree.str2pos_ belongsto, xml_to_spec spec) : Inform.icalhd
 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
 fun xml_of_sub (id, value) =
 XML.Elem (("PAIR", []), [
 (XML.Elem (("PAIR", []), [
 XML.Elem (("VARIABLE", []), [id]),
 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
 fun xml_of_subs (subs : Selem.subs) =
-XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (assoc_thy "Isac") subs))
+XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (Celem.assoc_thy "Isac") subs))
 fun xml_to_subs
 (XML.Elem (("SUBSTITUTION", []),
 subs)) = Selem.subst2subs (map xml_to_sub subs)
 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
 fun xml_of_sube sube =
-XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (assoc_thy "Isac") sube))
+XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (Celem.assoc_thy "Isac") sube))
 fun xml_to_sube
 (XML.Elem (("SUBSTITUTION", []),
 xml_var_val_pairs)) = Selem.subst2sube (map xml_to_sub xml_var_val_pairs)
 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
 fun thm''2xml j (thm : thm) =
 indt j ^ "<THEOREM>\n" ^
-indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
+indt (j+i) ^ "<ID> " ^ Celem.thmID_of_derivation_name' thm ^ " </ID>\n"^
 term2xml j (Thm.prop_of thm) ^ "\n" ^
-indt j ^ "</THEOREM>\n" : xml;
+indt j ^ "</THEOREM>\n";
-fun xml_of_thm' ((ID, form) : thm') =
+fun xml_of_thm' (ID, form) =
 XML.Elem (("THEOREM", []), [
 XML.Elem (("ID", []), [XML.Text ID]),
 XML.Elem (("FORMULA", []), [
 XML.Text form])])           (* repair for MathML: use term instead String *)
 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
-fun xml_of_thm'' ((ID, thm) : thm'') =
+fun xml_of_thm'' (ID, thm) =
 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
 XML.Elem (("THEOREM", []), [
 XML.Elem (("ID", []), [XML.Text ID]),
 xml_of_term_NEW term])
 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
 XML.Elem (("THEOREM", []), [
 XML.Elem (("ID", []), [XML.Text ID]),
 XML.Elem (("FORMULA", []), [
-XML.Text ((term2str o Thm.prop_of) thm)])])           (* repair for MathML: use term instead String *)
+XML.Text ((Celem.term2str o Thm.prop_of) thm)])])           (* repair for MathML: use term instead String *)
 fun xml_to_thm'
 (XML.Elem (("THEOREM", []), [
 XML.Elem (("ID", []), [XML.Text ID]),
 XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) =
-((ID, "NO_ad_hoc_thm_FROM_GUI = True") : thm')
+(ID, "NO_ad_hoc_thm_FROM_GUI = True")
 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:\n" ^ xmlstr 0 x)
 (* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
 fun xml_to_thm''
 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
 (XML.Elem (("THEOREM", []), [
 | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x)
 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
 (XML.Elem (("THEOREM", []), [
 XML.Elem (("ID", []), [XML.Text ID]),
 XML.Elem (("FORMULA", []), [
-XML.Text term])])) = (ID, Rewrite.assoc_thm'' (Isac ()) ID) : thm''
+XML.Text term])])) = (ID, Rewrite.assoc_thm'' (Celem.Isac ()) ID)
 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
 fun xml_of_src EmptyScr =
 XML.Elem (("NOCODE", []), [XML.Text "empty"])
-| xml_of_src (Prog term) =
+| xml_of_src (Celem.Prog term) =
 XML.Elem (("CODE", []), [
-if term = e_term then xml_of_src EmptyScr
+if term = Celem.e_term then xml_of_src Celem.EmptyScr
 else xml_of_term (TermC.inst_abs term)])
-| xml_of_src (Rfuns _) =
+| xml_of_src (Celem.Rfuns _) =
 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
 (*.convert a tactic into xml-format .*)
 fun xml_of_tac (Tac.Subproblem (dI, pI)) =
 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
 (XML.Elem (("STRINGLISTTACTIC", [
 ("name", "Specify_Problem")]), [ct])) = Tac.Specify_Problem (xml_to_strs ct)
 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Script}))
-		    ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
+		    ("Problem (" ^ Celem.e_domID ^ "," ^ strs2str' Celem.e_pblID ^ ")");
 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
 fun xml_of_posterm (p, t) =
 let val input_request = Free ("________________________________________________", dummyT)
 in
 (*.a reference to an element in the theory hierarchy;
 compare 'fun keref2xml'.*)
 (* val (j, thyID, typ, xstring) =
 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
 *)
-fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
+fun theref2xml j thyID typ xstring =
-let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
+let val guh = Celem.theID2guh ["IsacKnowledge", thyID, typ, xstring]
 	val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
 in indt j ^ "<KESTOREREF>\n" ^
 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
 indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
-indt j ^ "</KESTOREREF>\n" : xml
+indt j ^ "</KESTOREREF>\n"
 end;
-fun xml_of_theref (thyid : thyID) typ (xstring : xstring) =
+fun xml_of_theref thyid typ xstring =
 let
-val guh = theID2guh ["IsacKnowledge", thyid, typ, xstring]
+val guh = Celem.theID2guh ["IsacKnowledge", thyid, typ, xstring]
 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
 in
 XML.Elem (("KESTOREREF", []),[
 XML.Elem (("TAG", []), [XML.Text typ']),
 XML.Elem (("ID", []), [XML.Text xstring]),
 | xml_of_contthy (Rtools.ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
 				reword, asms, lhs, rhs, result, resasms, asmrls}) =
 XML.Elem (("CONTEXTDATA", []), [
 XML.Elem (("GUH", []), [XML.Text thm]),
 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
-xml_of_cterm (subst2str' bdvs)]),
+xml_of_cterm (Celem.subst2str' bdvs)]),
 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
 XML.Elem (("APPLTO", []), [xml_of_term applto]),
 XML.Elem (("APPLAT", []), [xml_of_term applat]),
 XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
 XML.Elem (("ID", []), [XML.Text reword])]),
 | xml_of_contthy (Rtools.ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
 XML.Elem (("CONTEXTDATA", []), [
 XML.Elem (("GUH", []), [XML.Text rls]),
 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
-xml_of_cterm (subst2str' bdvs)]),
+xml_of_cterm (Celem.subst2str' bdvs)]),
-XML.Elem (("INSTANTIATED", []), [xml_of_cterm (subst2str' bdvs)]),
+XML.Elem (("INSTANTIATED", []), [xml_of_cterm (Celem.subst2str' bdvs)]),
 XML.Elem (("APPLTO", []), [xml_of_term applto]),
 XML.Elem (("RESULT", []), [xml_of_term result]),
 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
 | xml_of_contthy (Rtools.ContNOrew {thyID = _, thm_rls, applto}) =
 | xml_of_contthy (Rtools.ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
 XML.Elem (("CONTEXTDATA", []), [
 XML.Elem (("GUH", []), [XML.Text thm_rls]),
 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
-xml_of_cterm (subst2str' bdvs)]),
+xml_of_cterm (Celem.subst2str' bdvs)]),
 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
 XML.Elem (("APPLTO", []), [xml_of_term applto])])
 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
 XML.Elem (("CONTEXTDATA", []), [

changeset 59405	49d7d410b83c
parent 59393	4274a44ec183
child 59408	0b11cdcb1bea