/**

  * Created on Oct 13, 2003

  * @author Richard Gradischnegg RG

  */

 package isac.bridge;

 import isac.bridge.xml.DataTypes;

 import isac.bridge.xml.IntAssumptions;

 import isac.bridge.xml.IntCalcHead;

 import isac.bridge.xml.IntCChanged;

 import isac.bridge.xml.IntCEvent;

 import isac.bridge.xml.IntFormHead;

 import isac.bridge.xml.IntFormulas;

 import isac.bridge.xml.IntIntCompound;

 import isac.bridge.xml.IntContext;

 import isac.bridge.xml.IntPosition;

 import isac.bridge.xml.IntTactic;

 import isac.bridge.xml.IntTacticErrPats;

 import isac.bridge.xml.IntTactics;

 import isac.bridge.xml.IsaToJava;

 import isac.bridge.xml.JavaToIsa;

 import isac.interfaces.ICalcElement;

 import isac.interfaces.ICalcIterator;

 import isac.interfaces.IToCalc;

 import isac.util.Formalization;

 import isac.util.Message;

 import isac.util.ResponseWrapper;

 import isac.util.formulae.Assumptions;

 import isac.util.formulae.CalcHead;

 import isac.util.formulae.Context;

 import isac.util.formulae.ContextMethod;

 import isac.util.formulae.ContextProblem;

 import isac.util.formulae.ContextTheory;

 import isac.util.formulae.HierarchyKey;

 import isac.util.formulae.CalcHeadSimpleID;

 import isac.util.formulae.CalcFormula;

 import isac.util.formulae.FormHeadsContainer;

 import isac.util.formulae.Match;

 import isac.util.formulae.MethodID;

 import isac.util.formulae.Position;

 import isac.util.formulae.ProblemID;

 import isac.util.parser.XMLParserDigest;

 import isac.util.tactics.SimpleTactic;

 import isac.util.tactics.Tactic;

 import isac.util.tactics.TacticsContainer;

 import isac.wsdialog.IContextProvider.ContextType;

 import edu.tum.cs.isabelle.japi.JSystem;

 import edu.tum.cs.isabelle.japi.Operations;

 import isabelle.XML;

 import isabelle.XML.Tree;

 import java.io.BufferedReader;

 import java.io.IOException;

 import java.io.InputStreamReader;

 import java.io.PrintWriter;

 import java.math.BigInteger;

 import java.net.MalformedURLException;

 import java.net.Socket;

 import java.net.UnknownHostException;

 import java.rmi.Naming;

 import java.rmi.RMISecurityManager;

 import java.rmi.RemoteException;

 import java.rmi.registry.LocateRegistry;

 import java.rmi.server.UnicastRemoteObject;

 import java.util.HashMap;

 import java.util.Iterator;

 import java.util.Map;

 import java.util.Set;

 import java.util.Vector;

 import scala.math.BigInt;

 import org.apache.log4j.Logger;

 /**

  * @author Richard Gradischnegg RG

  * 

  * WN0422 here seems to be the key for simplifying the whole bridge.* drawbacks

  * of the present implementation: # more complicated than necessary #

  * JUnitTestCases require BridgeMain running # BridgeLogger cannot be made

  * serializable, thus not accessible for writing by JUnitTestCases #

  */

 public class BridgeRMI extends UnicastRemoteObject implements IBridgeRMI {

     static final long serialVersionUID = -3047706038036289437L;

     private static final Logger logger = Logger.getLogger(BridgeRMI.class.getName());

 	private BridgeMain bridge_;

     private XMLParserDigest xml_parser_digest_;

     // Socket used to communicate with bridge

     private Socket socket_ = null;

     // Writer to write sml requests to the kernel

     private PrintWriter out_ = null;

     // Reader to read sml response from kernel

     private BufferedReader in_ = null;

     private String host_;

     private int rmiid_;

     /**

      * Maps the Java calc(Tree)rmiID to the sml calc(Tree)rmiID. A mapping is

      * nescessary because these ids are not (nescessary) the same: For example

      * when restoring the kernel, the calcTree rmiID can change because of

      * already finished CalcTrees no longer existing and their CalcId assigned

      * to another CalcTree. key: Integer (javaCalcID) value: Integer (smlCalcID)

      */

     private Map java_calcid_to_smlcalcid_;

     /**

      * This map stores user inputs which have already been answered by the

      * kernel and the response being sent back to the user. These inputs are

      * resent to the kernel in the case of a newstart of the kernel. key:

      * Integer (javaCalcID) value: Vector (containing input strings)

      */

     private Map inputs_;

 	private JSystem connection_to_kernel_;

     public BridgeRMI(BridgeMain bridge, String host, int port, String dtdPath)

             throws RemoteException {

         if (logger.isDebugEnabled())

             logger.debug("BridgeRMI obj.init: bridge=" + bridge + ", host=" + host

                 + ", port=" + port + ", dtdPath=" + dtdPath);

         this.host_ = host;

         this.bridge_ = bridge;

         this.connection_to_kernel_ = bridge.getConnectionToKernel();

         /*

          * out = bridge.getSmlWriter(); in = bridge.getSmlReader();

          */

         in_ = bridge.getSmlReader();

         try {

             socket_ = new Socket(host, port);

             out_ = new PrintWriter(socket_.getOutputStream(), true);

             in_ = new BufferedReader(new InputStreamReader(socket_

                     .getInputStream()));

         } catch (UnknownHostException e) {

             System.out.println("Unknown host: " + host + "\n");

         } catch (IOException e) {

             System.out.println("No I/O\n");

         }

         rmiBind();

         xml_parser_digest_ = new XMLParserDigest(dtdPath);

         //xml_parser_digest_.setValidating(true);

         //...all XML-data should be tested in

         //javatest.isac.util.parser.TestXMLParserDigest

         inputs_ = new HashMap();

         java_calcid_to_smlcalcid_ = new HashMap();

     }

     /**

      * Buffers input sent to the sml-Kernel (for later possible restart)

      * 

      * @param javaCalcID

      *            calcTree this input belongs to

      * @param input

      *            to be buffered

      */

     public void bufferInput(int javaCalcID, String input) {

         Vector v = (Vector) inputs_.get(new Integer(javaCalcID));

         if (v == null) {

             v = new Vector();

             inputs_.put(new Integer(javaCalcID), v);

         }

         v.add(input);

     }

     // '@calcid@' is a placeholder for the CalcID

     // this method replaces it with a real CalcID

     private String insertCalcID(int id, String s) {

         return s.replaceAll("@calcid@", String.valueOf(id));

     }

     // return smallest integer which is not yet

     // used as a (java)CalcID

     private int smallestFreeCalcID() {

         Set set = java_calcid_to_smlcalcid_.keySet();

         for (int i = 0; i < set.size(); i++) {

             if (!set.contains(new Integer(i))) {

                 return i;

             }

         }

         return set.size();

     }

     /*

      * Send a sml instruction to the kernel. restore == true, if the instruction

      * is resent after the kernel crashed

      */

     private ResponseWrapper sendToKernel(String smlInstr, boolean restore) {

         if (logger.isDebugEnabled())

             logger.debug("   BR->KN: sendToKernel(" + smlInstr + ")");

         ResponseWrapper wrapper = null;

         //bridge.log(1,"---sendToKernel |

         //bridge.isRestoring=="+bridge.isRestoring());

         //bridge.log(1,"---sendToKernel | restoring=="+restore);

         if (!bridge_.isRestoring() || restore) {

             String xmlString = "";

             out_.println(smlInstr);// send the sml Instruction to the sml Kernel

             try {

                 xmlString = in_.readLine();//read the response from the kernel

                 if (logger.isInfoEnabled())

                     logger.info("   BR<-KN: sendToKernel <- xml= " + xmlString);

             } catch (IOException e) {

                 bridge_.log(1, "BridgeRMI.interpretSKN: IOException");

                 e.printStackTrace();

             }

             //if (!(restore) && bridge.isRestoring()) {

             //	this.restoreExistingCalcTrees();

             //}

             bridge_.log( 1, xmlString );

             wrapper = xml_parser_digest_.parse(xmlString);

         }

         return wrapper;

     }

     /**

      * Send an instruction to the SML-Kernel and return the response

      * 

      * @param smlInstr

      *            Instruction

      * @return response from SML-Kernel

      */

     private synchronized ResponseWrapper interpretSML(int javaCalcID,

             String instr, boolean restore) {

         int smlCalcID;

         Integer smlCalcInteger = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

         if( smlCalcInteger == null ) {

         	bridge_.log(1, "smlCalcInteger is null for javaCalcID : " + javaCalcID );

         	return null;

         }

         smlCalcID = smlCalcInteger.intValue();

         String smlInstr = insertCalcID(smlCalcID, instr);

         bridge_.log(1, "JavaCalcID " + javaCalcID + " == SmlCalcID "

                 + smlCalcID);

         bridge_.log(1, "sent to bridge: " + smlInstr);

         ResponseWrapper wrapper = this.sendToKernel(smlInstr, restore); 

         if (!restore)

             bufferInput(javaCalcID, smlInstr);

         return wrapper;

     }

     private void rmiBind() {

         if (logger.isDebugEnabled())

             logger.debug("rmiBind");

         if (System.getSecurityManager() == null) {

             System.setSecurityManager(new RMISecurityManager());

         }

         String name = "//" + host_ + "/BridgeRMI";

         try {

             System.out.println("try to bind as " + name);

             Naming.rebind(name, this);

             System.out.println("Bridge RMI bound to " + name);

         } catch (java.rmi.ConnectException e) {

             System.err.println("failed to contact as " + name + " (creating RMI-Server on localhost: 1099)");

             try {

                 LocateRegistry.createRegistry(1099);

             } catch (java.rmi.RemoteException exc2) {

                 System.err.println("can not create registry: " + exc2.getMessage());

                 System.exit(1);

             }

             rmiBind();

         } catch (RemoteException e) {

         	System.err.println("RemoteException");

         	System.err.println(e.getMessage());

         	System.err.println(e.getCause().getMessage());

         	System.err.println(e.getCause().getClass());

         	e.printStackTrace();

         	System.exit(1);

         } catch (MalformedURLException e) {

         	System.err.println(e.getMessage());

         	e.printStackTrace();

         	System.exit(1);

         } catch (Exception e) {

         	System.err.println("----------- Exception");

         	System.err.println(e.getClass().getName());

         	System.err.println(e.getMessage());

         	e.printStackTrace();

         	System.exit(1);

         }

     }

     /**

      * Restore a saved calcTree.

      * 

      * @param v

      *            Vector containing strings

      * @return Java CalcTreeID (not SML-ID)

      */

     public int loadCalcTree(Vector v) {

         this.bridge_.log(1, "----------------begin loading------------");

         int javaCalcID = smallestFreeCalcID();

         this.bridge_.log(1, "-----smallest free  = " + javaCalcID);

         restoreToSML(javaCalcID, v);

         this.bridge_.log(1, "----------------done loading-------------");

         return javaCalcID;

     }

     public int smlCalcIDtoJavaCalcID(int smlID) {

         Iterator it = java_calcid_to_smlcalcid_.keySet().iterator();

         while (it.hasNext()) {

             Object key = it.next();

             Integer value = (Integer) java_calcid_to_smlcalcid_.get(key);

             if (value.intValue() == smlID) {

                 return ((Integer) key).intValue();

             }

         }

         return -1;

     }

     public Map getInputs() {

         return inputs_;

     }

     public int getRmiID() {

         return rmiid_;

     }

     public void setRmiID(int i) {

         if (logger.isDebugEnabled())

             logger.debug("setRmiID: i=" + i);

         rmiid_ = i;

     }

     /**

      * causes a CalcChanged event for the first line on the Worksheet

      * 

      * @param id

      *            for the CalcTree (unused)

      * @return CalcChanged with Iterators pointing at the root of the CalcTree

      */

     public CChanged startCalculate(int id) {

         Position p = new Position();

         p.setKind("Pbl");// toSMLString --> ([],"Pbl")

         CChanged cc = new CChanged();

         cc.setLastUnchanged(p);

         cc.setLastDeleted(p);

         cc.setLastGenerated(p);

         return cc;

     }

     /**

      * Starts the specifying phase: fill the calcTree with the appropriate

      * information. Once the calc_head_ is fully specified, the user can begin

      * with the actual calculation.

      * 

      * @param f

      *            Formalization for this calculation (empty if user starts a

      *            complete new calculation)

      * @return javaCalcID

      */

     public int getCalcTree(Formalization formalization) {

     	int return_val;

     	int javaCalcID = smallestFreeCalcID();

     	this.bridge_.log(1, "-----smallest free javaCalcID = " + javaCalcID);

     	int smlCalcID = newCalculation(javaCalcID, 

     	  "CalcTree " + formalization.toSMLString() + ";", formalization, false);

     	return_val = javaCalcID;

         return return_val;

     }

     /***********************************************************************

      * Below are all the methods in structure Math_Engine : MATH_ENGINE

      * listed in the same order as in the signature.

      * The previous order still reflected original development;

      * method names reflect the original struggle at the 

      * interface Java <--> Isabelle/Isac: different names are made explicit.

      */

     /** MATH_ENGINE: val appendFormula : calcID -> cterm' -> XML.tree */

     public CEvent appendFormula(int id, CalcFormula f) {

     	CEvent return_val = null;

     	int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

         /*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/wrapper = interpretSML(id, "appendFormula @calcid@ \"" + f.toSMLString() + "\";", false);

     	//*TTY*/if (wrapper == null) return null;

     	//*TTY*/return_val = (CEvent) wrapper.getResponse();

         /*---------------------------------------------------------------------------*/

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "appendFormula " + sml_id + " \"" + f.toSMLString() + "\";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.append_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), f.getFormula());    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);    	

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.APPEND_FORM, xml_in);

     	/*PIDE*/IntCEvent java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) java_out = IsaToJava.append_form_out(xml_out);

     	/*PIDE*/// else: no message handling by DialogGuide

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);

     	/*PIDE*/return_val = java_out.getCEvent();

         /*---------------------------------------------------------------------------*/

         return return_val;   

     }

     /** MATH_ENGINE: val autoCalculate : calcID -> auto -> XML.tree */

     public CEvent autoCalculate(int id, int scope, int steps) {

         if (logger.isDebugEnabled())

             logger.debug("BridgeRMI#autoCalculate: id=" + id + ", scope" + scope + ", steps" + steps);

         ResponseWrapper wrapper = null;

     	CEvent return_val = null;

     	int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	String log_str;

         /*---------------------------------------------------------------------------*/

     	//*TTY*/if ((scope == 3) && (steps == 0)) { //scope ==3 means IToCalc.SCOPE_CALCHEAD:

     	//*TTY*/    wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteCalcHead;", false);

     	//*TTY*/} else if ((scope == IToCalc.SCOPE_CALCULATION) && (steps == 0)) {

     	//*TTY*/    wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteCalc;", false);

         //*TTY*/} else if ((scope == IToCalc.SCOPE_MODEL) && (steps == 0)) {

         //*TTY*/    wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteModel;", false);

         //*TTY*/} else if ((scope == IToCalc.SCOPE_SUBCALCULATION) && (steps == 0)) {

         //*TTY*/    wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteToSubpbl;", false);

         //*TTY*/} else if ((scope == IToCalc.SCOPE_SUBPROBLEM) && (steps == 0)) {

         //*TTY*/    wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteSubpbl;", false);

         //*TTY*/} else { //FIXXXME040624: steps do not regard the scope

         //*TTY*/    wrapper = interpretSML(id, "autoCalculate @calcid@ (Step " + steps + ");", false);

         //*TTY*/}

         //*TTY*/if (wrapper == null) return_val =  null;

         //*TTY*/return_val = (CEvent) wrapper.getResponse();

         //-----------------------------------------------------------------------------

     	/*PIDE*/String scope_str;

     	/*PIDE*/if ((scope == 3) && (steps == 0)) { //scope ==3 means IToCalc.SCOPE_CALCHEAD:

     	/*PIDE*/	scope_str = "CompleteCalcHead"; //FIXXXME.WN040624 steps == 0 hides mismatch in specifications

     	/*PIDE*/} else if ((scope == IToCalc.SCOPE_CALCULATION) && (steps == 0)) {

     	/*PIDE*/	scope_str = "CompleteCalc";

     	/*PIDE*/} else if ((scope == IToCalc.SCOPE_MODEL) && (steps == 0)) {

     	/*PIDE*/	scope_str = "CompleteModel";

     	/*PIDE*/} else if ((scope == IToCalc.SCOPE_SUBCALCULATION) && (steps == 0)) {

     	/*PIDE*/	scope_str = "CompleteToSubpbl";

     	/*PIDE*/} else if ((scope == IToCalc.SCOPE_SUBPROBLEM) && (steps == 0)) {

     	/*PIDE*/	scope_str = "CompleteSubpbl";

     	/*PIDE*/} else { //FIXXXME040624: steps do not regard the scope

     	/*PIDE*/	scope_str = "Step"; // steps > 0 according to impl.in "isabelle tty"

     	/*PIDE*/}

     	/*PIDE*/if (steps == 0) log_str = scope_str; else log_str = "(Step " + steps + ")";

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "autoCalculate " + sml_id + " " + log_str + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  scope_str, new scala.math.BigInt(BigInteger.valueOf(steps)));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.AUTO_CALC, xml_in);

     	/*PIDE*/IntCEvent java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.auto_calc_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCEvent();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

         /*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val applyTactic : calcID -> pos' -> tac -> XML.tree 

      * not implemented in Math_Engine.

      * compare setNextTactic. */

     /**

      * Starts a new calculation in the sml-Kernel: i.e. a new CalcTree with the

      * initial hot_spot_

      * 

      * @param instr

      *            "CalcTree" + Formalization in string Representation

      * @param fmz 

      * @return sml_calcid //WN150817 why return SML(?!) calcid to Java(?!)

      * 

      * MATH_ENGINE: val CalcTree : fmz list -> XML.tree

      */

     private synchronized int newCalculation(int javaCalcID, String instr,

             Formalization fmz, boolean restore) {

         if (logger.isDebugEnabled())

             logger.debug("newCalculation: javaCalcID=" + javaCalcID + ", instr" + instr + ", restore=" + restore);

         int sml_calcid;

         int return_val;

         /*---------------------------------------------------------------------------*/

         //*TTY*/bridge_.log(1, "new calculation: " + instr);

         //*TTY*/ResponseWrapper wrapper = sendToKernel(instr, restore);

         //*TTY*/if (wrapper == null) return -1;

         //*TTY*/sml_calcid = wrapper.getCalcID();

         //*TTY*/sendToKernel("Iterator " + sml_calcid + ";", restore);//WN041209 no

         //*TTY*/sendToKernel("moveActiveRoot " + sml_calcid + ";", restore);//WN041209

         //*TTY*/if (!restore) bufferInput(javaCalcID, instr);

         /*---------------------------------------------------------------------------*/

         /*PIDE*/bridge_.log(1, "-->ISA: " + instr);

         /*PIDE*/XML.Tree CALC_TREE_out = connection_to_kernel_.invoke(Operations.CALC_TREE,

         /*PIDE*/  DataTypes.xml_of_Formalization(fmz));

         /*PIDE*/bridge_.log(1, "<--ISA: " + CALC_TREE_out);

         /*PIDE*/sml_calcid = (IsaToJava.calc_tree_out(CALC_TREE_out)).intValue();

         /*PIDE*/bridge_.log(1, "-->ISA: " + "Iterator " + sml_calcid + ";");

         /*PIDE*/XML.Tree ITERATOR_out = connection_to_kernel_.invoke(Operations.ITERATOR,

         /*PIDE*/  new scala.math.BigInt(BigInteger.valueOf(sml_calcid)));

         /*PIDE*/IntIntCompound int_int = IsaToJava.iterator_out(ITERATOR_out);

         /*PIDE*/sml_calcid = int_int.getCalcId().intValue();

         /*PIDE*/int userid = int_int.getUserId().intValue(); //WN150808 ununsed

         /*PIDE*/bridge_.log(1, "<--ISA: " + ITERATOR_out);

         /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveRoot " + sml_calcid + ";");

         /*PIDE*/XML.Tree MOVE_ACTIVE_ROOT_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_ROOT,

         /*PIDE*/  new scala.math.BigInt(BigInteger.valueOf(sml_calcid)));

         /*PIDE*/IntPosition calcid_pos = IsaToJava.move_active_root_out(MOVE_ACTIVE_ROOT_out);

         /*PIDE*/return_val = calcid_pos.getCalcId();

         /*PIDE*/Position pos = calcid_pos.getPosition(); //WN150808 unused

         /*PIDE*/bridge_.log(1, "<--ISA: " + MOVE_ACTIVE_ROOT_out);

         /*---------------------------------------------------------------------------*/

         java_calcid_to_smlcalcid_.put(new Integer(javaCalcID), new Integer(sml_calcid));

         return_val = sml_calcid; //WN150808 SML_caldid --> JAVA frontend ?!?

         return return_val;

     }

     /** MATH_ENGINE: val checkContext : calcID -> pos' -> guh -> XML.tree */

     public Context checkContext(int javaCalcID, Context context, Position pos) throws RemoteException {

     	Context return_val = null;

         /*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/  "checkContext @calcid@ " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";", false);

     	//*TTY*/if(wrapper == null) return null;

     	//*TTY*/return_val = (Context) wrapper.getResponse();

         /*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "checkContext " + sml_id + " " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.check_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  pos, context.getKEStoreKey().toString() + "\"");

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);    	

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.CHECK_CTXT, xml_in);

     	/*PIDE*/ContextTheory java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.check_ctxt_out(xml_out);

     	/*PIDE*/  return_val = java_out;

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

         /*---------------------------------------------------------------------------*/

         return return_val;

     }    

     /** MATH_ENGINE: val DEconstrCalcTree : calcID -> XML.tree */

     public boolean destruct(int javaCalcID) {

     	boolean return_val;

         /*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/  "DEconstrCalcTree @calcid@;", false);

     	//*TTY*/if (wrapper == null) { return_val = false; }

     	//*TTY*/inputs_.remove(new Integer(javaCalcID));

     	//*TTY*/return_val = true;

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "DEconstrCalcTree " + sml_id);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.DEL_CALC,

     	/*PIDE*/  new scala.math.BigInt(BigInteger.valueOf(sml_id)));

     	/*PIDE*/Integer java_out = IsaToJava.del_calc_out(xml_out);

     	/*PIDE*/return_val = true;

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*---------------------------------------------------------------------------*/

     	java_calcid_to_smlcalcid_.remove(new Integer(javaCalcID));

     	return return_val;

     }

     /** MATH_ENGINE: val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree */

     public Vector<Tactic> getAppliableTactics(int id, int scope, Position pos) {

     	Vector<Tactic> return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(id,

     	//*TTY*/  "fetchApplicableTactics @calcid@ " + scope + pos.toSMLString() + ";", false);

     	//*TTY*/if (wrapper == null) return null;

     	//*TTY*/TacticsContainer tc = (TacticsContainer) wrapper.getResponse();

     	//*TTY*/if( tc == null ) return null;

     	//*TTY*/return_val = tc.getTactics();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "fetchApplicableTactics " + sml_id + " " + scope + pos.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.fetch_applicable_tacs(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  new scala.math.BigInt(BigInteger.valueOf(scope)), pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.FETCH_APPL_TACS, xml_in);

     	/*PIDE*/IntTactics java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.fetch_applicable_tacs_out(xml_out);

     	/*PIDE*/  return_val = java_out.getTactics();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

        return return_val;

     }

     /** MATH_ENGINE: val fetchProposedTactic : calcID -> XML.tree */

     public Tactic fetchProposedTactic(int id) {

     	Tactic return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(id, "fetchProposedTactic @calcid@;", false);

         //*TTY*/if (wrapper == null) { return null; }

         //*TTY*/return_val = (Tactic) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "fetchProposedTactic " + sml_id + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.fetch_proposed_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.FETCH_PROP_TAC, xml_in);

     	/*PIDE*/IntTacticErrPats java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.fetch_proposed_tac_out(xml_out);

     	/*PIDE*/  return_val = java_out.getTactic();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val findFillpatterns : calcID -> errpatID -> XML.tree 

      * only implemented in Math_Engine */

     /**

      * @see isac.bridge.IBridgeRMI#getAccumulatedAssumptions(int,

      *      isac.util.formulae.Position)

      *      

      * ** MATH_ENGINE: val getAccumulatedAsms : calcID -> pos' -> XML.tree

      */

     public Assumptions getAccumulatedAssumptions(int calcTreeID, Position pos) throws RemoteException {

     	Assumptions return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,

     	//*TTY*/  "getAccumulatedAsms @calcid@ " + pos.toSMLString() + ";", false);

     	//*TTY*/return_val = (Assumptions) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "getAccumulatedAsms " + sml_id + " " + pos.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.get_accumulated_asms(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.GET_ACC_ASMS, xml_in);

     	/*PIDE*/IntAssumptions java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.get_accumulated_asms_out(xml_out);

     	/*PIDE*/  return_val = java_out.getAssumptions();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val getActiveFormula : calcID -> XML.tree */

     public Position getActiveFormula(int javaCalcID) {

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/  "getActiveFormula @calcid@ ;", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "getActiveFormula " + sml_id + " ;");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.GET_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.get_active_form_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.bridge.IBridgeRMI#getAssumption(int, int)

      * 

      * MATH_ENGINE: val getAssumptions : calcID -> pos' -> XML.tree

      */

     public Assumptions getAssumptions(int calcTreeID, Position pos) throws RemoteException {

     	Assumptions return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,

     	//*TTY*/  "getAssumptions @calcid@ " + pos.toSMLString() + ";", false);

     	//*TTY*/return_val = (Assumptions) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "getAssumptions " + sml_id + " " + pos.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.get_asms(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.GET_ASMS, xml_in);

     	/*PIDE*/IntAssumptions java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.get_asms_out(xml_out);

     	/*PIDE*/  return_val = java_out.getAssumptions();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree */

     public Vector getFormulaeFromTo(int id, ICalcIterator iterator_from,

             ICalcIterator iterator_to, Integer level, boolean result_includes_tactics) {

         XML.Tree xml_in = null;

     	ResponseWrapper wrapper = null;

         Vector return_val = null;      

     	/*---------------------------------------------------------------------------*/

         //*TTY*/try { wrapper = interpretSML(id, "getFormulaeFromTo @calcid@ "

         //*TTY*/    + iterator_from.toSMLString() + " " + iterator_to.toSMLString()

         //*TTY*/    + " " + level + " " + result_includes_tactics + ";", false);

         //*TTY*/} catch (RemoteException e) { e.printStackTrace(); }

         //*TTY*/if (wrapper == null) return null;

         //*TTY*/FormHeadsContainer con = (FormHeadsContainer) wrapper.getResponse();

         //*TTY*/if (con != null) return_val = con.getElements();

         //*TTY*/else return_val = null;

     	/*---------------------------------------------------------------------------*/

         /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

         /*PIDE*/try {

         /*PIDE*/  bridge_.log(1, "-->ISA: " + "getFormulaeFromTo " + sml_id + " "

         /*PIDE*/    + iterator_from.toSMLString() + " " + iterator_to.toSMLString()

 		/*PIDE*/    + " " + level + " " + result_includes_tactics + ";");

 		/*PIDE*/} catch (RemoteException e2) { e2.printStackTrace(); }

         /*PIDE*/try {

         /*PIDE*/  xml_in = JavaToIsa.get_formulae(new scala.math.BigInt(BigInteger.valueOf(sml_id)),

 		/*PIDE*/    iterator_from.getPosition(), iterator_to.getPosition(), 

 		/*PIDE*/    new scala.math.BigInt(BigInteger.valueOf(level)), result_includes_tactics);

         /*PIDE*/} catch (RemoteException e1) { e1.printStackTrace(); }

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.GET_FORMULAE, xml_in);

     	/*PIDE*/IntFormulas java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.get_formulae_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcFormulas();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

         /*---------------------------------------------------------------------------*/

         return return_val;

     }

     /*

      * @see isac.bridge.IBridgeRMI#getTactic(int, int)

      * 

      * MATH_ENGINE: val getTactic : calcID -> pos' -> XML.tree

      */

     public Tactic getTactic(int calcTreeID, Position pos) throws RemoteException {

     	Tactic return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,

     	//*TTY*/  "getTactic @calcid@ " + pos.toSMLString() + ";", false);

     	//*TTY*/return_val = (Tactic) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "getTactic " + sml_id + " " + pos.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.get_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.GET_TAC, xml_in);

     	/*PIDE*/IntTactic java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.get_tac_out(xml_out);

     	/*PIDE*/  return_val = java_out.getTactic();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val initContext : calcID -> ketype -> pos' -> XML.tree 

      *

      * This method is implemented in Isabelle/Isac, but seems to never have been completed in Java.

      * See isac.bridge.TestContext#testContext.

      */

     public Context initContext(int javaCalcID, ContextType type, Position pos) throws RemoteException {

     	Context return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/  "initContext @calcid@ " + type.toSMLString() + " " + pos.toSMLString() + ";", false);

     	//*TTY*/if(wrapper == null) return null;

     	//*TTY*/return_val = (Context) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "initContext " + sml_id + " " + type.toSMLString() + " " + pos.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.init_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)), type, pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.INIT_CTXT, xml_in);

     	/*PIDE*/Context java_out = null; // front-end later distinguishes ContextTheory, ContextProblem, ..

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = (Context) IsaToJava.init_ctxt_out(xml_out);

     	/*PIDE*/  return_val = java_out;

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val inputFillFormula: calcID -> string -> XML.tree 

      * only implemented in Math_Engine */

     /** MATH_ENGINE: val interSteps : calcID -> pos' -> XML.tree */

     public CEvent intermediateSteps(int id, ICalcIterator ci) {

     	CEvent return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

         //*TTY*/try {

         //*TTY*/    wrapper = interpretSML(id, "interSteps @calcid@ " + ci.toSMLString() + ";", false);

         //*TTY*/} catch (RemoteException e) { e.printStackTrace(); }

         //*TTY*/if (wrapper == null) return null;

         //*TTY*/return_val = (CEvent) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	/*PIDE*/XML.Tree xml_in = null;

     	/*PIDE*/try {

     	/*PIDE*/	bridge_.log(1, "-->ISA: " + "interSteps " + sml_id + " " + ci.toSMLString() + ";");

     	/*PIDE*/} catch (RemoteException e1) { e1.printStackTrace(); }

     	/*PIDE*/try {

     	/*PIDE*/  xml_in = JavaToIsa.inter_steps(new scala.math.BigInt(BigInteger.valueOf(sml_id)), ci.getPosition());

     	/*PIDE*/} catch (Exception e1) { e1.printStackTrace();}    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.INTER_STEPS, xml_in);

     	/*PIDE*/IntCEvent java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.inter_steps_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCEvent();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val Iterator : calcID -> XML.tree */

     public int iterator(int id) {

         if (logger.isDebugEnabled())

           logger.debug("iterator: id=" + id);

         int return_val = 4711;

     	/*---------------------------------------------------------------------------*/

         //*TTY*/if (id == 1) {

         //*TTY*/    ResponseWrapper wrapper = interpretSML(id, "Iterator @calcid@;", false);

         //*TTY*/    if (wrapper == null) return_val = -1;

         //*TTY*/    else return_val = Integer.parseInt(((CalcHeadSimpleID) wrapper .getResponse()).getID());

         //*TTY*/} else return_val = 4711;//TODO.WN041208 drop CalcIterator.iteratorID_

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "Iterator " + sml_id + ";");

     	/*PIDE*/BigInt xml_in = new scala.math.BigInt(BigInteger.valueOf(sml_id));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.ITERATOR, xml_in);

     	/*PIDE*/IntIntCompound java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.iterator_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcId().intValue();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.interfaces.IToCalc#modelProblem()

      * 

      * MATH_ENGINE: val modelProblem : calcID -> XML.tree

      */

     public CalcHead modelProblem(int calc_tree_id) throws RemoteException {

     	CalcHead return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id, "modelProblem @calcid@;", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "modelProblem " + sml_id + ";");

     	/*PIDE*/BigInt xml_in = new scala.math.BigInt(BigInteger.valueOf(sml_id));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.MODEL_PBL, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.modify_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.interfaces.IToCalc#checkCalcHead(isac.util.formulae.CalcHead)

      * 

      * MATH_ENGINE: val modifyCalcHead : calcID -> icalhd -> XML.tree

      */

     public CalcHead checkCalcHead(int calc_tree_id, CalcHead calchead) throws RemoteException {

     	CalcHead return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "modifyCalcHead @calcid@ " + calchead.toSMLString() + ";", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "modelProblem " + sml_id + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.modify_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)), calchead);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.MODIFY_CALCHEAD, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.modify_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val moveActiveCalcHead : calcID -> XML.tree */

     public Position moveCalcHead(int javaCalcID, int iteratorID, Position p) {

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/if (iteratorID == 1)

     	//*TTY*/  wrapper = interpretSML(javaCalcID, "moveActiveCalcHead @calcid@" + ";", false);

     	//*TTY*/else

     	//*TTY*/  wrapper = interpretSML(javaCalcID, "moveCalcHead @calcid@ " + " " + p.toSMLString() + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/XML.Tree xml_in = null;

     	/*PIDE*/XML.Tree xml_out = null;

     	/*PIDE*/if (iteratorID == 1) {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveCalcHead " + sml_id + "" + ";");    	

     	/*PIDE*/xml_in = JavaToIsa.move_active_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/} else {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveCalcHead " + sml_id + " " + " " + p.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)), null);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val moveActiveDown : calcID -> XML.tree */

     public Position moveDown(int javaCalcID, int iteratorID, Position p) {

         if (logger.isDebugEnabled())

             logger.debug("moveDown: javaCalcID=" + javaCalcID + ", sml_pos=" + p.toSMLString());

         Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/if (iteratorID == 1)

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveActiveDown @calcid@" + ";", false);

     	//*TTY*/else

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveDown @calcid@ " + p.toSMLString() + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/XML.Tree xml_in = null;

     	/*PIDE*/XML.Tree xml_out = null;

     	/*PIDE*/if (iteratorID == 1) {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveDown " + sml_id + "" + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_active_down(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_DOWN, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_down_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/} else {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveDown " + sml_id + " " + p.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_down(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_DOWN, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_down_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** 

      * returns Position for uniformity with move*; not required elsewhere

      * 

      * MATH_ENGINE: val moveActiveFormula : calcID -> pos' -> XML.tree 

      */

     public Position moveActiveFormula(int javaCalcID, Position p) {

         if (logger.isDebugEnabled())

             logger.debug("moveDown: javaCalcID=" + javaCalcID + ", sml_pos=" + p.toSMLString());

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/  "moveActiveFormula @calcid@ " + p.toSMLString() + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveFormula " + sml_id + " " + p.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.move_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_form_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val moveActiveLevelDown : calcID -> XML.tree */

     public Position moveLevelDown(int javaCalcID, int iteratorID, Position p) {

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/if (iteratorID == 1)

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveActiveLevelDown @calcid@" + ";", false);

     	//*TTY*/else

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveLevelDown @calcid@ " + " " + p.toSMLString() + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/XML.Tree xml_in = null;

     	/*PIDE*/XML.Tree xml_out = null;

     	/*PIDE*/if (iteratorID == 1) {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveLevelDown " + sml_id + "" + ";");    	

     	/*PIDE*/xml_in = JavaToIsa.move_active_levdown(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_LEVDN, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_levdown_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/} else {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveLevelDown " + sml_id + " " + " " + p.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_levdn(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_LEVDN, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_levdn_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val moveActiveLevelUp : calcID -> XML.tree */

     public Position moveLevelUp(int javaCalcID, int iteratorID, Position p) {

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/if (iteratorID == 1)

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveActiveLevelUp @calcid@" + ";", false);

     	//*TTY*/else

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveLevelUp @calcid@ " + p.toSMLString() + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/XML.Tree xml_in = null;

     	/*PIDE*/XML.Tree xml_out = null;

     	/*PIDE*/if (iteratorID == 1) {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveLevelUp " + sml_id + "" + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_active_levup(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_LEVUP, xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_levup_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/} else {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveLevelUp " + sml_id + " " + p.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_levup(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_LEVUP, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_levup_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val moveActiveRoot : calcID -> XML.tree */

     public Position moveRoot(int javaCalcID, int iteratorID) {

         if (logger.isDebugEnabled())

             logger.debug("moveRoot: javaCalcID=" + javaCalcID);

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/if (iteratorID == 1)

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveActiveRoot @calcid@" + ";", false);

     	//*TTY*/else

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveRoot @calcid@ " + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/scala.math.BigInt xml_in = null;

     	/*PIDE*/XML.Tree xml_out = null;

     	/*PIDE*/if (iteratorID == 1) {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveRoot " + sml_id + "" + ";");

     	/*PIDE*/xml_in = new scala.math.BigInt(BigInteger.valueOf(sml_id));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_ROOT, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_root_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/} else {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveRoot " + sml_id + " " + ";");

     	/*PIDE*/XML.Tree xml_in2 = JavaToIsa.move_root(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in2);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ROOT, xml_in2);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_root_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val moveActiveRootTEST : calcID -> XML.tree 

      *  used only internally in Math_Engine */

     /** MATH_ENGINE: val moveActiveUp : calcID -> XML.tree */

     public Position moveUp(int javaCalcID, int iteratorID, Position p) {

     	Position return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/if (iteratorID == 1)

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveActiveUp @calcid@" + ";", false);

     	//*TTY*/else

     	//*TTY*/    wrapper = interpretSML(javaCalcID, "moveUp @calcid@ " + p.toSMLString() + ";", false);

     	//*TTY*/return_val = moveSuccess(wrapper);

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/XML.Tree xml_in = null;

     	/*PIDE*/XML.Tree xml_out = null;

     	/*PIDE*/if (iteratorID == 1) {

     	/*PIDE*/xml_in = JavaToIsa.move_active_up(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_UP, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_active_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/} else {

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "moveUp " + sml_id + " " + p.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.move_up(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.MOVE_UP, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.move_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     // /----- these methods are designed for a visitor of the CalcTree ------------\

     //        (with a iteratorID > 1), e.g. a teacher watching the student.

     /** MATH_ENGINE: val moveCalcHead : calcID -> pos' -> XML.tree 

      *  does not exist in isac-java, see val moveActiveCalcHead */

     /** MATH_ENGINE: val moveDown : calcID -> pos' -> XML.tree 

      *  does not exist in isac-java, see val moveActiveDown */

     /** MATH_ENGINE: val val moveLevelDown : calcID -> pos' -> XML.tree 

      *  does not exist in isac-java, see val moveActiveLevelDown */

     /** MATH_ENGINE: val moveLevelUp : calcID -> pos' -> XML.tree 

      *  does not exist in isac-java, see val moveActiveLevelUp */

     /** MATH_ENGINE: val moveRoot : calcID -> XML.tree

      *  does not exist in isac-java, see val moveActiveRoot */

     /** MATH_ENGINE: val moveUp : calcID -> pos' -> XML.tree

      *  does not exist in isac-java, see val moveActiveUp */

     // \----- these methods are designed for a visitor of the CalcTree ------------/

     /**

      * @see isac.bridge.IBridgeRMI#getElement(int, int)

      * MATH_ENGINE: val refFormula : calcID -> pos' -> XML.tree

      */

     public ICalcElement getElement(int javaCalcID, Position p) {

     	ICalcElement return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/        "(*getElement*)refFormula @calcid@ " + p.toSMLString() + ";", false);

     	//*TTY*/if (wrapper == null) return_val =  null;

     	//*TTY*/return_val =  (ICalcElement) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_calcid = ((Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID))).intValue();

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*getElement*)refFormula " + sml_calcid

     	/*PIDE*/  + " " + p.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_calcid)), p);

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.REF_FORMULA, xml_in);

     	/*PIDE*/IntFormHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.ref_formula_out(xml_out);

     	/*PIDE*/  return_val = (ICalcElement)java_out.getFormHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

     	return return_val;

     }

     /**

      * @see isac.bridge.IBridgeRMI#getFormula(int, int)

      * @deprecated in favour of getElement.

      * ... WN150812: never used although it is in IBridgeRMI !!

      * 

      * MATH_ENGINE: val refFormula : calcID -> pos' -> XML.tree

      */

     public ICalcElement getFormula(int calcTreeID, Position p) throws RemoteException {

     	ICalcElement return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,

     	//*TTY*/  "(*getFormula*)refFormula @calcid@ " + p.toSMLString() + ";", false);

     	//*TTY*/if (wrapper == null) return_val = null;

     	//*TTY*/else return_val = (ICalcElement) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*getFormula*)refFormula " + sml_id + " " + p.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.REF_FORMULA, xml_in);

     	/*PIDE*/IntFormHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.ref_formula_out(xml_out);

     	/*PIDE*/  return_val = (ICalcElement)java_out.getFormHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val refineProblem : calcID -> pos' -> guh -> XML.tree 

      *  see notes WN150824 */

     public Context refineProblem(int javaCalcID, Context context, Position pos) throws RemoteException {

     	Context return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,

     	//*TTY*/  "refineProblem @calcid@ " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";", false); 

     	//*TTY*/if(wrapper == null) return null;

     	//*TTY*/return_val = (Context) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "refineProblem " + sml_id + " " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.refine_pbl(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  pos, context.getKEStoreKey().toString() + "\"");

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.REFINE_PBL, xml_in);

     	/*PIDE*/IntContext java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.refine_pbl_out(xml_out);

     	/*PIDE*/  return_val = java_out.getContext();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val replaceFormula : calcID -> cterm' -> XML.tree */

     public CEvent replaceFormula(int id, CalcFormula f) {

     	CEvent return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = null;

     	//*TTY*/wrapper = interpretSML(id, "replaceFormula @calcid@ \"" + f.toSMLString() + "\";", false);

     	//*TTY*/if (wrapper == null) return_val = null;

     	//*TTY*/else return_val = (CEvent) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "replaceFormula " + sml_id + " \"" + f.toSMLString() + "\";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.replace_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), f.getFormula());    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.REPLACE_FORM, xml_in);

     	/*PIDE*/IntCEvent java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.replace_form_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCEvent();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

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

      * only implemented in Math_Engine */

     /** MATH_ENGINE: val resetCalcHead : calcID -> XML.tree */

     /**

      * @see isac.interfaces.IToCalc#resetCalcHead()

      */

     public CalcHead resetCalcHead(int calc_tree_id) throws RemoteException {

     	CalcHead return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id, "resetCalcHead @calcid@;", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "resetCalcHead " + sml_id + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.reset_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.RESET_CALCHEAD, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.reset_calchead_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val setContext : calcID -> pos' -> guh -> XML.tree */

     /* The status of this method is unclear:

      * 

      ** There is no use-case and no test

      ** The code is NOT used when showing the contexts

      *    of thy, pbl, met, exp for example Biegelinie.

      ** The code is not deleted, nevertheless, because there is

      *    code in isabisac: interface#setContext

      *    

      *  So the changes for "isabelle tty" --> libisabelle adapt to the XML 

      *  sent from isabisac interface#setContext > autocalculateOK2xml.

      */

     public CChanged setContext(int javaCalcID, ContextTheory context, Position pos ) throws RemoteException {

     	CChanged return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper =  interpretSML(javaCalcID,

     	//*TTY*/  "setContext @calcid@ " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";", false);

     	//*TTY*/if(wrapper == null) return_val = null;

     	//*TTY*/else return_val = (CChanged) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "setContext " + sml_id + " " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.set_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  pos, context.getKEStoreKey().toString() + "\"");

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.SET_CTXT, xml_in);

     	/*PIDE*/IntCEvent java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.set_ctxt_out(xml_out);

     	/*PIDE*/  return_val = (CChanged) java_out.getCEvent();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }   

     /**

      * @see isac.interfaces.IToCalc#setMethod()

      * 

      * MATH_ENGINE: val setMethod : calcID -> metID -> XML.tree

      */

     public CalcHead setMethod(int calc_tree_id, MethodID id) throws RemoteException {

     	CalcHead return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "setMethod @calcid@ " + id.toSMLString() + ";", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "setMethod " + sml_id + " " + id.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.set_met(new scala.math.BigInt(BigInteger.valueOf(sml_id)), id.getID());    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.SET_MET, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.set_met_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /** MATH_ENGINE: val setNextTactic : calcID -> tac -> XML.tree */

     public int setNextTactic(int id, Tactic tactic) {

     	int return_val = 4711;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(id, 

     	//*TTY*/  "setNextTactic @calcid@ (" + tactic.toSMLString() + ");", false);

     	//*TTY*/if (wrapper == null) return_val = -1;//WN050223 response ... MESSAGE not parsed

     	//*TTY*/if (wrapper.getResponse() == null) { return_val = 0; //Everything is ok

     	//*TTY*/} else { return_val = -1; } //An Error occcured

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "setNextTactic " + sml_id + " (" + tactic.toSMLString() + ");");    	

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.set_next_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), tactic);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.SET_NEXT_TAC, xml_in);

     	/*PIDE*/Message java_out = null;

     	/*PIDE*/if (!IsaToJava.is_syserror(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.set_next_tac_out(xml_out); //DialogGuide handles no Messages, still WN150821

     	/*PIDE*/  return_val = 0; //Everything is ok

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else {

     	/*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_syserror: REVIEW!"); 

     	/*PIDE*/}

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.interfaces.IToCalc#setProblem()

      * 

      * MATH_ENGINE: val setProblem : calcID -> pblID -> XML.tree

      */

     public CalcHead setProblem(int calc_tree_id, ProblemID id) throws RemoteException {

     	CalcHead return_val = null;

     	/*---------------------------------------------------------------------------*/

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "setProblem @calcid@ " + id.toSMLString() + ";", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "setProblem " + sml_id + " " + id.toSMLString() + ";");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.set_met(new scala.math.BigInt(BigInteger.valueOf(sml_id)), id.getID());    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.SET_PBL, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.set_met_out(xml_out);

     	/*PIDE*/  return_val = java_out.getCalcHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.interfaces.IToCalc#setTheory()

      * 

      * TODO/WN150812: use implementation in Math_Engine.

      * MATH_ENGINE: val setTheory : calcID -> thyID -> XML.tree

      */

     public CalcHead setTheory(int calc_tree_id, String thy_id)

             throws RemoteException {

     	CalcHead return_val = null;

     	Position pos = null;

     	/*---------------------------------------------------------------------------*/

        	//*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "(*setTheory*)setNextTactic @calcid@ (Specify_Theory \"" + thy_id + "\");", false);

     	//*TTY*/wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "(*setTheory*)autoCalculate @calcid@ (Step 1);", false);

     	//*TTY*///drop the CalcChanged returned by autoCalculate

     	//*TTY*/wrapper = interpretSML(calc_tree_id, 

     	//*TTY*/  "(*setTheory*)getActiveFormula @calcid@ ;", false);

     	//*TTY*/pos = moveSuccess(wrapper);

     	//*TTY*/wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "(*setTheory*)refFormula @calcid@ " + pos.toSMLString() + ";", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

         //\---End hack

     	/*---------------------------------------------------------------------------*/

         //---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)setNextTactic " + sml_id + " (Specify_Theory \"" + thy_id + "\");");    	

     	/*PIDE*/SimpleTactic tac = new SimpleTactic("Specify_Theory", thy_id + "\"");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.set_next_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), tac);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.SET_NEXT_TAC, xml_in);

     	/*PIDE*/bridge_.log(1, "<--ISA: message not sent to Dialog ... " + xml_out);

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)autoCalculate " + sml_id + " (Step 1);");   	

     	/*PIDE*/xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  "Step", new scala.math.BigInt(BigInteger.valueOf(1)));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.AUTO_CALC, xml_in);

     	/*PIDE*/bridge_.log(1, "<--ISA: CalcChanged not sent to Dialog ... " + xml_out);

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)getActiveFormula " + sml_id + ";");   	

     	/*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.GET_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.get_active_form_out(xml_out);

     	/*PIDE*/  pos = java_out.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)refFormula " + sml_id + " " + pos.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);//^^pos.setKind("DUMMY")

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.REF_FORMULA, xml_in);

     	/*PIDE*/IntFormHead java_out2 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out2 = IsaToJava.ref_formula_out(xml_out);

     	/*PIDE*/  return_val = (CalcHead)java_out2.getFormHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

        	/*PIDE*///\---End hack

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /***********************************************************************

      * Below are methods not contained in MATH_ENGINE, rather

      * they composed from other methods in Math_Engine. 

      */

     /**

      * @see isac.interfaces.IToCalc#completeCalcHead()

      */

     public CalcHead completeCalcHead(int calc_tree_id) {

     	CalcHead return_val = null;

     	Position pos = null;

     	/*---------------------------------------------------------------------------*/

        	//*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

     	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "(*completeCalcHead*)autoCalculate @calcid@ CompleteCalcHead;", false);

     	//*TTY*///drop the CalcChanged returned by autoCalculate

     	//*TTY*/wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "(*completeCalcHead*)getActiveFormula @calcid@ ;", false);

     	//*TTY*/pos = moveSuccess(wrapper);

     	//*TTY*/wrapper = interpretSML(calc_tree_id,

     	//*TTY*/  "(*completeCalcHead*)refFormula @calcid@ " + pos.toSMLString() + ";", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

     	//*TTY*///\---End hack

     	/*---------------------------------------------------------------------------*/

         //---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeCalcHead*)autoCalculate " + sml_id + "CompleteCalcHead;");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  "CompleteCalcHead", new scala.math.BigInt(BigInteger.valueOf(0)));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.AUTO_CALC, xml_in);

     	/*PIDE*/IntCEvent java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.auto_calc_out(xml_out);

     	/*PIDE*///  return_val = java_out.getCEvent();

     	/*PIDE*/bridge_.log(1, "<--ISA: not sent to Dialog ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeCalcHead*)getActiveFormula " + sml_id + ";");

     	/*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.GET_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out2 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out2 = IsaToJava.get_active_form_out(xml_out);

     	/*PIDE*/ pos = java_out2.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeCalcHead*)refFormula " + sml_id + pos.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.REF_FORMULA, xml_in);

     	/*PIDE*/IntFormHead java_out3 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out3 = IsaToJava.ref_formula_out(xml_out);

     	/*PIDE*/ return_val = (CalcHead)java_out3.getFormHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	   	

        	/*PIDE*///\---End hack

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.interfaces.IToCalc#completeModel() WN050809 push this method

      *      through to the SML-kernel

      */

     public CalcHead completeModel(int calc_tree_id) throws RemoteException {

        	CalcHead return_val = null;

     	Position pos = null;

     	/*---------------------------------------------------------------------------*/

         //*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

        	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

        	//*TTY*/  "(*completeModel*)autoCalculate @calcid@ CompleteModel;", false);

        	//*TTY*///drop the CalcChanged returned by autoCalculate

        	//*TTY*/wrapper = interpretSML(calc_tree_id,

        	//*TTY*/  "(*completeModel*)getActiveFormula @calcid@ ;", false);

        	//*TTY*/pos = moveSuccess(wrapper);

        	//*TTY*/wrapper = interpretSML(calc_tree_id,

        	//*TTY*/  "(*completeModel*)refFormula @calcid@ " + pos.toSMLString() + ";", false);

     	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

         //\---End hack

     	/*---------------------------------------------------------------------------*/

         //---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeModel*)autoCalculate " + sml_id + " CompleteModel;");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  "CompleteModel", new scala.math.BigInt(BigInteger.valueOf(0)));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.AUTO_CALC, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.set_met_out(xml_out);

     	/*PIDE*/bridge_.log(1, "<--ISA: not sent to Dialog = " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeModel*)getActiveFormula " + sml_id + ";");

     	/*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.GET_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out2 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out2 = IsaToJava.get_active_form_out(xml_out);

     	/*PIDE*/ pos = java_out2.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeModel*)refFormula " + sml_id + " " + pos.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.REF_FORMULA, xml_in);

     	/*PIDE*/IntFormHead java_out3 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out3 = IsaToJava.ref_formula_out(xml_out);

     	/*PIDE*/ return_val = (CalcHead)java_out3.getFormHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	   	

        	/*PIDE*///\---End hack

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /**

      * @see isac.interfaces.IToCalc#nextSpecify() WN050809 push this method

      *      through to the SML-kernel.

      */

     public CalcHead nextSpecify(int calc_tree_id) throws RemoteException {

        	CalcHead return_val = null;

     	Position pos = null;

     	/*---------------------------------------------------------------------------*/

        	//*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

        	//*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,

        	//*TTY*/  "(*nextSpecify*)autoCalculate @calcid@ (Step 1);", false);

        	//*TTY*///drop the CalcChanged returned by autoCalculate

        	//*TTY*/wrapper = interpretSML(calc_tree_id,

        	//*TTY*/  "(*nextSpecify*)getActiveFormula @calcid@ ;", false);

        	//*TTY*/pos = moveSuccess(wrapper);

        	//*TTY*/wrapper = interpretSML(calc_tree_id,

        	//*TTY*/  "(*nextSpecify*)refFormula @calcid@ " + pos.toSMLString() + ";", false);

        	//*TTY*/return_val = (CalcHead) wrapper.getResponse();

        	//*TTY*///\---End hack

     	/*---------------------------------------------------------------------------*/

     	/*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));

        	/*PIDE*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*nextSpecify*)autoCalculate " + sml_id + " (Step 1);");

     	/*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

     	/*PIDE*/  "Step", new scala.math.BigInt(BigInteger.valueOf(1)));

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.AUTO_CALC, xml_in);

     	/*PIDE*/IntCalcHead java_out = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out = IsaToJava.set_met_out(xml_out);

     	/*PIDE*/bridge_.log(1, "<--ISA: not sent to Dialog = " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*nextSpecify*)getActiveFormula " + sml_id + ";");

     	/*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));    	

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.GET_ACTIVE_FORM, xml_in);

     	/*PIDE*/IntPosition java_out2 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out2 = IsaToJava.get_active_form_out(xml_out);

     	/*PIDE*/ pos = java_out2.getPosition();

     	/*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	

     	/*PIDE*/bridge_.log(1, "-->ISA: " + "(*nextSpecify*)refFormula " + sml_id + pos.toSMLString() + ";");

     	/*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);//^^pos.setKind("DUMMY")

     	/*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);

     	/*PIDE*/xml_out = connection_to_kernel_.invoke(Operations.REF_FORMULA, xml_in);

     	/*PIDE*/IntFormHead java_out3 = null;

     	/*PIDE*/if (!IsaToJava.is_message(xml_out)) {

     	/*PIDE*/  java_out3 = IsaToJava.ref_formula_out(xml_out);

     	/*PIDE*/ return_val = (CalcHead)java_out3.getFormHead();

     	/*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);    	

     	/*PIDE*/} else

         /*PIDE*/  bridge_.log(1, "<--ISA: IsaToJava.is_message: REVIEW!");    	   	

        	/*PIDE*///\---End hack

     	/*---------------------------------------------------------------------------*/

         return return_val;

     }

     /***********************************************************************

      * Below are methods not implemented in MATH_ENGINE at all,

      * or only very fragmentarily.

      * WN150812 here are also methods, where the status is not clarified. 

      * Some methods seem to be replaced by similar ones.

      * TODO: review IBridgeRMI, MathEngine, etc.

      */

     /**

      * @see isac.interfaces.ICalcIterator#tryMatchMethod(MethodID)

      * @deprecated WN150812: not impl. in Math_Engine.

      */

     public Match initMatchMethod(int javaCalcID) throws RemoteException {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

           "initMatchMethod @calcid@ ;", false);

         Object response = wrapper.getResponse();

         CalcHead ch = (CalcHead) response;

         Match m = new Match(ch.getSpecification().getProblem(), ch

                 .getStatusString(), ch.getHeadLine(), ch.getModel());

         return m;

     }

     /**

      * @see isac.interfaces.ICalcIterator#tryMatchProblem(HierarchyKey)

      * @deprecated WN150812: not impl. in Math_Engine.

      */

     public Match initMatchProblem(int javaCalcID) {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

           "initMatchProblem @calcid@ ;", false);

         Object response = wrapper.getResponse();

         CalcHead ch = (CalcHead) response;

         Match m = new Match(ch.getSpecification().getProblem(), ch

                 .getStatusString(), ch.getHeadLine(), ch.getModel());

         return m;

     }

     /**

      * @deprecated in favour of getFormula

      * WN150812: but used frequently ?!

      */

     public boolean moveFormula(int javaCalcID, int iteratorID) {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

           "moveFormula @calcid@ " + iteratorID + ";", false);

         return true;//WN041208 moveSuccess(wrapper);

     }

     /** WN150812 unused ? */

     private Position moveSuccess(ResponseWrapper wrapper) {

         if (wrapper == null)

             return null;

         else {

             Object r = wrapper.getResponse();

             if (r instanceof CMessage)

                 return null;//TODO.WN041209 handle messages

             else {

                 Position p = (Position) wrapper.getResponse();

                 return p;

             }

         }

     }

     /**

      * @deprecated in favour of getTactic

      * WN150812: but used frequently ?!

      */

     public boolean moveTactic(int javaCalcID, int iteratorID) {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

                 "moveTactic @calcid@ " + iteratorID + ";", false);

         return true;//WN041208 moveSuccess(wrapper);

     }

     /**

      * @see isac.interfaces.ICalcIterator#tryMatchMethod(MethodID)

      * @deprecated is not impl. in math-engine !!!

      */

     public Match tryMatchMethod(int javaCalcID, MethodID keStoreID)

             throws RemoteException {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

                 "tryMatchMethod @calcid@ " + keStoreID.toSMLString() + ";",

                 false);

         Object response = wrapper.getResponse();

         CalcHead ch = (CalcHead) response;

         Match m = new Match(ch.getSpecification().getProblem(), ch

                 .getStatusString(), ch.getHeadLine(), ch.getModel());

         return m;

     }

     /** enforced by IBridgeRMI, WN150812: exp-, met-, pbl-, thy-contexts all work --

      * -- see: CChanged setContext(int, ContextTheory, ... */

 	@Override

 	public CalcHead setContext(int javaCalcID, ContextMethod context, Position pos) throws RemoteException {

 		return null;

 	}

     /** enforced by IBridgeRMI, WN150812: exp-, met-, pbl-, thy-contexts all work --

      * -- see: CChanged setContext(int, ContextTheory, ... 

      * This method changed role with ^^^^^^^^^^^^^^^^ during "isabelle tty" --> libisabelle

      */

 	@Override

 	public CalcHead setContext(int javaCalcID, ContextProblem context, Position pos) throws RemoteException {

 		return null;

 	}

     /**

      * @see isac.interfaces.ICalcIterator#tryMatchProblem(HierarchyKey)

      * 

      * WN150812: tryMatchProblem, trymatch only partially implemented in Math_Engine

      */

     public Match tryMatchProblem(int javaCalcID, ProblemID problemID) {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

                 "tryMatchProblem @calcid@ " + problemID.toSMLString() + ";",

                 false);

         Object response = wrapper.getResponse();

         CalcHead ch = (CalcHead) response;

         Match m = new Match(ch.getSpecification().getProblem(), ch

                 .getStatusString(), ch.getHeadLine(), ch.getModel());

         return m;

     }

     /**

      * @see isac.interfaces.ICalcIterator#tryRefineProblem(HierarchyKey)

      * @deprecated in favour of refineProblem.

      */

     public Match tryRefineProblem(int javaCalcID, ProblemID problemID) {

         ResponseWrapper wrapper = interpretSML(javaCalcID,

                 "tryRefineProblem @calcid@ " + problemID.toSMLString() + ";",

                 false);

         Object response = wrapper.getResponse();

         CalcHead ch = (CalcHead) response;

         Match m = new Match(ch.getSpecification().getProblem(), ch

                 .getStatusString(), ch.getHeadLine(), ch.getModel());

         return m;

     }

     /***********************************************************************

      * Below are methods for restoring Isabelle/Isac after a crash.

      * This never worked, is to be deleted and 

      * to be reconsidered with introduction of libisabelle.

      */

     /**

      * This method is used when the kernel crashes and the CalcTrees need to be

      * entered again to the kernel to restore the previous state. The

      * Java-CalcIDs stay the same

      */

     public void restoreExistingCalcTrees() {

         bridge_.log(1, "---- entering restoreExistingCalcTrees");

         Iterator it = java_calcid_to_smlcalcid_.keySet().iterator();

         // keySet = javaCalcIDs

         int javaCalcID, newSmlCalcID;

         Vector v;

         while (it.hasNext()) {

             //bridge.log(1, "1");

             //int i = ((Integer)it.next()).intValue();

             javaCalcID = ((Integer) it.next()).intValue();

             //bridge.log(1, "2");

             v = saveCalcTree(javaCalcID);

             //bridge.log(1, "3");

             this.restoreToSML(javaCalcID, v);

         }

         bridge_.log(1, "---- done restoreExistingCalcTrees");

     }

     private void restoreToSML(int javaCalcID, Vector v) {

         Iterator it = ((Vector) v.clone()).iterator();

         CalcTree result = null;

         String s = (String) it.next();

         int smlCalcID = newCalculation(javaCalcID, s, null/*never worked*/, true);

         //javaCalcIDtoSmlCalcID.put(new Integer(javaCalcID), new

         // Integer(smlCalcID));

         //int smlID = ((Integer)javaCalcIDtoSmlCalcID.get(new

         // Integer(calcID))).intValue();

         while (it.hasNext()) {

             s = (String) it.next();

             interpretSML(javaCalcID, s, true);

         }

     }

     /**

      * Save a calcTree for later restoring (probably to another SML Kernel)

      * 

      * @param calcTreeID

      *            the ID of the calcTree

      * @return a vector containing strings. This is representatation of the

      *         status of the calcTree

      */

     public Vector saveCalcTree(int calcTreeID) {

         this.bridge_.log(1, "----------------begin saving calcTree "

                 + calcTreeID + "------------");

         return (Vector) inputs_.get(new Integer(calcTreeID));

     }

 }