Mercurial Mercurial > wneuper > isac / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
isac-java/src/java/isac/bridge/xml/IsaToJava.scala
author Walther Neuper <walther.neuper@jku.at>
Fri, 26 Mar 2021 10:45:05 +0100
changeset 5239 b4e3883d7b66
parent 5229 6bf0e95981e3
permissions -rw-r--r--
reset mathematics-engine to Isabelle2015

note: for this version libisabelle was available,
which connects front-end (Java) and back-end (Isabelle/ML) 
     1 /* 

     2  * @author Walther Neuper

     3  * Copyright (c) due to license terms

     4  * Created on Jul 14, 2015

     5  * Institute for Softwaretechnology, Graz University of Technology, Austria.

     6  */

     7 

     8 package isac.bridge.xml

     9 

    10 import isac.bridge.CChanged

    11 import isac.bridge.CEvent

    12 import isac.bridge.CMessage

    13 import isac.util.formulae.Assumptions

    14 import isac.util.formulae.CalcFormula

    15 import isac.util.formulae.CalcHead

    16 import isac.util.formulae.CalcHeadSimpleID

    17 import isac.util.formulae.Context

    18 import isac.util.formulae.ContextTheory

    19 import isac.util.formulae.Formula

    20 import isac.util.formulae.HierarchyKey

    21 import isac.util.formulae.KEStoreKey

    22 import isac.util.formulae.Model

    23 import isac.util.formulae.ModelItem

    24 import isac.util.formulae.ModelItemList

    25 import isac.util.formulae.Position

    26 import isac.util.formulae.Specification

    27 import isac.util.Message

    28 

    29 import edu.tum.cs.isabelle.api.XML

    30 

    31 import java.util.ArrayList

    32 import java.util.Vector

    33 import java.math.BigInteger

    34 import scala.math.BigInt

    35 import scala.collection.JavaConverters._

    36 

    37 /**

    38  * Convert results of JSystem.invoke(Operations.* to Java-objects.

    39  * Conversions use Scala's pattern matching, which is not available in Java.

    40  * 

    41  * The sequence in the kernel's signature below is maintained.

    42  */

    43 object IsaToJava {

    44   

    45   //is the tree (expected to contain data going to Dialog) a message ?

    46   //  CALCMESSAGE is excluded, because this goes to Dialog as CCEvent

    47   def is_message(t: XML.Tree): java.lang.Boolean = t match {

    48     case

    49       XML.Elem(("MESSAGE", Nil), List(

    50         XML.Elem(("CALCID", Nil), List(XML.Text (_))),

    51         XML.Elem(("STRING", Nil), List(XML.Text (_))))) => true

    52     case

    53       XML.Elem(("SYSERROR", Nil), List(

    54         XML.Elem(("CALCID", Nil), List(XML.Text (_))),

    55         XML.Elem(("ERROR", Nil), List(XML.Text (_))))) => true

    56     case

    57       XML.Elem((_/*"SETNEXTTACTIC"*/, Nil), List(

    58         XML.Elem(("CALCID", Nil), List(XML.Text (_))),

    59         XML.Elem(("MESSAGE", Nil), List(XML.Text (_))))) => true

    60     case _ => false //expected data going to Dialog

    61   }

    62   def is_syserror(t: XML.Tree): java.lang.Boolean = t match {

    63     case

    64       XML.Elem(("SYSERROR", Nil), List(

    65         XML.Elem(("CALCID", Nil), List(XML.Text (_))),

    66         XML.Elem(("ERROR", Nil), List(XML.Text (_))))) => true

    67     case _ => false

    68   }

    69 

    70 /* from isabisac/src/Tools/Frontend/interface.sml + XML generation

    71 signature MATH_ENGINE =

    72   sig

    73     val appendFormula : calcID -> cterm' -> XML.tree

    74           appendformulaOK2xml

    75           appendformulaERROR2xml

    76           sysERROR2xml

    77     val autoCalculate : calcID -> auto -> XML.tree

    78           autocalculateOK2xml

    79           autocalculateERROR2xml

    80           sysERROR2xml

    81     val applyTactic : calcID -> pos' -> tac -> XML.tree

    82           autocalculateOK2xml

    83           autocalculateERROR2xml

    84     val CalcTree : fmz list -> XML.tree

    85           calctreeOK2xml

    86           sysERROR2xml

    87     val checkContext : calcID -> pos' -> guh -> XML.tree

    88           message2xml

    89           contextthyOK2xml

    90           sysERROR2xml

    91     val DEconstrCalcTree : calcID -> XML.tree

    92           deconstructcalctreeOK2xml

    93     val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

    94           applicabletacticsOK

    95           sysERROR2xml

    96     val fetchProposedTactic : calcID -> XML.tree

    97           fetchproposedtacticOK2xml

    98           fetchproposedtacticERROR2xml

    99           sysERROR2xml

   100     val findFillpatterns : calcID -> errpatID -> XML.tree

   101           findFillpatterns2xml

   102     val getAccumulatedAsms : calcID -> pos' -> XML.tree

   103           getasmsOK2xml

   104           sysERROR2xml

   105     val getActiveFormula : calcID -> XML.tree

   106           iteratorOK2xml

   107     val getAssumptions : calcID -> pos' -> XML.tree

   108           getasmsOK2xml

   109           sysERROR2xml

   110     val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

   111           getintervalOK

   112           sysERROR2xml

   113     val getTactic : calcID -> pos' -> XML.tree

   114           gettacticOK2xml

   115           gettacticERROR2xml

   116           sysERROR2xml

   117     val initContext : calcID -> ketype -> pos' -> XML.tree

   118           message2xml

   119           contextthyOK2xml

   120           sysERROR2xml

   121     val inputFillFormula: calcID -> string -> XML.tree

   122           autocalculateOK2xml

   123           autocalculateERROR2xml

   124           message2xml

   125     val interSteps : calcID -> pos' -> XML.tree

   126           interStepsOK

   127           interStepsERROR

   128           sysERROR2xml

   129     val Iterator : calcID -> XML.tree

   130           adduserOK2xml

   131           sysERROR2xml

   132     val IteratorTEST : calcID -> iterID

   133     val modelProblem : calcID -> XML.tree

   134           modifycalcheadOK2xml

   135           sysERROR2xml

   136     val modifyCalcHead : calcID -> icalhd -> XML.tree

   137           modifycalcheadOK2xml

   138           sysERROR2xml

   139     val moveActiveCalcHead : calcID -> XML.tree

   140           iteratorOK2xml

   141           sysERROR2xml

   142     val moveActiveDown : calcID -> XML.tree

   143           iteratorOK2xml

   144           iteratorERROR2xml

   145           sysERROR2xml

   146     val moveActiveFormula : calcID -> pos' -> XML.tree

   147           iteratorOK2xml

   148           sysERROR2xml

   149     val moveActiveLevelDown : calcID -> XML.tree

   150           iteratorOK2xml

   151           iteratorERROR2xml

   152           sysERROR2xml

   153     val moveActiveLevelUp : calcID -> XML.tree

   154           iteratorOK2xml

   155           iteratorERROR2xml

   156           sysERROR2xml

   157     val moveActiveRoot : calcID -> XML.tree

   158           iteratorOK2xml

   159           sysERROR2xml

   160     val moveActiveRootTEST : calcID -> XML.tree

   161     val moveActiveUp : calcID -> XML.tree

   162           iteratorOK2xml

   163           iteratorERROR2xml

   164           sysERROR2xml

   165     val moveCalcHead : calcID -> pos' -> XML.tree

   166           iteratorOK2xml

   167           iteratorERROR2xml

   168           sysERROR2xml

   169     val moveDown : calcID -> pos' -> XML.tree

   170           iteratorOK2xml

   171           iteratorERROR2xml

   172           sysERROR2xml

   173     val moveLevelDown : calcID -> pos' -> XML.tree

   174           iteratorOK2xml

   175           iteratorERROR2xml

   176           sysERROR2xml

   177     val moveLevelUp : calcID -> pos' -> XML.tree

   178           iteratorOK2xml

   179           iteratorERROR2xml

   180           sysERROR2xml

   181     val moveRoot : calcID -> XML.tree

   182           iteratorOK2xml

   183           sysERROR2xml

   184     val moveUp : calcID -> pos' -> XML.tree

   185           iteratorOK2xml

   186           iteratorERROR2xml

   187           sysERROR2xml

   188     val refFormula : calcID -> pos' -> XML.tree

   189           refformulaOK2xml

   190           sysERROR2xml

   191     val refineProblem : calcID -> pos' -> guh -> XML.tree

   192           xml_of_matchpbl

   193           sysERROR2xml

   194     val replaceFormula : calcID -> cterm' -> XML.tree

   195           replaceformulaOK2xml

   196           replaceformulaERROR2xml

   197           sysERROR2xml

   198     val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

   199           autocalculateOK2xml

   200           autocalculateERROR2xml

   201     val resetCalcHead : calcID -> XML.tree

   202           modifycalcheadOK2xml

   203           sysERROR2xml

   204     val setContext : calcID -> pos' -> guh -> XML.tree

   205           message2xml

   206           autocalculateOK2xml

   207           sysERROR2xml

   208     val setMethod : calcID -> metID -> XML.tree

   209           modifycalcheadOK2xml

   210           sysERROR2xml

   211     val setNextTactic : calcID -> tac -> XML.tree

   212           setnexttactic2xml

   213           sysERROR2xml

   214     val setProblem : calcID -> pblID -> XML.tree

   215           modifycalcheadOK2xml

   216           sysERROR2xml

   217     val setTheory : calcID -> thyID -> XML.tree

   218           modifycalcheadOK2xml

   219           sysERROR2xml

   220   end

   221 */

   222   

   223   //fun appendFormula : calcID -> cterm' -> XML.tree

   224   def append_form_out(t: XML.Tree): IntCEvent = t match {

   225     case

   226       XML.Elem(("APPENDFORMULA", Nil), List(

   227         XML.Elem(("CALCID", Nil), List(XML.Text (calcid))),

   228         cevent_xml))

   229       => new IntCEvent(new java.lang.Integer(calcid), 

   230            DataTypes.xml_to_CEvent(cevent_xml))

   231     case _ => throw new IllegalArgumentException("append_form_out wrong arg: " + t)

   232   }

   233 

   234   //fun autoCalculate : calcID -> auto -> XML.tree

   235   def auto_calc_out(t: XML.Tree): IntCEvent = t match {

   236     case

   237       XML.Elem(("AUTOCALC", Nil), List(

   238         XML.Elem(("CALCID", Nil), List(XML.Text (calcid))),

   239         cevent_xml))

   240       => new IntCEvent(new java.lang.Integer(calcid), 

   241            DataTypes.xml_to_CEvent(cevent_xml))

   242     case _ => throw new IllegalArgumentException("auto_calc_out wrong arg: " + t)

   243   }

   244 

   245   //fun applyTactic : calcID -> pos' -> tac -> XML.tree  ...NOT IMPL. IN isac-java WN150813

   246 

   247   //fun CalcTree : fmz list -> XML.tree

   248   def calc_tree_out(t: XML.Tree): java.lang.Integer = t match {

   249     case

   250        XML.Elem(("CALCTREE", Nil), List(

   251          XML.Elem(("CALCID", Nil), List(XML.Text(i)))))

   252       => new Integer(i)

   253     case //TODO catch in Java

   254        XML.Elem(("SYSERROR", Nil), List(

   255          XML.Elem(("CALCID", Nil), List(XML.Text(i))),

   256          XML.Elem(("ERROR", Nil), List(XML.Text(msg)))))

   257       => throw new IllegalArgumentException("calc_tree_out SYSERROR wrong arg: " + t)

   258     case _ => throw new IllegalArgumentException("calc_tree_out wrong arg: " + t)

   259   }

   260 

   261   //fun checkContext : calcID -> pos' -> guh -> XML.tree

   262   def check_ctxt_out(t: XML.Tree): ContextTheory = t match {

   263     case

   264       XML.Elem(("CONTEXTTHY", Nil), List(

   265         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   266         contthy_xml))

   267       => DataTypes.xml_to_ContextTheory(contthy_xml)

   268     case _ => throw new IllegalArgumentException("check_ctxt_out wrong arg: " + t)

   269   }

   270 

   271   //fun DEconstrCalcTree : calcID -> XML.tree

   272   def del_calc_out(t: XML.Tree): java.lang.Integer = t match {

   273     case

   274       XML.Elem(("DELCALC", Nil), List(

   275         XML.Elem(("CALCID", Nil), List(XML.Text(calcid)))))

   276       => new java.lang.Integer(calcid)

   277     case _ => throw new IllegalArgumentException("del_calc_out wrong arg: " + t)

   278   }

   279 

   280   //fun fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

   281   def fetch_applicable_tacs_out(t: XML.Tree): IntTactics = t match {

   282     case

   283       XML.Elem(("APPLICABLETACTICS", Nil), List(

   284         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   285         tacs_xml))

   286       =>  new IntTactics(new java.lang.Integer(calcid), 

   287             DataTypes.xml_to_VectorTactic(tacs_xml))

   288     case _ => throw new IllegalArgumentException("fetch_applicable_tacs_out wrong arg: " + t)

   289   }

   290 

   291   //fun fetchProposedTactic : calcID -> XML.tree

   292   def fetch_proposed_tac_out(t: XML.Tree): IntTacticErrPats = t match {

   293     case

   294       XML.Elem(("NEXTTAC", Nil), List(

   295         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   296         XML.Elem(("TACTICERRORPATTERNS", Nil), List(errpat_ids)),

   297         tac))

   298       =>  new IntTacticErrPats(new java.lang.Integer(calcid), 

   299             DataTypes.xml_to_VectorString(errpat_ids), DataTypes.xml_to_Tactic(tac))

   300     case _ => throw new IllegalArgumentException("fetch_proposed_tac_out wrong arg: " + t)

   301   }

   302   

   303   //fun findFillpatterns : calcID -> errpatID -> XML.tree

   304   //... only implemented in Math_Engine

   305 

   306   //fun getAccumulatedAsms : calcID -> pos' -> XML.tree

   307   def get_accumulated_asms_out(t: XML.Tree): IntAssumptions = t match {

   308     case

   309       XML.Elem(("ASSUMPTIONS", Nil), List(

   310         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   311         XML.Elem(("ASMLIST", Nil), asms)))

   312        => new IntAssumptions(new java.lang.Integer(calcid), 

   313             new Assumptions(DataTypes.sListToVectorFormula(asms map DataTypes.xml_to_Formula_NEW)))

   314     case _ => throw new IllegalArgumentException("get_accumulated_asms_out wrong arg: " + t)

   315   }

   316 

   317   //fun getActiveFormula : calcID -> XML.tree

   318   def get_active_form_out(t: XML.Tree): IntPosition = t match {

   319     case

   320       XML.Elem(("CALCITERATOR", Nil), List(

   321         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   322         pos_xml))

   323        => new IntPosition(new java.lang.Integer(calcid), 

   324             DataTypes.xml_to_Position(pos_xml))

   325     case _ => throw new IllegalArgumentException("get_SOME_Iterator wrong arg: " + t)

   326   }

   327 

   328   //fun getAssumptions : calcID -> pos' -> XML.tree

   329   def get_asms_out(t: XML.Tree): IntAssumptions = t match {

   330     case

   331       XML.Elem(("ASSUMPTIONS", Nil), List(

   332         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   333         XML.Elem(("ASMLIST", Nil), asms)))

   334        => new IntAssumptions(new java.lang.Integer(calcid), 

   335             new Assumptions(DataTypes.sListToVectorFormula(asms map DataTypes.xml_to_Formula_NEW)))

   336     case _ => throw new IllegalArgumentException("get_asms wrong arg: " + t)

   337   }

   338 

   339   //fun getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

   340   def get_formulae_out(t: XML.Tree): IntFormulas = t match {

   341     case

   342       XML.Elem(("GETELEMENTSFROMTO", Nil), List(

   343         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   344         XML.Elem(("FORMHEADS", Nil), forms)))

   345        => new IntFormulas(new java.lang.Integer(calcid), 

   346             DataTypes.sListToVectorCalcFormula(forms map DataTypes.xml_to_CalcFormula))

   347     case _ => throw new IllegalArgumentException("iterator_out wrong arg: " + t)

   348   }

   349 

   350   //fun getTactic : calcID -> pos' -> XML.tree

   351   def get_tac_out(t: XML.Tree): IntTactic = t match {

   352     case

   353       XML.Elem(("GETTACTIC", Nil), List(

   354         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   355         tac))

   356       => new IntTactic(new java.lang.Integer(calcid), 

   357            DataTypes.xml_to_Tactic(tac))

   358     case _ => throw new IllegalArgumentException("get_tac_out wrong arg: " + t)

   359   }

   360 

   361   //fun initContext : calcID -> ketype -> pos' -> XML.tree

   362   def init_ctxt_out(t: XML.Tree): Context = t match {

   363     case

   364       XML.Elem(("CONTEXTTHY", Nil), List(

   365         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   366         contthy_xml))

   367       => DataTypes.xml_to_ContextTheory(contthy_xml)

   368     case

   369       XML.Elem(("CONTEXTPBL", Nil), List(

   370         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   371         contpbl_xml))

   372       => DataTypes.xml_to_ContextProblem(contpbl_xml)

   373     case

   374       XML.Elem(("CONTEXTMET", Nil), List(

   375         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   376         contmet_xml))

   377       => DataTypes.xml_to_ContextMethod(contmet_xml)

   378     case _ => throw new IllegalArgumentException("init_ctxt_out wrong arg: " + t)

   379   }

   380 

   381   //fun inputFillFormula: calcID -> string -> XML.tree

   382   //... ONLY IMPL. IN Math_Engine

   383 

   384   //fun interSteps : calcID -> pos' -> XML.tree

   385   def inter_steps_out(t: XML.Tree): IntCEvent = t match {

   386     case

   387       XML.Elem(("INTERSTEPS", Nil), List(

   388         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   389         cevent_xml))

   390       => new IntCEvent(new java.lang.Integer(calcid), 

   391            DataTypes.xml_to_CEvent(cevent_xml))

   392     case _ => throw new IllegalArgumentException("inter_steps_out wrong arg: " + t)

   393   }

   394 

   395   //fun Iterator : calcID -> XML.tree

   396   def iterator_out(t: XML.Tree): IntIntCompound = t match {

   397     case

   398       XML.Elem(("ADDUSER", Nil), List(

   399         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   400         XML.Elem(("USERID", Nil), List(XML.Text(userid)))))

   401       => new IntIntCompound(new java.lang.Integer(calcid), new java.lang.Integer(userid))

   402     case _ => throw new IllegalArgumentException("iterator_out wrong arg: " + t)

   403   }

   404 

   405   //fun IteratorTEST : calcID -> iterID              

   406   //... only relevant for Isabelle/Isac

   407 

   408   //fun modelProblem : calcID -> XML.tree

   409   def modify_calchead_out(t: XML.Tree): IntCalcHead = t match {

   410     case

   411       XML.Elem(("MODIFYCALCHEAD", Nil), List(

   412         XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   413         calchead_xml))

   414       => new IntCalcHead(new java.lang.Integer(calcid), 

   415            DataTypes.xml_to_CalcHead(calchead_xml))

   416     case _ => throw new IllegalArgumentException("modify_calchead_out wrong arg: " + t)

   417   }

   418   

   419   //fun modifyCalcHead : calcID -> icalhd -> XML.tree

   420   def model_pbl_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)  

   421   //fun moveActiveCalcHead : calcID -> XML.tree

   422   def move_active_calchead_out(t: XML.Tree): IntPosition = get_active_form_out(t)    

   423   //fun moveActiveDown : calcID -> XML.tree

   424   def move_active_down_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   425   //fun moveActiveFormula : calcID -> pos' -> XML.tree

   426   def move_active_form_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   427   //fun moveActiveLevelDown : calcID -> XML.tree

   428   def move_active_levdown_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   429   //fun moveActiveLevelUp : calcID -> XML.tree

   430   def move_active_levup_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   431   //fun moveActiveRoot : calcID -> XML.tree

   432   def move_active_root_out(t: XML.Tree): IntPosition = get_active_form_out(t)

   433 

   434 

   435   //fun moveActiveRootTEST : calcID -> XML.tree

   436   //... only relevant for Isabelle/Isac

   437 

   438   //fun moveActiveUp : calcID -> XML.tree

   439   def move_active_up_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   440   //fun moveCalcHead : calcID -> pos' -> XML.tree

   441   def move_calchead_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   442   //fun moveDown : calcID -> pos' -> XML.tree

   443   def move_down_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   444   //fun moveLevelDown : calcID -> pos' -> XML.tree

   445   def move_levdn_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   446   //fun moveLevelUp : calcID -> pos' -> XML.tree

   447   def move_levup_out(t: XML.Tree): IntPosition = get_active_form_out(t)  

   448   //fun moveRoot : calcID -> XML.tree

   449   def move_root_out(t: XML.Tree): IntPosition = get_active_form_out(t)

   450   //fun moveUp : calcID -> pos' -> XML.tree

   451   def move_up_out(t: XML.Tree): IntPosition = get_active_form_out(t)

   452 

   453   //fun refFormula : calcID -> pos' -> XML.tree

   454   def ref_formula_out(t: XML.Tree): IntFormHead = t match {

   455     case

   456       XML.Elem(("REFFORMULA", Nil), List(

   457         XML.Elem(("CALCID", Nil), List(

   458           XML.Text (calcid))), 

   459            XML.Elem(("CALCFORMULA", Nil), cform_etc)))

   460       => new IntFormHead(new java.lang.Integer(calcid), 

   461              DataTypes.xml_to_CalcFormula(XML.Elem(("CALCFORMULA", Nil), cform_etc)))

   462     case

   463       XML.Elem(("REFFORMULA", Nil), List(

   464         XML.Elem(("CALCID", Nil), List(XML.Text (calcid))), 

   465         XML.Elem(("CALCHEAD", status), chead_etc)))

   466       => new IntFormHead(new java.lang.Integer(calcid), 

   467            DataTypes.xml_to_CalcHead(XML.Elem(("CALCHEAD", status), chead_etc)))

   468     case // singularity in error handling

   469       XML.Elem(("REFFORMULA", Nil), List(

   470         XML.Elem(("CALCID", Nil), List(XML.Text (calcid))), 

   471         XML.Elem(("ERROR", Nil), List(XML.Text(msg)))))

   472       => new IntFormHead(new java.lang.Integer(calcid), new Message(msg))

   473     case _ => throw new IllegalArgumentException("ref_formula_out wrong arg: " + t)

   474   }

   475 

   476   //fun refineProblem : calcID -> pos' -> guh -> XML.tree

   477     /* WN150824: isabisac ... isac-java seems to incompatible:

   478      * isabisac/../interface-xml.xml_of_matchpbl is incompatible with

   479      * isac.util.parser.XMLParserDigest //=== Rules for parsing Contexts.

   480      * 

   481      * Unfortunately there is no use-case and no test for refineProblem,

   482      * so the Context only gets the KEStoreKey ("GUH"), 

   483      * not the HierarchyKey.

   484      */

   485   def refine_pbl_out(t: XML.Tree): IntContext = t match {

   486     case

   487       XML.Elem(("CONTEXTPBL", Nil), List(

   488         // WN150530: calcid will be required for asynchronous communication *)

   489         // XML.Elem(("CALCID", Nil), List(XML.Text(calcid))),

   490         XML.Elem(("GUH", Nil), List(XML.Text(guh))),

   491         XML.Elem(("STATUS", Nil), List(XML.Text(status))),

   492         form_xml,

   493         model_xml))

   494       => new IntContext(/*new java.lang.Integer(calcid),*/ 

   495            new Context(null/*see WN150824*/, new KEStoreKey(guh)))

   496     case _ => throw new IllegalArgumentException("refine_pbl_out wrong arg: " + t)

   497   }

   498 

   499   //fun replaceFormula : calcID -> cterm' -> XML.tree

   500   def replace_form_out(t: XML.Tree): IntCEvent = t match {

   501     case

   502       XML.Elem(("REPLACEFORMULA", Nil), List(

   503         XML.Elem(("CALCID", Nil), List(XML.Text (calcid))),

   504         cevent_xml))

   505       => new IntCEvent(new java.lang.Integer(calcid), 

   506            DataTypes.xml_to_CEvent(cevent_xml))

   507     case _ => throw new IllegalArgumentException("replace_form_out wrong arg: " + t)

   508   }

   509 

   510   //fun requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

   511   //...ONLY IMPLEMENTED IN Math_Engine

   512 

   513   //fun resetCalcHead : calcID -> XML.tree

   514   def reset_calchead_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

   515   

   516   //fun setContext : calcID -> pos' -> guh -> XML.tree

   517   def set_ctxt_out(t: XML.Tree): IntCEvent = auto_calc_out(t)

   518 

   519   //fun setMethod : calcID -> metID -> XML.tree

   520   def set_met_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

   521 

   522   //fun setNextTactic : calcID -> tac -> XML.tree

   523   def set_next_tac_out(t: XML.Tree): Message = t match {

   524     case

   525       XML.Elem(("SETNEXTTACTIC", Nil), List(

   526         XML.Elem(("CALCID", Nil), List(XML.Text (_))),

   527         XML.Elem(("MESSAGE", Nil), List(XML.Text (msg))))) 

   528       => new Message(msg) 

   529     case t => throw new IllegalArgumentException("set_next_tac_out wrong arg: " + t)

   530   }

   531 

   532   //fun setProblem : calcID -> pblID -> XML.tree

   533   def set_pbl_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

   534   //fun setTheory : calcID -> thyID -> XML.tree

   535   def set_thy_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)

   536 

   537 }
wneuper/isac