1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Tue Sep 10 10:47:18 2019 +0200
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Tue Sep 10 16:13:28 2019 +0200
     1.3 @@ -11,11 +11,15 @@
     1.4    ML_file datatypes.sml
     1.5    ML_file "pbl-met-hierarchy.sml"
     1.6    ML_file "thy-hierarchy.sml" 
     1.7 -(*ML_file "interface-xml.sml"       --- rm libisabelle ---*)
     1.8 -(*ML_file interface.sml             --- rm libisabelle ---*)
     1.9 +  ML_file "interface-xml.sml"
    1.10 +  ML_file interface.sml
    1.11  (*declare [[ML_print_depth = 999]]*)
    1.12  ML \<open>
    1.13  \<close> ML \<open>
    1.14 + "XML.tree"
    1.15 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    1.16 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    1.17 +\<close> ML \<open>
    1.18  \<close>
    1.19  
    1.20  end

     2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Tue Sep 10 10:47:18 2019 +0200
     2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Tue Sep 10 16:13:28 2019 +0200
     2.3 @@ -408,8 +408,10 @@
     2.4    | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
     2.5  fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
     2.6    | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
     2.7 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
     2.8  
     2.9 -fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Ctree.ocalhd) =
    2.10 +fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Ctree.ocalhd) = "XML.tree"
    2.11 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    2.12    XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
    2.13      XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
    2.14      xml_of_model gfr pre,
    2.15 @@ -777,8 +779,11 @@
    2.16        XML.Text ((if model_ok then "correct" else "incorrect"))]),
    2.17      XML.Elem (("PROGRAM", []), [xml_of_src scr]),
    2.18      xml_of_model pbl pre])
    2.19 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    2.20  
    2.21 -fun xml_of_calcchanged calcid tag old del new = (*TODO: make analogous to xml_to_calcchanged*)
    2.22 +fun xml_of_calcchanged calcid tag old del new = "XML.tree"
    2.23 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    2.24 +  (*TODO: make analogous to xml_to_calcchanged*)
    2.25    XML.Elem ((tag, []),[
    2.26      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    2.27      XML.Elem (("CALCCHANGED", []), [

     3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml	Tue Sep 10 10:47:18 2019 +0200
     3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml	Tue Sep 10 16:13:28 2019 +0200
     3.3 @@ -15,62 +15,86 @@
     3.4  *)
     3.5  
     3.6  (**FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
     3.7 -fun adduserOK2xml (calcid : Celem.calcID) (userid : Celem.iterID) =
     3.8 +fun adduserOK2xml (calcid : Celem.calcID) (userid : Celem.iterID) = "XML.tree"
     3.9 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.10    XML.Elem (("ADDUSER", []),
    3.11      [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.12      XML.Elem (("USERID", []), [XML.Text (string_of_int userid)])])
    3.13 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.14  
    3.15 -fun calctreeOK2xml (calcid : Celem.calcID) = 
    3.16 +fun calctreeOK2xml (calcid : Celem.calcID) = "XML.tree"
    3.17 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.18    XML.Elem (("CALCTREE", []),
    3.19      [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])    
    3.20 -fun deconstructcalctreeOK2xml (calcid : Celem.calcID) = 
    3.21 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.22 +fun deconstructcalctreeOK2xml (calcid : Celem.calcID) = "XML.tree"
    3.23 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.24    XML.Elem (("DELCALC", []),
    3.25      [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])    
    3.26 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.27  
    3.28 -fun iteratorOK2xml (calcid : Celem.calcID) (p : Ctree.pos')= 
    3.29 +fun iteratorOK2xml (calcid : Celem.calcID) (p : Ctree.pos') = "XML.tree"
    3.30 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.31    XML.Elem (("CALCITERATOR", []),
    3.32      [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.33      xml_of_pos "POSITION" p])
    3.34 -fun iteratorERROR2xml  (calcid : Celem.calcID) = 
    3.35 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.36 +fun iteratorERROR2xml  (calcid : Celem.calcID) = "XML.tree"
    3.37 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.38    XML.Elem (("CALCITERATOR", []),
    3.39      [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.40      XML.Elem (("ERROR", []), [XML.Text " iteratorERROR2xml: pos does not exist "])])
    3.41 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.42  
    3.43 -fun sysERROR2xml (calcid : Celem.calcID) str =
    3.44 +fun sysERROR2xml (calcid : Celem.calcID) str = "XML.tree"
    3.45 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.46    XML.Elem (("SYSERROR", []),
    3.47      [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.48      XML.Elem (("ERROR", []), [XML.Text (if str = "" then " ERROR in kernel " else str)])])
    3.49 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.50  
    3.51 -fun refformulaOK2xml (calcid : Celem.calcID) p (Ctree.Form t) = 
    3.52 +fun refformulaOK2xml (calcid : Celem.calcID) p (Ctree.Form t) = "XML.tree"
    3.53 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.54        XML.Elem (("REFFORMULA", []),
    3.55          [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.56          XML.Elem (("CALCFORMULA", []), [
    3.57            xml_of_pos "POSITION" p,
    3.58            xml_of_term_NEW t])])
    3.59 -  | refformulaOK2xml (calcid : Celem.calcID) p (Ctree.ModSpec modspec) = 
    3.60 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.61 +  | refformulaOK2xml (calcid : Celem.calcID) p (Ctree.ModSpec modspec) = "XML.tree"
    3.62 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.63        XML.Elem (("REFFORMULA", []), [
    3.64          XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.65          (*L.Elem (("CALCHEAD*) xml_of_posmodspec (p, modspec)])
    3.66 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.67  
    3.68 -fun gettacticOK2xml (calcid : Celem.calcID) tac = 
    3.69 +fun gettacticOK2xml (calcid : Celem.calcID) tac = "XML.tree"
    3.70 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.71    XML.Elem (("GETTACTIC", []),[
    3.72      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.73      xml_of_tac tac])
    3.74 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.75  
    3.76 -fun gettacticERROR2xml (calcid : Celem.calcID) str = 
    3.77 +fun gettacticERROR2xml (calcid : Celem.calcID) str = "XML.tree"
    3.78 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.79    XML.Elem (("GETTACTIC", []),[
    3.80      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.81      XML.Elem (("ERROR", []), [XML.Text  str])])
    3.82 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.83  
    3.84 -fun applicabletacticsOK calcid tacs =
    3.85 +fun applicabletacticsOK calcid tacs = "XML.tree"
    3.86 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.87    XML.Elem (("APPLICABLETACTICS", []), [
    3.88      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.89      XML.Elem (("TACLIST", []), (map xml_of_tac tacs))])
    3.90 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.91  
    3.92 -fun getasmsOK2xml (calcid : Celem.calcID) terms = 
    3.93 +fun getasmsOK2xml (calcid : Celem.calcID) terms = "XML.tree"
    3.94 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
    3.95    XML.Elem (("ASSUMPTIONS", []), [
    3.96      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    3.97      XML.Elem (("ASMLIST", []), (map xml_of_term_NEW terms))])
    3.98 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
    3.99  
   3.100  (*WN0502 getaccuasmsOK2xml @see ME/ctree: type asms: illdesigned, thus not used*)
   3.101  fun formula2xml j term = (*TODO.WN050211: use for _all_ <FORMULA>*)
   3.102 @@ -95,45 +119,62 @@
   3.103     getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
   3.104     *)
   3.105  
   3.106 -fun getintervalOK (calcid : Celem.calcID) fs = 
   3.107 +fun getintervalOK (calcid : Celem.calcID) fs = "XML.tree"
   3.108 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.109        XML.Elem (("GETELEMENTSFROMTO", []),
   3.110          [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.111          XML.Elem (("FORMHEADS", []), map xml_of_posterm fs)])
   3.112 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.113  
   3.114 -fun appendformulaOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') = 
   3.115 +fun appendformulaOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') = "XML.tree"
   3.116 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.117    xml_of_calcchanged calcid "APPENDFORMULA" old del new
   3.118 -fun appendformulaERROR2xml (calcid : Celem.calcID) e = 
   3.119 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.120 +fun appendformulaERROR2xml (calcid : Celem.calcID) e = "XML.tree"
   3.121 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.122    XML.Elem (("APPENDFORMULA", []), [
   3.123      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.124      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
   3.125 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.126  
   3.127  fun replaceformulaOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') = 
   3.128    xml_of_calcchanged calcid "REPLACEFORMULA" old del new
   3.129 -fun replaceformulaERROR2xml (calcid : Celem.calcID) e = 
   3.130 +fun replaceformulaERROR2xml (calcid : Celem.calcID) e = "XML.tree"
   3.131 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.132 +
   3.133    XML.Elem (("REPLACEFORMULA", []), [
   3.134      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.135      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
   3.136 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.137  
   3.138 -fun message2xml (calcid : Celem.calcID) e = 
   3.139 +fun message2xml (calcid : Celem.calcID) e = "XML.tree"
   3.140 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.141    XML.Elem (("MESSAGE", []), [
   3.142      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.143      XML.Elem (("STRING", []), [XML.Text e])])
   3.144 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.145  
   3.146 -fun setnexttactic2xml (calcid : Celem.calcID) e = 
   3.147 +fun setnexttactic2xml (calcid : Celem.calcID) e = "XML.tree"
   3.148 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.149    XML.Elem (("SETNEXTTACTIC", []), [
   3.150      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.151      XML.Elem (("MESSAGE", []), [XML.Text e])])
   3.152 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.153  
   3.154 -fun fetchproposedtacticOK2xml (calcid : Celem.calcID) tac (errpatIDs : Rule.errpatID list) = 
   3.155 +fun fetchproposedtacticOK2xml (calcid : Celem.calcID) tac (errpatIDs : Rule.errpatID list) = "XML.tree"
   3.156 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.157    XML.Elem (("NEXTTAC", []), [
   3.158      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.159      XML.Elem (("TACTICERRORPATTERNS", []), [xml_of_strs errpatIDs]),
   3.160      xml_of_tac tac])
   3.161 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.162  
   3.163 -fun fetchproposedtacticERROR2xml (calcid : Celem.calcID) e = 
   3.164 +fun fetchproposedtacticERROR2xml (calcid : Celem.calcID) e = "XML.tree"
   3.165 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.166    XML.Elem (("NEXTTAC", []), [
   3.167      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.168      XML.Elem (("ERROR", []), [XML.Text e])])
   3.169 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.170  
   3.171  (*. UNCHANGED: the pos' of the active formula autocalculate has been applied at
   3.172      DELETED:   last pos' of the succesional sequence of formulae prob. deleted
   3.173 @@ -141,46 +182,60 @@
   3.174  .*)
   3.175  fun autocalculateOK2xml (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') = 
   3.176    xml_of_calcchanged calcid "AUTOCALC" old del new
   3.177 -fun autocalculateERROR2xml (calcid : Celem.calcID) e = 
   3.178 +fun autocalculateERROR2xml (calcid : Celem.calcID) e = "XML.tree"
   3.179 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.180    XML.Elem (("AUTOCALC", []), [
   3.181      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.182      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
   3.183 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.184  
   3.185  fun interStepsOK (calcid : Celem.calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
   3.186     xml_of_calcchanged calcid "INTERSTEPS" old del new
   3.187 -fun interStepsERROR (calcid : Celem.calcID) e = 
   3.188 +fun interStepsERROR (calcid : Celem.calcID) e = "XML.tree"
   3.189 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.190    XML.Elem (("INTERSTEPS", []), [
   3.191      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.192      XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
   3.193 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.194  
   3.195  fun calcMessage2xml (cI: Celem.calcID) e =
   3.196      writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   3.197  	     "  <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
   3.198  	     "@@@@@end@@@@@");
   3.199  
   3.200 -fun modifycalcheadOK2xml (calcid : Celem.calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : Ctree.ocalhd) =
   3.201 +fun modifycalcheadOK2xml (calcid : Celem.calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : Ctree.ocalhd) = "XML.tree"
   3.202 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.203    XML.Elem (("MODIFYCALCHEAD", []), [
   3.204      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.205      XML.Elem (("STATUS", []), [
   3.206        XML.Text (if complete then "complete" else "incomplete")]),
   3.207      xml_of_modspec chd])
   3.208 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.209  
   3.210 -fun contextthyOK2xml calcid contthy = 
   3.211 +fun contextthyOK2xml calcid contthy = "XML.tree"
   3.212 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.213    XML.Elem (("CONTEXTTHY", []), [
   3.214      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.215      xml_of_contthy contthy])
   3.216 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.217  
   3.218 -fun contextpblOK2xml calcid contpbl = 
   3.219 +fun contextpblOK2xml calcid contpbl = "XML.tree"
   3.220 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.221    XML.Elem (("CONTEXTPBL", []), [
   3.222      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.223      xml_of_matchpbl contpbl])
   3.224 -fun contextmetOK2xml calcid contmet = 
   3.225 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.226 +fun contextmetOK2xml calcid contmet = "XML.tree"
   3.227 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.228    XML.Elem (("CONTEXTMET", []), [
   3.229      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.230      xml_of_matchmet contmet])
   3.231 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.232  
   3.233 -fun findFillpatterns2xml (calcid : Celem.calcID) pattIDs = 
   3.234 +fun findFillpatterns2xml (calcid : Celem.calcID) pattIDs = "XML.tree"
   3.235 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
   3.236    XML.Elem (("FINDFILLPATTERNS", []), [
   3.237      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
   3.238      xml_of_strs pattIDs])
   3.239 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
   3.240  

     4.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Tue Sep 10 10:47:18 2019 +0200
     4.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Tue Sep 10 16:13:28 2019 +0200
     4.3 @@ -11,51 +11,51 @@
     4.4  
     4.5  signature KERNEL =
     4.6    sig
     4.7 -    val appendFormula : Celem.calcID -> Rule.cterm' -> XML.tree (*unit future*)
     4.8 -    val autoCalculate : Celem.calcID -> Solve.auto -> XML.tree (*unit future*)
     4.9 -    val applyTactic : Celem.calcID -> Ctree.pos' -> Tactic.input -> XML.tree
    4.10 -    val CalcTree : Selem.fmz list -> XML.tree
    4.11 -    val checkContext : Celem.calcID -> Ctree.pos' -> Celem.guh -> XML.tree
    4.12 -    val DEconstrCalcTree : Celem.calcID -> XML.tree
    4.13 -    val fetchApplicableTactics : Celem.calcID -> int -> Ctree.pos' -> XML.tree
    4.14 -    val fetchProposedTactic : Celem.calcID -> XML.tree
    4.15 -    val findFillpatterns : Celem.calcID -> Rule.errpatID -> XML.tree
    4.16 -    val getAccumulatedAsms : Celem.calcID -> Ctree.pos' -> XML.tree
    4.17 -    val getActiveFormula : Celem.calcID -> XML.tree
    4.18 -    val getAssumptions : Celem.calcID -> Ctree.pos' -> XML.tree
    4.19 -    val getFormulaeFromTo : Celem.calcID -> Ctree.pos' -> Ctree.pos' -> int -> bool -> XML.tree
    4.20 -    val getTactic : Celem.calcID -> Ctree.pos' -> XML.tree
    4.21 -    val initContext : Celem.calcID -> Celem.ketype -> Ctree.pos' -> XML.tree
    4.22 -    val inputFillFormula: Celem.calcID -> string -> XML.tree
    4.23 -    val interSteps : Celem.calcID -> Ctree.pos' -> XML.tree
    4.24 -    val Iterator : Celem.calcID -> XML.tree
    4.25 +    val appendFormula : Celem.calcID -> Rule.cterm' -> string(*XML.tree (*unit future*)*)
    4.26 +    val autoCalculate : Celem.calcID -> Solve.auto -> string(*XML.tree (*unit future*)*)
    4.27 +    val applyTactic : Celem.calcID -> Ctree.pos' -> Tactic.input -> string(*XML.tree*)
    4.28 +    val CalcTree : Selem.fmz list -> string(*XML.tree*)
    4.29 +    val checkContext : Celem.calcID -> Ctree.pos' -> Celem.guh -> string(*XML.tree*)
    4.30 +    val DEconstrCalcTree : Celem.calcID -> string(*XML.tree*)
    4.31 +    val fetchApplicableTactics : Celem.calcID -> int -> Ctree.pos' -> string(*XML.tree*)
    4.32 +    val fetchProposedTactic : Celem.calcID -> string(*XML.tree*)
    4.33 +    val findFillpatterns : Celem.calcID -> Rule.errpatID -> string(*XML.tree*)
    4.34 +    val getAccumulatedAsms : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.35 +    val getActiveFormula : Celem.calcID -> string(*XML.tree*)
    4.36 +    val getAssumptions : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.37 +    val getFormulaeFromTo : Celem.calcID -> Ctree.pos' -> Ctree.pos' -> int -> bool -> string(*XML.tree*)
    4.38 +    val getTactic : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.39 +    val initContext : Celem.calcID -> Celem.ketype -> Ctree.pos' -> string(*XML.tree*)
    4.40 +    val inputFillFormula: Celem.calcID -> string -> string(*XML.tree*)
    4.41 +    val interSteps : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.42 +    val Iterator : Celem.calcID -> string(*XML.tree*)
    4.43      val IteratorTEST : Celem.calcID -> Celem.iterID
    4.44 -    val modelProblem : Celem.calcID -> XML.tree
    4.45 -    val modifyCalcHead : Celem.calcID -> Inform.icalhd -> XML.tree
    4.46 -    val moveActiveCalcHead : Celem.calcID -> XML.tree
    4.47 -    val moveActiveDown : Celem.calcID -> XML.tree
    4.48 -    val moveActiveFormula : Celem.calcID -> Ctree.pos' -> XML.tree
    4.49 -    val moveActiveLevelDown : Celem.calcID -> XML.tree
    4.50 -    val moveActiveLevelUp : Celem.calcID -> XML.tree
    4.51 -    val moveActiveRoot : Celem.calcID -> XML.tree
    4.52 -    val moveActiveRootTEST : Celem.calcID -> XML.tree
    4.53 -    val moveActiveUp : Celem.calcID -> XML.tree
    4.54 -    val moveCalcHead : Celem.calcID -> Ctree.pos' -> XML.tree
    4.55 -    val moveDown : Celem.calcID -> Ctree.pos' -> XML.tree
    4.56 -    val moveLevelDown : Celem.calcID -> Ctree.pos' -> XML.tree
    4.57 -    val moveLevelUp : Celem.calcID -> Ctree.pos' -> XML.tree
    4.58 -    val moveRoot : Celem.calcID -> XML.tree
    4.59 -    val moveUp : Celem.calcID -> Ctree.pos' -> XML.tree
    4.60 -    val refFormula : Celem.calcID -> Ctree.pos' -> XML.tree
    4.61 -    val refineProblem : Celem.calcID -> Ctree.pos' -> Celem.guh -> XML.tree
    4.62 -    val replaceFormula : Celem.calcID -> Rule.cterm' -> XML.tree
    4.63 -    val requestFillformula : Celem.calcID -> Rule.errpatID * Celem.fillpatID -> XML.tree
    4.64 -    val resetCalcHead : Celem.calcID -> XML.tree
    4.65 -    val setContext : Celem.calcID -> Ctree.pos' -> Celem.guh -> XML.tree
    4.66 -    val setMethod : Celem.calcID -> Celem.metID -> XML.tree
    4.67 -    val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
    4.68 -    val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
    4.69 -    val setTheory : Celem.calcID -> Rule.thyID -> XML.tree
    4.70 +    val modelProblem : Celem.calcID -> string(*XML.tree*)
    4.71 +    val modifyCalcHead : Celem.calcID -> Inform.icalhd -> string(*XML.tree*)
    4.72 +    val moveActiveCalcHead : Celem.calcID -> string(*XML.tree*)
    4.73 +    val moveActiveDown : Celem.calcID -> string(*XML.tree*)
    4.74 +    val moveActiveFormula : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.75 +    val moveActiveLevelDown : Celem.calcID -> string(*XML.tree*)
    4.76 +    val moveActiveLevelUp : Celem.calcID -> string(*XML.tree*)
    4.77 +    val moveActiveRoot : Celem.calcID -> string(*XML.tree*)
    4.78 +    val moveActiveRootTEST : Celem.calcID -> string(*XML.tree*)
    4.79 +    val moveActiveUp : Celem.calcID -> string(*XML.tree*)
    4.80 +    val moveCalcHead : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.81 +    val moveDown : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.82 +    val moveLevelDown : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.83 +    val moveLevelUp : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.84 +    val moveRoot : Celem.calcID -> string(*XML.tree*)
    4.85 +    val moveUp : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.86 +    val refFormula : Celem.calcID -> Ctree.pos' -> string(*XML.tree*)
    4.87 +    val refineProblem : Celem.calcID -> Ctree.pos' -> Celem.guh -> string(*XML.tree*)
    4.88 +    val replaceFormula : Celem.calcID -> Rule.cterm' -> string(*XML.tree*)
    4.89 +    val requestFillformula : Celem.calcID -> Rule.errpatID * Celem.fillpatID -> string(*XML.tree*)
    4.90 +    val resetCalcHead : Celem.calcID -> string(*XML.tree*)
    4.91 +    val setContext : Celem.calcID -> Ctree.pos' -> Celem.guh -> string(*XML.tree*)
    4.92 +    val setMethod : Celem.calcID -> Celem.metID -> string(*XML.tree*)
    4.93 +    val setNextTactic : Celem.calcID -> Tactic.input -> string(*XML.tree*)
    4.94 +    val setProblem : Celem.calcID -> Celem.pblID -> string(*XML.tree*)
    4.95 +    val setTheory : Celem.calcID -> Rule.thyID -> string(*XML.tree*)
    4.96  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    4.97      (* NONE *)
    4.98  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.99 @@ -64,8 +64,8 @@
   4.100  (**)
   4.101  structure Kernel(**): KERNEL(**) =
   4.102  struct
   4.103 +(**)
   4.104  open Ctree
   4.105 -(**)
   4.106  (* encode "Isabelle"-strings as seen by the user to the
   4.107     format accepted by Isabelle.
   4.108     encode "^" ---> "^^^"; see Knowledge/Atools.thy;
   4.109 @@ -714,6 +714,5 @@
   4.110          end
   4.111      | (msg, _) => message2xml cI msg
   4.112    end
   4.113 -(**)
   4.114 -end
   4.115 -(**)
   4.116 +
   4.117 +(**)end(**)

     5.1 --- a/src/Tools/isac/Build_Isac.thy	Tue Sep 10 10:47:18 2019 +0200
     5.2 +++ b/src/Tools/isac/Build_Isac.thy	Tue Sep 10 16:13:28 2019 +0200
     5.3 @@ -95,7 +95,7 @@
     5.4  ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
     5.5  ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
     5.6  ML \<open>Math_Engine.me;\<close>
     5.7 -ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
     5.8 +text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
     5.9  ML \<open>list_rls\<close>
    5.10                                                           
    5.11  ML \<open>Prog_Expr.eval_occurs_in\<close>

     6.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Tue Sep 10 10:47:18 2019 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Tue Sep 10 16:13:28 2019 +0200
     6.3 @@ -31,7 +31,7 @@
     6.4              ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
     6.5                "KantenSenkrecht s_s", "KantenOben o_o"]),
     6.6            ("#Find", ["GesamtLaenge l_l"])],
     6.7 -        Rule.e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))];\<close>
     6.8 +        Rule.e_rls, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
     6.9  
    6.10  setup \<open>KEStore_Elems.add_mets
    6.11      [Specify.prep_met thy "met_algein" [] Celem.e_metID

     7.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Sep 10 10:47:18 2019 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Sep 10 16:13:28 2019 +0200
     7.3 @@ -65,11 +65,13 @@
     7.4    and "IsacScripts" is determined in KEStore.thy.
     7.5  \<close>
     7.6  ML \<open>
     7.7 -val thydata_list = 
     7.8 +val thydata_list = []
     7.9 +(*//--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------\\* )
    7.10    collect_part       "IsacKnowledge" knowledge_parent knowthys' @
    7.11    (map (collect_isab "Isabelle") rlsthmsNOTisac) @
    7.12    collect_part       "IsacScripts" proglang_parent progthys'
    7.13  : (Celem.theID * Celem.thydata) list
    7.14 +( *\\--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------//*)
    7.15  \<close>
    7.16  setup \<open>KEStore_Elems.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
    7.17  
    7.18 @@ -89,6 +91,7 @@
    7.19            @{thm  diff_exp_chain}])]]
    7.20  \<close>
    7.21  
    7.22 +(*//--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------\* )
    7.23  setup \<open>
    7.24  KEStore_Elems.insert_fillpats
    7.25    [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
    7.26 @@ -104,6 +107,7 @@
    7.27        TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Celem.fillpat list))
    7.28    ]
    7.29  \<close>
    7.30 +( *\\--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------//*)
    7.31  
    7.32  subsubsection \<open>Error patterns for calculation with rationals\<close>
    7.33