/**

 * 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.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.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));

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

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

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

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

    	/*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();

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

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

    	/*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();

        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;

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

    	/*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 TODO = 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: " + TODO);

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

    	/*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!");    	

    	//THIS RUN ON TestBridge: ----------------------------------------------------

    	//*PIDE*/XML.Tree AUTO_CALC_out = connection_to_kernel_.invoke(Operations.AUTO_CALC,

    	//*PIDE*/  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: " + AUTO_CALC_out);

    	//*PIDE*/IntCChanged calcid_cc = IsaToJava.auto_calc_out(AUTO_CALC_out);

    	//*PIDE*/int calcid = calcid_cc.getCalcId();

    	//*PIDE*/return_val = (CEvent) calcid_cc.getCChanged();

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

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

    	/*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();

        /*\-------------------------------------------------------------------------/*/

        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;

        //----- Mini_Test step 1, 2, 3 -----------------------------------------------\

        /*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();

        //----- Mini_Test step 2 WN150808 try to drop this step, see WN041209

        /*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);

        //----- Mini_Test step 3

        /*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);

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

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

        /*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);

        /*\-------------------------------------------------------------------------/*/

        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;

    	/*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 TODO = JavaToIsa.check_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)), 

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

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

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

    	/*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!");    	

    	/*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();

        return return_val;

    }    

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

    public boolean destruct(int javaCalcID) {

    	boolean return_val;

    	/*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 = null;

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

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

    	/*PIDE*/  return_val = true;

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

    	/*PIDE*/} else

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

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

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

    	/*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;

    	/*\-------------------------------------------------------------------------/*/

    	java_calcid_to_smlcalcid_.remove(new Integer(javaCalcID));

    	return return_val;

    }

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

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

    	Vector return_val = null;

    	/*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 TODO = 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: " + TODO);

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

    	/*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();

        return return_val;

    }

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

    public Tactic fetchProposedTactic(int id) {

    	Tactic return_val = null;

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

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

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

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

        //----^^^ delete at end of phase-2a ------------------------------------------------

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        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;

    	/*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 TODO = JavaToIsa.get_accumulated_asms(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        return return_val;

    }

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

    public Position getActiveFormula(int javaCalcID) {

    	Position return_val = null;

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

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

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

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        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;

    	/*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 TODO = JavaToIsa.get_asms(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        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 TODO = null;

    	ResponseWrapper wrapper = null;

        Vector return_val = null;      

        //----- Mini_Test step 4 ------------------------------------------------------

        /*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*/  TODO = 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: " + TODO);

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

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

    	//THIS RUN ON TestBridge:

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

        //*PIDE*/try { GET_FORMULAE_out = connection_to_kernel_.invoke(Operations.GET_FORMULAE,

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

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

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

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

        //*PIDE*/IntFormulas calcid_forms = IsaToJava.get_formulae_out(GET_FORMULAE_out);

        //*PIDE*/sml_id = calcid_forms.getCalcId();

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

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

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

        /*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;

        /*\-------------------------------------------------------------------------/*/

        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;

    	/*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 TODO = JavaToIsa.get_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);    	

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        return return_val;

    }

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

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

    	Context return_val = null;

    	/*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 TODO = JavaToIsa.init_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)), type, pos);    	

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

    	/*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();

        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;

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

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

    	/*PIDE*/try {

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

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

    	/*PIDE*/try {

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

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

    	/*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();

        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;

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

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

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

        /*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_

        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;

    	/*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 TODO = new scala.math.BigInt(BigInteger.valueOf(sml_id));    	

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

        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;

    	/*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 TODO = JavaToIsa.modify_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)), calchead);    	

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        return return_val;

    }

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

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

    	Position return_val = null;

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

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

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

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

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

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

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

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

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

    	/*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);

        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;

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

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

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

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

    	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_DOWN, TODO);

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

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

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

    	/*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);

        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;

    	/*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 TODO = JavaToIsa.move_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);    	

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

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

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

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

        return return_val;

    }

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

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

    	Position return_val = null;

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

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

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

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

    	/*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(Operations.MOVE_ACTIVE_LEVDN, TODO);

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

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

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

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

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

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

    	//*PIDE*/return_val = TODOTODOTODOTODO;

    	/*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);

        return return_val;

    }

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