2 * Created on Oct 13, 2003
3 * @author Richard Gradischnegg RG
7 import isac.bridge.xml.DataTypes;
8 import isac.bridge.xml.IntAssumptions;
9 import isac.bridge.xml.IntCalcHead;
10 import isac.bridge.xml.IntCEvent;
11 import isac.bridge.xml.IntFormHead;
12 import isac.bridge.xml.IntFormulas;
13 import isac.bridge.xml.IntIntCompound;
14 import isac.bridge.xml.IntContext;
15 import isac.bridge.xml.IntPosition;
16 import isac.bridge.xml.IntTactic;
17 import isac.bridge.xml.IntTacticErrPats;
18 import isac.bridge.xml.IntTactics;
19 import isac.bridge.xml.IsaToJava;
20 import isac.bridge.xml.JavaToIsa;
21 import isac.interfaces.ICalcElement;
22 import isac.interfaces.ICalcIterator;
23 import isac.interfaces.IToCalc;
24 import isac.util.Formalization;
25 import isac.util.Message;
26 import isac.util.ResponseWrapper;
27 import isac.util.formulae.Assumptions;
28 import isac.util.formulae.CalcHead;
29 import isac.util.formulae.Context;
30 import isac.util.formulae.ContextMethod;
31 import isac.util.formulae.ContextProblem;
32 import isac.util.formulae.ContextTheory;
33 import isac.util.formulae.HierarchyKey;
34 import isac.util.formulae.CalcFormula;
35 import isac.util.formulae.Match;
36 import isac.util.formulae.MethodID;
37 import isac.util.formulae.Position;
38 import isac.util.formulae.ProblemID;
39 import isac.util.parser.XMLParserDigest;
40 import isac.util.tactics.SimpleTactic;
41 import isac.util.tactics.Tactic;
42 import isac.wsdialog.IContextProvider.ContextType;
43 import edu.tum.cs.isabelle.api.XML;
44 import edu.tum.cs.isabelle.japi.JSystem;
46 import java.io.BufferedReader;
47 import java.io.IOException;
48 import java.io.InputStreamReader;
49 import java.io.PrintWriter;
50 import java.math.BigInteger;
51 import java.net.MalformedURLException;
52 import java.net.Socket;
53 import java.net.UnknownHostException;
54 import java.rmi.Naming;
55 import java.rmi.RMISecurityManager;
56 import java.rmi.RemoteException;
57 import java.rmi.registry.LocateRegistry;
58 import java.rmi.server.UnicastRemoteObject;
59 import java.util.HashMap;
60 import java.util.Iterator;
63 import java.util.Vector;
65 import scala.math.BigInt;
67 import org.apache.log4j.Logger;
70 * @author Richard Gradischnegg RG
72 * WN0422 here seems to be the key for simplifying the whole bridge.* drawbacks
73 * of the present implementation: # more complicated than necessary #
74 * JUnitTestCases require BridgeMain running # BridgeLogger cannot be made
75 * serializable, thus not accessible for writing by JUnitTestCases #
77 public class BridgeRMI extends UnicastRemoteObject implements IBridgeRMI {
79 static final long serialVersionUID = -3047706038036289437L;
80 private static final Logger logger = Logger.getLogger(BridgeRMI.class.getName());
82 private BridgeMain bridge_;
84 private XMLParserDigest xml_parser_digest_;
86 // Socket used to communicate with bridge
87 private Socket socket_ = null;
89 // Writer to write sml requests to the kernel
90 private PrintWriter out_ = null;
92 // Reader to read sml response from kernel
93 private BufferedReader in_ = null;
100 * Maps the Java calc(Tree)rmiID to the sml calc(Tree)rmiID. A mapping is
101 * nescessary because these ids are not (nescessary) the same: For example
102 * when restoring the kernel, the calcTree rmiID can change because of
103 * already finished CalcTrees no longer existing and their CalcId assigned
104 * to another CalcTree. key: Integer (javaCalcID) value: Integer (smlCalcID)
106 private Map java_calcid_to_smlcalcid_;
109 * This map stores user inputs which have already been answered by the
110 * kernel and the response being sent back to the user. These inputs are
111 * resent to the kernel in the case of a newstart of the kernel. key:
112 * Integer (javaCalcID) value: Vector (containing input strings)
115 private JSystem connection_to_kernel_;
117 public BridgeRMI(BridgeMain bridge, String host, int port, String dtdPath)
118 throws RemoteException {
119 if (logger.isDebugEnabled())
120 logger.debug("BridgeRMI obj.init: bridge=" + bridge + ", host=" + host
121 + ", port=" + port + ", dtdPath=" + dtdPath);
123 this.bridge_ = bridge;
124 this.connection_to_kernel_ = bridge.getConnectionToKernel();
125 in_ = bridge.getSmlReader();
127 socket_ = new Socket(host, port);
128 out_ = new PrintWriter(socket_.getOutputStream(), true);
129 in_ = new BufferedReader(new InputStreamReader(socket_
131 } catch (UnknownHostException e) {
132 System.out.println("Unknown host: " + host + "\n");
133 } catch (IOException e) {
134 System.out.println("probably just a remainder of 'bridge-internal RMI'");
137 xml_parser_digest_ = new XMLParserDigest(dtdPath);
138 //xml_parser_digest_.setValidating(true);
139 //...all XML-data should be tested in
140 //javatest.isac.util.parser.TestXMLParserDigest
141 inputs_ = new HashMap<Integer, Vector<String>>();
142 java_calcid_to_smlcalcid_ = new HashMap<Integer, Integer>();
146 * Buffers input sent to the sml-Kernel (for later possible restart)
149 * calcTree this input belongs to
153 public void bufferInput(int javaCalcID, String input) {
154 Vector<String> v = (Vector<String>) inputs_.get(new Integer(javaCalcID));
157 inputs_.put(new Integer(javaCalcID), v);
162 // '@calcid@' is a placeholder for the CalcID
163 // this method replaces it with a real CalcID
164 private String insertCalcID(int id, String s) {
165 return s.replaceAll("@calcid@", String.valueOf(id));
168 // return smallest integer which is not yet
169 // used as a (java)CalcID
170 private int smallestFreeCalcID() {
171 Set<?> set = java_calcid_to_smlcalcid_.keySet();
172 for (int i = 0; i < set.size(); i++) {
173 if (!set.contains(new Integer(i))) {
181 * Send a sml instruction to the kernel. restore == true, if the instruction
182 * is resent after the kernel crashed
184 private ResponseWrapper sendToKernel(String smlInstr, boolean restore) {
185 if (logger.isDebugEnabled())
186 logger.debug(" BR->KN: sendToKernel(" + smlInstr + ")");
187 ResponseWrapper wrapper = null;
188 //bridge.log(1,"---sendToKernel |
189 //bridge.isRestoring=="+bridge.isRestoring());
190 //bridge.log(1,"---sendToKernel | restoring=="+restore);
191 if (!bridge_.isRestoring() || restore) {
192 String xmlString = "";
194 out_.println(smlInstr);// send the sml Instruction to the sml Kernel
196 xmlString = in_.readLine();//read the response from the kernel
197 if (logger.isInfoEnabled())
198 logger.info(" BR<-KN: sendToKernel <- xml= " + xmlString);
199 } catch (IOException e) {
200 bridge_.log(1, "BridgeRMI.interpretSKN: IOException");
203 //if (!(restore) && bridge.isRestoring()) {
204 // this.restoreExistingCalcTrees();
207 bridge_.log( 1, xmlString );
208 wrapper = xml_parser_digest_.parse(xmlString);
214 * Send an instruction to the SML-Kernel and return the response
218 * @return response from SML-Kernel
220 private synchronized ResponseWrapper interpretSML(int javaCalcID,
221 String instr, boolean restore) {
224 Integer smlCalcInteger = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
225 if( smlCalcInteger == null ) {
226 bridge_.log(1, "smlCalcInteger is null for javaCalcID : " + javaCalcID );
230 smlCalcID = smlCalcInteger.intValue();
231 String smlInstr = insertCalcID(smlCalcID, instr);
232 bridge_.log(1, "JavaCalcID " + javaCalcID + " == SmlCalcID "
234 bridge_.log(1, "sent to bridge: " + smlInstr);
235 ResponseWrapper wrapper = this.sendToKernel(smlInstr, restore);
237 bufferInput(javaCalcID, smlInstr);
241 private void rmiBind() {
242 if (logger.isDebugEnabled())
243 logger.debug("rmiBind");
244 if (System.getSecurityManager() == null) {
245 System.setSecurityManager(new RMISecurityManager());
248 String name = "//" + host_ + "/BridgeRMI";
250 System.out.println("try to bind as " + name);
251 Naming.rebind(name, this);
252 System.out.println("Bridge RMI bound to " + name);
253 } catch (java.rmi.ConnectException e) {
254 System.err.println("failed to contact as " + name + " (creating RMI-Server on localhost: 1099)");
256 LocateRegistry.createRegistry(1099);
257 } catch (java.rmi.RemoteException exc2) {
258 System.err.println("can not create registry: " + exc2.getMessage());
262 } catch (RemoteException e) {
263 System.err.println("RemoteException");
264 System.err.println(e.getMessage());
265 System.err.println(e.getCause().getMessage());
266 System.err.println(e.getCause().getClass());
270 } catch (MalformedURLException e) {
271 System.err.println(e.getMessage());
275 } catch (Exception e) {
276 System.err.println("----------- Exception");
277 System.err.println(e.getClass().getName());
278 System.err.println(e.getMessage());
286 * Restore a saved calcTree.
289 * Vector containing strings
290 * @return Java CalcTreeID (not SML-ID)
292 public int loadCalcTree(Vector v) {
293 this.bridge_.log(1, "----------------begin loading------------");
294 int javaCalcID = smallestFreeCalcID();
295 this.bridge_.log(1, "-----smallest free = " + javaCalcID);
296 restoreToSML(javaCalcID, v);
297 this.bridge_.log(1, "----------------done loading-------------");
301 public int smlCalcIDtoJavaCalcID(int smlID) {
302 Iterator<?> it = java_calcid_to_smlcalcid_.keySet().iterator();
303 while (it.hasNext()) {
304 Object key = it.next();
305 Integer value = (Integer) java_calcid_to_smlcalcid_.get(key);
306 if (value.intValue() == smlID) {
307 return ((Integer) key).intValue();
313 public Map<?, Vector<String>> getInputs() {
317 public int getRmiID() {
321 public void setRmiID(int i) {
322 if (logger.isDebugEnabled())
323 logger.debug("setRmiID: i=" + i);
328 * causes a CalcChanged event for the first line on the Worksheet
331 * for the CalcTree (unused)
332 * @return CalcChanged with Iterators pointing at the root of the CalcTree
334 public CChanged startCalculate(int id) {
335 Position p = new Position();
336 p.setKind("Pbl");// toSMLString --> ([],"Pbl")
337 CChanged cc = new CChanged();
338 cc.setLastUnchanged(p);
339 cc.setLastDeleted(p);
340 cc.setLastGenerated(p);
345 * Starts the specifying phase: fill the calcTree with the appropriate
346 * information. Once the calc_head_ is fully specified, the user can begin
347 * with the actual calculation.
350 * Formalization for this calculation (empty if user starts a
351 * complete new calculation)
354 public int getCalcTree(Formalization formalization) {
356 int javaCalcID = smallestFreeCalcID();
357 this.bridge_.log(1, "-----smallest free javaCalcID = " + javaCalcID);
358 newCalculation(javaCalcID,
359 "CalcTree " + formalization.toSMLString() + ";", formalization, false);
360 return_val = javaCalcID;
364 /***********************************************************************
365 * Below are all the methods in structure Math_Engine : MATH_ENGINE
366 * listed in the same order as in the signature.
367 * The previous order still reflected original development;
368 * method names reflect the original struggle at the
369 * interface Java <--> Isabelle/Isac: different names are made explicit.
372 /** MATH_ENGINE: val appendFormula : calcID -> cterm' -> XML.tree */
373 public CEvent appendFormula(int id, CalcFormula f) {
374 CEvent return_val = null;
375 int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
376 /*---------------------------------------------------------------------------*/
377 //*TTY*/ResponseWrapper wrapper = null;
378 //*TTY*/wrapper = interpretSML(id, "appendFormula @calcid@ \"" + f.toSMLString() + "\";", false);
379 //*TTY*/if (wrapper == null) return null;
380 //*TTY*/return_val = (CEvent) wrapper.getResponse();
381 /*---------------------------------------------------------------------------*/
382 /*PIDE*/bridge_.log(1, "-->ISA: " + "appendFormula " + sml_id + " \"" + f.toSMLString() + "\";");
383 /*PIDE*/XML.Tree xml_in = JavaToIsa.append_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), f.getFormula());
384 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
385 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.APPEND_FORM, xml_in);
387 /*PIDE*/IntCEvent java_out = null;
388 /*PIDE*/if (!IsaToJava.is_message(xml_out)) java_out = IsaToJava.append_form_out(xml_out);
389 /*PIDE*/// else: no message handling by DialogGuide
390 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
391 /*PIDE*/return_val = java_out.getCEvent();
392 /*---------------------------------------------------------------------------*/
396 /** MATH_ENGINE: val autoCalculate : calcID -> auto -> XML.tree */
397 public CEvent autoCalculate(int id, int scope, int steps) {
398 if (logger.isDebugEnabled())
399 logger.debug("BridgeRMI#autoCalculate: id=" + id + ", scope" + scope + ", steps" + steps);
400 CEvent return_val = null;
401 int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
403 /*---------------------------------------------------------------------------*/
404 //*TTY*/if ((scope == 3) && (steps == 0)) { //scope ==3 means IToCalc.SCOPE_CALCHEAD:
405 //*TTY*/ wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteCalcHead;", false);
406 //*TTY*/} else if ((scope == IToCalc.SCOPE_CALCULATION) && (steps == 0)) {
407 //*TTY*/ wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteCalc;", false);
408 //*TTY*/} else if ((scope == IToCalc.SCOPE_MODEL) && (steps == 0)) {
409 //*TTY*/ wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteModel;", false);
410 //*TTY*/} else if ((scope == IToCalc.SCOPE_SUBCALCULATION) && (steps == 0)) {
411 //*TTY*/ wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteToSubpbl;", false);
412 //*TTY*/} else if ((scope == IToCalc.SCOPE_SUBPROBLEM) && (steps == 0)) {
413 //*TTY*/ wrapper = interpretSML(id, "autoCalculate @calcid@ CompleteSubpbl;", false);
414 //*TTY*/} else { //FIXXXME040624: steps do not regard the scope
415 //*TTY*/ wrapper = interpretSML(id, "autoCalculate @calcid@ (Step " + steps + ");", false);
417 //*TTY*/if (wrapper == null) return_val = null;
418 //*TTY*/return_val = (CEvent) wrapper.getResponse();
419 //-----------------------------------------------------------------------------
420 /*PIDE*/String scope_str;
421 /*PIDE*/if ((scope == 3) && (steps == 0)) { //scope ==3 means IToCalc.SCOPE_CALCHEAD:
422 /*PIDE*/ scope_str = "CompleteCalcHead"; //FIXXXME.WN040624 steps == 0 hides mismatch in specifications
423 /*PIDE*/} else if ((scope == IToCalc.SCOPE_CALCULATION) && (steps == 0)) {
424 /*PIDE*/ scope_str = "CompleteCalc";
425 /*PIDE*/} else if ((scope == IToCalc.SCOPE_MODEL) && (steps == 0)) {
426 /*PIDE*/ scope_str = "CompleteModel";
427 /*PIDE*/} else if ((scope == IToCalc.SCOPE_SUBCALCULATION) && (steps == 0)) {
428 /*PIDE*/ scope_str = "CompleteToSubpbl";
429 /*PIDE*/} else if ((scope == IToCalc.SCOPE_SUBPROBLEM) && (steps == 0)) {
430 /*PIDE*/ scope_str = "CompleteSubpbl";
431 /*PIDE*/} else { //FIXXXME040624: steps do not regard the scope
432 /*PIDE*/ scope_str = "Step"; // steps > 0 according to impl.in "isabelle tty"
434 /*PIDE*/if (steps == 0) log_str = scope_str; else log_str = "(Step " + steps + ")";
435 /*PIDE*/bridge_.log(1, "-->ISA: " + "autoCalculate " + sml_id + " " + log_str + ";");
437 /*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
438 /*PIDE*/ scope_str, new scala.math.BigInt(BigInteger.valueOf(steps)));
439 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
440 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.AUTO_CALC, xml_in);
442 /*PIDE*/IntCEvent java_out = null;
443 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
444 /*PIDE*/ java_out = IsaToJava.auto_calc_out(xml_out);
445 /*PIDE*/ return_val = java_out.getCEvent();
446 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
448 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
449 /*---------------------------------------------------------------------------*/
453 /** MATH_ENGINE: val applyTactic : calcID -> pos' -> tac -> XML.tree
454 * not implemented in Math_Engine.
455 * compare setNextTactic. */
458 * Starts a new calculation in the sml-Kernel: i.e. a new CalcTree with the
462 * "CalcTree" + Formalization in string Representation
464 * @return sml_calcid //WN150817 why return SML(?!) calcid to Java(?!)
466 * MATH_ENGINE: val CalcTree : fmz list -> XML.tree
468 private synchronized int newCalculation(int javaCalcID, String instr,
469 Formalization fmz, boolean restore) {
471 if (logger.isDebugEnabled())
472 logger.debug("newCalculation: javaCalcID=" + javaCalcID + ", instr" + instr + ", restore=" + restore);
475 /*---------------------------------------------------------------------------*/
476 //*TTY*/bridge_.log(1, "new calculation: " + instr);
477 //*TTY*/ResponseWrapper wrapper = sendToKernel(instr, restore);
478 //*TTY*/if (wrapper == null) return -1;
479 //*TTY*/sml_calcid = wrapper.getCalcID();
480 //*TTY*/sendToKernel("Iterator " + sml_calcid + ";", restore);//WN041209 no
481 //*TTY*/sendToKernel("moveActiveRoot " + sml_calcid + ";", restore);//WN041209
482 //*TTY*/if (!restore) bufferInput(javaCalcID, instr);
483 /*---------------------------------------------------------------------------*/
484 /*PIDE*/bridge_.log(1, "-->ISA: " + instr);
485 /*PIDE*/bridge_.log(1, "-->ISA: " + DataTypes.xml_of_Formalization(fmz));
486 /*PIDE*/XML.Tree CALC_TREE_out = connection_to_kernel_.invoke(IsacOperations.CALC_TREE,
487 /*PIDE*/ DataTypes.xml_of_Formalization(fmz));
488 /*PIDE*/bridge_.log(1, "<--ISA: " + CALC_TREE_out);
489 /*PIDE*/sml_calcid = (IsaToJava.calc_tree_out(CALC_TREE_out)).intValue();
491 /*PIDE*/bridge_.log(1, "-->ISA: " + "Iterator " + sml_calcid + ";");
492 /*PIDE*/XML.Tree ITERATOR_out = connection_to_kernel_.invoke(IsacOperations.ITERATOR,
493 /*PIDE*/ new scala.math.BigInt(BigInteger.valueOf(sml_calcid)));
494 /*PIDE*/IntIntCompound int_int = IsaToJava.iterator_out(ITERATOR_out);
495 /*PIDE*/sml_calcid = int_int.getCalcId().intValue();
496 int_int.getUserId().intValue();
497 /*PIDE*/bridge_.log(1, "<--ISA: " + ITERATOR_out);
499 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveRoot " + sml_calcid + ";");
500 /*PIDE*/XML.Tree MOVE_ACTIVE_ROOT_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_ROOT,
501 /*PIDE*/ new scala.math.BigInt(BigInteger.valueOf(sml_calcid)));
502 /*PIDE*/IntPosition calcid_pos = IsaToJava.move_active_root_out(MOVE_ACTIVE_ROOT_out);
503 /*PIDE*/return_val = calcid_pos.getCalcId();
504 calcid_pos.getPosition();
505 /*PIDE*/bridge_.log(1, "<--ISA: " + MOVE_ACTIVE_ROOT_out);
506 /*---------------------------------------------------------------------------*/
507 java_calcid_to_smlcalcid_.put(new Integer(javaCalcID), new Integer(sml_calcid));
508 return_val = sml_calcid; //WN150808 SML_caldid --> JAVA frontend ?!?
512 /** MATH_ENGINE: val checkContext : calcID -> pos' -> guh -> XML.tree */
513 public Context checkContext(int javaCalcID, Context context, Position pos) throws RemoteException {
514 Context return_val = null;
515 /*---------------------------------------------------------------------------*/
516 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
517 //*TTY*/ "checkContext @calcid@ " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";", false);
518 //*TTY*/if(wrapper == null) return null;
519 //*TTY*/return_val = (Context) wrapper.getResponse();
520 /*---------------------------------------------------------------------------*/
521 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
522 /*PIDE*/bridge_.log(1, "-->ISA: " + "checkContext " + sml_id + " " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";");
524 /*PIDE*/XML.Tree xml_in = JavaToIsa.check_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
525 /*PIDE*/ pos, context.getKEStoreKey().toString() + "\"");
526 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
527 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.CHECK_CTXT, xml_in);
529 /*PIDE*/ContextTheory java_out = null;
530 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
531 /*PIDE*/ java_out = IsaToJava.check_ctxt_out(xml_out);
532 /*PIDE*/ return_val = java_out;
533 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
535 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
536 /*---------------------------------------------------------------------------*/
540 /** MATH_ENGINE: val DEconstrCalcTree : calcID -> XML.tree */
541 public boolean destruct(int javaCalcID) {
543 /*---------------------------------------------------------------------------*/
544 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
545 //*TTY*/ "DEconstrCalcTree @calcid@;", false);
546 //*TTY*/if (wrapper == null) { return_val = false; }
547 //*TTY*/inputs_.remove(new Integer(javaCalcID));
548 //*TTY*/return_val = true;
549 /*---------------------------------------------------------------------------*/
550 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
551 /*PIDE*/bridge_.log(1, "-->ISA: " + "DEconstrCalcTree " + sml_id);
552 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.DEL_CALC,
553 /*PIDE*/ new scala.math.BigInt(BigInteger.valueOf(sml_id)));
555 IsaToJava.del_calc_out(xml_out);
556 /*PIDE*/return_val = true;
557 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
558 /*---------------------------------------------------------------------------*/
559 java_calcid_to_smlcalcid_.remove(new Integer(javaCalcID));
563 /** MATH_ENGINE: val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree */
564 public Vector<Tactic> getAppliableTactics(int id, int scope, Position pos) {
565 Vector<Tactic> return_val = null;
566 /*---------------------------------------------------------------------------*/
567 //*TTY*/ResponseWrapper wrapper = interpretSML(id,
568 //*TTY*/ "fetchApplicableTactics @calcid@ " + scope + pos.toSMLString() + ";", false);
569 //*TTY*/if (wrapper == null) return null;
570 //*TTY*/TacticsContainer tc = (TacticsContainer) wrapper.getResponse();
571 //*TTY*/if( tc == null ) return null;
572 //*TTY*/return_val = tc.getTactics();
573 /*---------------------------------------------------------------------------*/
574 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
575 /*PIDE*/bridge_.log(1, "-->ISA: " + "fetchApplicableTactics " + sml_id + " " + scope + pos.toSMLString() + ";");
577 /*PIDE*/XML.Tree xml_in = JavaToIsa.fetch_applicable_tacs(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
578 /*PIDE*/ new scala.math.BigInt(BigInteger.valueOf(scope)), pos);
579 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
580 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.FETCH_APPL_TACS, xml_in);
582 /*PIDE*/IntTactics java_out = null;
583 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
584 /*PIDE*/ java_out = IsaToJava.fetch_applicable_tacs_out(xml_out);
585 /*PIDE*/ return_val = java_out.getTactics();
586 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
588 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
589 /*---------------------------------------------------------------------------*/
593 /** MATH_ENGINE: val fetchProposedTactic : calcID -> XML.tree */
594 public Tactic fetchProposedTactic(int id) {
595 Tactic return_val = null;
596 /*---------------------------------------------------------------------------*/
597 //*TTY*/ResponseWrapper wrapper = interpretSML(id, "fetchProposedTactic @calcid@;", false);
598 //*TTY*/if (wrapper == null) { return null; }
599 //*TTY*/return_val = (Tactic) wrapper.getResponse();
600 /*---------------------------------------------------------------------------*/
601 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
602 /*PIDE*/bridge_.log(1, "-->ISA: " + "fetchProposedTactic " + sml_id + ";");
604 /*PIDE*/XML.Tree xml_in = JavaToIsa.fetch_proposed_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
605 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
606 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.FETCH_PROP_TAC, xml_in);
608 /*PIDE*/IntTacticErrPats java_out = null;
609 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
610 /*PIDE*/ java_out = IsaToJava.fetch_proposed_tac_out(xml_out);
611 /*PIDE*/ return_val = java_out.getTactic();
612 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
614 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
615 /*---------------------------------------------------------------------------*/
619 /** MATH_ENGINE: val findFillpatterns : calcID -> errpatID -> XML.tree
620 * only implemented in Math_Engine */
623 * @see isac.bridge.IBridgeRMI#getAccumulatedAssumptions(int,
624 * isac.util.formulae.Position)
626 * ** MATH_ENGINE: val getAccumulatedAsms : calcID -> pos' -> XML.tree
628 public Assumptions getAccumulatedAssumptions(int calcTreeID, Position pos) throws RemoteException {
629 Assumptions return_val = null;
630 /*---------------------------------------------------------------------------*/
631 //*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,
632 //*TTY*/ "getAccumulatedAsms @calcid@ " + pos.toSMLString() + ";", false);
633 //*TTY*/return_val = (Assumptions) wrapper.getResponse();
634 /*---------------------------------------------------------------------------*/
635 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));
636 /*PIDE*/bridge_.log(1, "-->ISA: " + "getAccumulatedAsms " + sml_id + " " + pos.toSMLString() + ";");
638 /*PIDE*/XML.Tree xml_in = JavaToIsa.get_accumulated_asms(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);
639 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
640 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ACC_ASMS, xml_in);
642 /*PIDE*/IntAssumptions java_out = null;
643 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
644 /*PIDE*/ java_out = IsaToJava.get_accumulated_asms_out(xml_out);
645 /*PIDE*/ return_val = java_out.getAssumptions();
646 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
648 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
649 /*---------------------------------------------------------------------------*/
653 /** MATH_ENGINE: val getActiveFormula : calcID -> XML.tree */
654 public Position getActiveFormula(int javaCalcID) {
655 Position return_val = null;
656 /*---------------------------------------------------------------------------*/
657 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
658 //*TTY*/ "getActiveFormula @calcid@ ;", false);
659 //*TTY*/return_val = moveSuccess(wrapper);
660 /*---------------------------------------------------------------------------*/
661 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
662 /*PIDE*/bridge_.log(1, "-->ISA: " + "getActiveFormula " + sml_id + " ;");
664 /*PIDE*/XML.Tree xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
665 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
666 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ACTIVE_FORM, xml_in);
668 /*PIDE*/IntPosition java_out = null;
669 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
670 /*PIDE*/ java_out = IsaToJava.get_active_form_out(xml_out);
671 /*PIDE*/ return_val = java_out.getPosition();
672 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
674 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
675 /*---------------------------------------------------------------------------*/
680 * @see isac.bridge.IBridgeRMI#getAssumption(int, int)
682 * MATH_ENGINE: val getAssumptions : calcID -> pos' -> XML.tree
684 public Assumptions getAssumptions(int calcTreeID, Position pos) throws RemoteException {
685 Assumptions return_val = null;
686 /*---------------------------------------------------------------------------*/
687 //*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,
688 //*TTY*/ "getAssumptions @calcid@ " + pos.toSMLString() + ";", false);
689 //*TTY*/return_val = (Assumptions) wrapper.getResponse();
690 /*---------------------------------------------------------------------------*/
691 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));
692 /*PIDE*/bridge_.log(1, "-->ISA: " + "getAssumptions " + sml_id + " " + pos.toSMLString() + ";");
694 /*PIDE*/XML.Tree xml_in = JavaToIsa.get_asms(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);
695 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
696 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ASMS, xml_in);
698 /*PIDE*/IntAssumptions java_out = null;
699 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
700 /*PIDE*/ java_out = IsaToJava.get_asms_out(xml_out);
701 /*PIDE*/ return_val = java_out.getAssumptions();
702 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
704 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
705 /*---------------------------------------------------------------------------*/
709 /** MATH_ENGINE: val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree */
710 public Vector<CalcFormula> getFormulaeFromTo(int id, ICalcIterator iterator_from,
711 ICalcIterator iterator_to, Integer level, boolean result_includes_tactics) {
712 XML.Tree xml_in = null;
713 Vector<CalcFormula> return_val = null;
714 /*---------------------------------------------------------------------------*/
715 //*TTY*/try { wrapper = interpretSML(id, "getFormulaeFromTo @calcid@ "
716 //*TTY*/ + iterator_from.toSMLString() + " " + iterator_to.toSMLString()
717 //*TTY*/ + " " + level + " " + result_includes_tactics + ";", false);
718 //*TTY*/} catch (RemoteException e) { e.printStackTrace(); }
719 //*TTY*/if (wrapper == null) return null;
720 //*TTY*/FormHeadsContainer con = (FormHeadsContainer) wrapper.getResponse();
721 //*TTY*/if (con != null) return_val = con.getElements();
722 //*TTY*/else return_val = null;
723 /*---------------------------------------------------------------------------*/
724 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
726 /*PIDE*/ bridge_.log(1, "-->ISA: " + "getFormulaeFromTo " + sml_id + " "
727 /*PIDE*/ + iterator_from.toSMLString() + " " + iterator_to.toSMLString()
728 /*PIDE*/ + " " + level + " " + result_includes_tactics + ";");
729 /*PIDE*/} catch (RemoteException e2) { e2.printStackTrace(); }
732 /*PIDE*/ xml_in = JavaToIsa.get_formulae(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
733 /*PIDE*/ iterator_from.getPosition(), iterator_to.getPosition(),
734 /*PIDE*/ new scala.math.BigInt(BigInteger.valueOf(level)), result_includes_tactics);
735 /*PIDE*/} catch (RemoteException e1) { e1.printStackTrace(); }
736 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
737 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.GET_FORMULAE, xml_in);
739 /*PIDE*/IntFormulas java_out = null;
740 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
741 /*PIDE*/ java_out = IsaToJava.get_formulae_out(xml_out);
742 /*PIDE*/ return_val = java_out.getCalcFormulas();
743 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
745 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
746 /*---------------------------------------------------------------------------*/
751 * @see isac.bridge.IBridgeRMI#getTactic(int, int)
753 * MATH_ENGINE: val getTactic : calcID -> pos' -> XML.tree
755 public Tactic getTactic(int calcTreeID, Position pos) throws RemoteException {
756 Tactic return_val = null;
757 /*---------------------------------------------------------------------------*/
758 //*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,
759 //*TTY*/ "getTactic @calcid@ " + pos.toSMLString() + ";", false);
760 //*TTY*/return_val = (Tactic) wrapper.getResponse();
761 /*---------------------------------------------------------------------------*/
762 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));
763 /*PIDE*/bridge_.log(1, "-->ISA: " + "getTactic " + sml_id + " " + pos.toSMLString() + ";");
765 /*PIDE*/XML.Tree xml_in = JavaToIsa.get_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);
766 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
767 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.GET_TAC, xml_in);
769 /*PIDE*/IntTactic java_out = null;
770 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
771 /*PIDE*/ java_out = IsaToJava.get_tac_out(xml_out);
772 /*PIDE*/ return_val = java_out.getTactic();
773 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
775 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
776 /*---------------------------------------------------------------------------*/
780 /** MATH_ENGINE: val initContext : calcID -> ketype -> pos' -> XML.tree
782 * This method is implemented in Isabelle/Isac, but seems to never have been completed in Java.
783 * See isac.bridge.TestContext#testContext.
785 public Context initContext(int javaCalcID, ContextType type, Position pos) throws RemoteException {
786 Context return_val = null;
787 /*---------------------------------------------------------------------------*/
788 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
789 //*TTY*/ "initContext @calcid@ " + type.toSMLString() + " " + pos.toSMLString() + ";", false);
790 //*TTY*/if(wrapper == null) return null;
791 //*TTY*/return_val = (Context) wrapper.getResponse();
792 /*---------------------------------------------------------------------------*/
793 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
794 /*PIDE*/bridge_.log(1, "-->ISA: " + "initContext " + sml_id + " " + type.toSMLString() + " " + pos.toSMLString() + ";");
796 /*PIDE*/XML.Tree xml_in = JavaToIsa.init_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)), type, pos);
797 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
798 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.INIT_CTXT, xml_in);
800 /*PIDE*/Context java_out = null; // front-end later distinguishes ContextTheory, ContextProblem, ..
801 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
802 /*PIDE*/ java_out = (Context) IsaToJava.init_ctxt_out(xml_out);
803 /*PIDE*/ return_val = java_out;
804 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
806 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
807 /*---------------------------------------------------------------------------*/
811 /** MATH_ENGINE: val inputFillFormula: calcID -> string -> XML.tree
812 * only implemented in Math_Engine */
814 /** MATH_ENGINE: val interSteps : calcID -> pos' -> XML.tree */
815 public CEvent intermediateSteps(int id, ICalcIterator ci) {
816 CEvent return_val = null;
817 /*---------------------------------------------------------------------------*/
818 //*TTY*/ResponseWrapper wrapper = null;
820 //*TTY*/ wrapper = interpretSML(id, "interSteps @calcid@ " + ci.toSMLString() + ";", false);
821 //*TTY*/} catch (RemoteException e) { e.printStackTrace(); }
822 //*TTY*/if (wrapper == null) return null;
823 //*TTY*/return_val = (CEvent) wrapper.getResponse();
824 /*---------------------------------------------------------------------------*/
825 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
826 /*PIDE*/XML.Tree xml_in = null;
828 /*PIDE*/ bridge_.log(1, "-->ISA: " + "interSteps " + sml_id + " " + ci.toSMLString() + ";");
829 /*PIDE*/} catch (RemoteException e1) { e1.printStackTrace(); }
832 /*PIDE*/ xml_in = JavaToIsa.inter_steps(new scala.math.BigInt(BigInteger.valueOf(sml_id)), ci.getPosition());
833 /*PIDE*/} catch (Exception e1) { e1.printStackTrace();}
834 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
835 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.INTER_STEPS, xml_in);
837 /*PIDE*/IntCEvent java_out = null;
838 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
839 /*PIDE*/ java_out = IsaToJava.inter_steps_out(xml_out);
840 /*PIDE*/ return_val = java_out.getCEvent();
841 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
843 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
844 /*---------------------------------------------------------------------------*/
848 /** MATH_ENGINE: val Iterator : calcID -> XML.tree */
849 public int iterator(int id) {
850 if (logger.isDebugEnabled())
851 logger.debug("iterator: id=" + id);
852 int return_val = 4711;
853 /*---------------------------------------------------------------------------*/
854 //*TTY*/if (id == 1) {
855 //*TTY*/ ResponseWrapper wrapper = interpretSML(id, "Iterator @calcid@;", false);
856 //*TTY*/ if (wrapper == null) return_val = -1;
857 //*TTY*/ else return_val = Integer.parseInt(((CalcHeadSimpleID) wrapper .getResponse()).getID());
858 //*TTY*/} else return_val = 4711;//TODO.WN041208 drop CalcIterator.iteratorID_
859 /*---------------------------------------------------------------------------*/
860 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
861 /*PIDE*/bridge_.log(1, "-->ISA: " + "Iterator " + sml_id + ";");
863 /*PIDE*/BigInt xml_in = new scala.math.BigInt(BigInteger.valueOf(sml_id));
864 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
865 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.ITERATOR, xml_in);
867 /*PIDE*/IntIntCompound java_out = null;
868 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
869 /*PIDE*/ java_out = IsaToJava.iterator_out(xml_out);
870 /*PIDE*/ return_val = java_out.getCalcId().intValue();
871 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
873 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
874 /*---------------------------------------------------------------------------*/
879 * @see isac.interfaces.IToCalc#modelProblem()
881 * MATH_ENGINE: val modelProblem : calcID -> XML.tree
883 public CalcHead modelProblem(int calc_tree_id) throws RemoteException {
884 CalcHead return_val = null;
885 /*---------------------------------------------------------------------------*/
886 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id, "modelProblem @calcid@;", false);
887 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
888 /*---------------------------------------------------------------------------*/
889 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
890 /*PIDE*/bridge_.log(1, "-->ISA: " + "modelProblem " + sml_id + ";");
892 /*PIDE*/BigInt xml_in = new scala.math.BigInt(BigInteger.valueOf(sml_id));
893 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
894 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.MODEL_PBL, xml_in);
896 /*PIDE*/IntCalcHead java_out = null;
897 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
898 /*PIDE*/ java_out = IsaToJava.modify_calchead_out(xml_out);
899 /*PIDE*/ return_val = java_out.getCalcHead();
900 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
902 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
903 /*---------------------------------------------------------------------------*/
908 * @see isac.interfaces.IToCalc#checkCalcHead(isac.util.formulae.CalcHead)
910 * MATH_ENGINE: val modifyCalcHead : calcID -> icalhd -> XML.tree
912 public CalcHead checkCalcHead(int calc_tree_id, CalcHead calchead) throws RemoteException {
913 CalcHead return_val = null;
914 /*---------------------------------------------------------------------------*/
915 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
916 //*TTY*/ "modifyCalcHead @calcid@ " + calchead.toSMLString() + ";", false);
917 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
918 /*---------------------------------------------------------------------------*/
919 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
920 /*PIDE*/bridge_.log(1, "-->ISA: " + "modelProblem " + sml_id + ";");
922 /*PIDE*/XML.Tree xml_in = JavaToIsa.modify_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)), calchead);
923 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
924 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.MODIFY_CALCHEAD, xml_in);
926 /*PIDE*/IntCalcHead java_out = null;
927 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
928 /*PIDE*/ java_out = IsaToJava.modify_calchead_out(xml_out);
929 /*PIDE*/ return_val = java_out.getCalcHead();
930 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
932 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
933 /*---------------------------------------------------------------------------*/
937 /** MATH_ENGINE: val moveActiveCalcHead : calcID -> XML.tree */
938 public Position moveCalcHead(int javaCalcID, int iteratorID, Position p) {
939 Position return_val = null;
940 /*---------------------------------------------------------------------------*/
941 //*TTY*/ResponseWrapper wrapper = null;
942 //*TTY*/if (iteratorID == 1)
943 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveActiveCalcHead @calcid@" + ";", false);
945 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveCalcHead @calcid@ " + " " + p.toSMLString() + ";", false);
946 //*TTY*/return_val = moveSuccess(wrapper);
947 /*---------------------------------------------------------------------------*/
948 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
949 /*PIDE*/XML.Tree xml_in = null;
950 /*PIDE*/XML.Tree xml_out = null;
952 /*PIDE*/if (iteratorID == 1) {
953 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveCalcHead " + sml_id + "" + ";");
954 /*PIDE*/xml_in = JavaToIsa.move_active_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
955 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
956 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_FORM, xml_in);
958 /*PIDE*/IntPosition java_out = null;
959 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
960 /*PIDE*/ java_out = IsaToJava.move_active_calchead_out(xml_out);
961 /*PIDE*/ return_val = java_out.getPosition();
962 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
964 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
968 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveCalcHead " + sml_id + " " + " " + p.toSMLString() + ";");
969 /*PIDE*/xml_in = JavaToIsa.move_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)), null);
970 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
971 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_FORM, xml_in);
973 /*PIDE*/IntPosition java_out = null;
974 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
975 /*PIDE*/ java_out = IsaToJava.move_calchead_out(xml_out);
976 /*PIDE*/ return_val = java_out.getPosition();
977 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
979 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
981 /*---------------------------------------------------------------------------*/
985 /** MATH_ENGINE: val moveActiveDown : calcID -> XML.tree */
986 public Position moveDown(int javaCalcID, int iteratorID, Position p) {
987 if (logger.isDebugEnabled())
988 logger.debug("moveDown: javaCalcID=" + javaCalcID + ", sml_pos=" + p.toSMLString());
989 Position return_val = null;
990 /*---------------------------------------------------------------------------*/
991 //*TTY*/ResponseWrapper wrapper = null;
992 //*TTY*/if (iteratorID == 1)
993 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveActiveDown @calcid@" + ";", false);
995 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveDown @calcid@ " + p.toSMLString() + ";", false);
996 //*TTY*/return_val = moveSuccess(wrapper);
997 /*---------------------------------------------------------------------------*/
998 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
999 /*PIDE*/XML.Tree xml_in = null;
1000 /*PIDE*/XML.Tree xml_out = null;
1002 /*PIDE*/if (iteratorID == 1) {
1003 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveDown " + sml_id + "" + ";");
1004 /*PIDE*/xml_in = JavaToIsa.move_active_down(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1005 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1006 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_DOWN, xml_in);
1008 /*PIDE*/IntPosition java_out = null;
1009 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1010 /*PIDE*/ java_out = IsaToJava.move_active_down_out(xml_out);
1011 /*PIDE*/ return_val = java_out.getPosition();
1012 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1014 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1018 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveDown " + sml_id + " " + p.toSMLString() + ";");
1019 /*PIDE*/xml_in = JavaToIsa.move_down(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);
1020 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1021 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_DOWN, xml_in);
1023 /*PIDE*/IntPosition java_out = null;
1024 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1025 /*PIDE*/ java_out = IsaToJava.move_down_out(xml_out);
1026 /*PIDE*/ return_val = java_out.getPosition();
1027 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1029 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1031 /*---------------------------------------------------------------------------*/
1036 * returns Position for uniformity with move*; not required elsewhere
1038 * MATH_ENGINE: val moveActiveFormula : calcID -> pos' -> XML.tree
1040 public Position moveActiveFormula(int javaCalcID, Position p) {
1041 if (logger.isDebugEnabled())
1042 logger.debug("moveDown: javaCalcID=" + javaCalcID + ", sml_pos=" + p.toSMLString());
1043 Position return_val = null;
1044 /*---------------------------------------------------------------------------*/
1045 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
1046 //*TTY*/ "moveActiveFormula @calcid@ " + p.toSMLString() + ";", false);
1047 //*TTY*/return_val = moveSuccess(wrapper);
1048 /*---------------------------------------------------------------------------*/
1049 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1050 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveFormula " + sml_id + " " + p.toSMLString() + ";");
1052 /*PIDE*/XML.Tree xml_in = JavaToIsa.move_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);
1053 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1054 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_FORM, xml_in);
1056 /*PIDE*/IntPosition java_out = null;
1057 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1058 /*PIDE*/ java_out = IsaToJava.move_active_form_out(xml_out);
1059 /*PIDE*/ return_val = java_out.getPosition();
1060 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1062 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1063 /*---------------------------------------------------------------------------*/
1067 /** MATH_ENGINE: val moveActiveLevelDown : calcID -> XML.tree */
1068 public Position moveLevelDown(int javaCalcID, int iteratorID, Position p) {
1069 Position return_val = null;
1070 /*---------------------------------------------------------------------------*/
1071 //*TTY*/ResponseWrapper wrapper = null;
1072 //*TTY*/if (iteratorID == 1)
1073 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveActiveLevelDown @calcid@" + ";", false);
1075 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveLevelDown @calcid@ " + " " + p.toSMLString() + ";", false);
1076 //*TTY*/return_val = moveSuccess(wrapper);
1077 /*---------------------------------------------------------------------------*/
1078 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1079 /*PIDE*/XML.Tree xml_in = null;
1080 /*PIDE*/XML.Tree xml_out = null;
1082 /*PIDE*/if (iteratorID == 1) {
1083 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveLevelDown " + sml_id + "" + ";");
1084 /*PIDE*/xml_in = JavaToIsa.move_active_levdown(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1085 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1086 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_LEVDN, xml_in);
1088 /*PIDE*/IntPosition java_out = null;
1089 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1090 /*PIDE*/ java_out = IsaToJava.move_active_levdown_out(xml_out);
1091 /*PIDE*/ return_val = java_out.getPosition();
1092 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1094 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1098 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveLevelDown " + sml_id + " " + " " + p.toSMLString() + ";");
1099 /*PIDE*/xml_in = JavaToIsa.move_levdn(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);
1100 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1101 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_LEVDN, xml_in);
1103 /*PIDE*/IntPosition java_out = null;
1104 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1105 /*PIDE*/ java_out = IsaToJava.move_levdn_out(xml_out);
1106 /*PIDE*/ return_val = java_out.getPosition();
1107 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1109 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1111 /*---------------------------------------------------------------------------*/
1115 /** MATH_ENGINE: val moveActiveLevelUp : calcID -> XML.tree */
1116 public Position moveLevelUp(int javaCalcID, int iteratorID, Position p) {
1117 Position return_val = null;
1118 /*---------------------------------------------------------------------------*/
1119 //*TTY*/ResponseWrapper wrapper = null;
1120 //*TTY*/if (iteratorID == 1)
1121 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveActiveLevelUp @calcid@" + ";", false);
1123 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveLevelUp @calcid@ " + p.toSMLString() + ";", false);
1124 //*TTY*/return_val = moveSuccess(wrapper);
1125 /*---------------------------------------------------------------------------*/
1126 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1127 /*PIDE*/XML.Tree xml_in = null;
1128 /*PIDE*/XML.Tree xml_out = null;
1130 /*PIDE*/if (iteratorID == 1) {
1131 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveLevelUp " + sml_id + "" + ";");
1132 /*PIDE*/xml_in = JavaToIsa.move_active_levup(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1133 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1134 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_LEVUP, xml_in);
1135 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_FORM, xml_in);
1137 /*PIDE*/IntPosition java_out = null;
1138 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1139 /*PIDE*/ java_out = IsaToJava.move_active_levup_out(xml_out);
1140 /*PIDE*/ return_val = java_out.getPosition();
1141 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1143 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1147 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveLevelUp " + sml_id + " " + p.toSMLString() + ";");
1148 /*PIDE*/xml_in = JavaToIsa.move_levup(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);
1149 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1150 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_LEVUP, xml_in);
1152 /*PIDE*/IntPosition java_out = null;
1153 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1154 /*PIDE*/ java_out = IsaToJava.move_levup_out(xml_out);
1155 /*PIDE*/ return_val = java_out.getPosition();
1156 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1158 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1160 /*---------------------------------------------------------------------------*/
1164 /** MATH_ENGINE: val moveActiveRoot : calcID -> XML.tree */
1165 public Position moveRoot(int javaCalcID, int iteratorID) {
1166 if (logger.isDebugEnabled())
1167 logger.debug("moveRoot: javaCalcID=" + javaCalcID);
1168 Position return_val = null;
1169 /*---------------------------------------------------------------------------*/
1170 //*TTY*/ResponseWrapper wrapper = null;
1171 //*TTY*/if (iteratorID == 1)
1172 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveActiveRoot @calcid@" + ";", false);
1174 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveRoot @calcid@ " + ";", false);
1175 //*TTY*/return_val = moveSuccess(wrapper);
1176 /*---------------------------------------------------------------------------*/
1177 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1178 /*PIDE*/scala.math.BigInt xml_in = null;
1179 /*PIDE*/XML.Tree xml_out = null;
1181 /*PIDE*/if (iteratorID == 1) {
1182 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveActiveRoot " + sml_id + "" + ";");
1183 /*PIDE*/xml_in = new scala.math.BigInt(BigInteger.valueOf(sml_id));
1184 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1185 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_ROOT, xml_in);
1187 /*PIDE*/IntPosition java_out = null;
1188 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1189 /*PIDE*/ java_out = IsaToJava.move_active_root_out(xml_out);
1190 /*PIDE*/ return_val = java_out.getPosition();
1191 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1193 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1197 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveRoot " + sml_id + " " + ";");
1198 /*PIDE*/XML.Tree xml_in2 = JavaToIsa.move_root(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1199 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in2);
1200 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ROOT, xml_in2);
1202 /*PIDE*/IntPosition java_out = null;
1203 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1204 /*PIDE*/ java_out = IsaToJava.move_root_out(xml_out);
1205 /*PIDE*/ return_val = java_out.getPosition();
1206 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1208 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1210 /*---------------------------------------------------------------------------*/
1214 /** MATH_ENGINE: val moveActiveRootTEST : calcID -> XML.tree
1215 * used only internally in Math_Engine */
1217 /** MATH_ENGINE: val moveActiveUp : calcID -> XML.tree */
1218 public Position moveUp(int javaCalcID, int iteratorID, Position p) {
1219 Position return_val = null;
1220 /*---------------------------------------------------------------------------*/
1221 //*TTY*/ResponseWrapper wrapper = null;
1222 //*TTY*/if (iteratorID == 1)
1223 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveActiveUp @calcid@" + ";", false);
1225 //*TTY*/ wrapper = interpretSML(javaCalcID, "moveUp @calcid@ " + p.toSMLString() + ";", false);
1226 //*TTY*/return_val = moveSuccess(wrapper);
1227 /*---------------------------------------------------------------------------*/
1228 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1229 /*PIDE*/XML.Tree xml_in = null;
1230 /*PIDE*/XML.Tree xml_out = null;
1232 /*PIDE*/if (iteratorID == 1) {
1233 /*PIDE*/xml_in = JavaToIsa.move_active_up(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1234 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1235 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_ACTIVE_UP, xml_in);
1237 /*PIDE*/IntPosition java_out = null;
1238 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1239 /*PIDE*/ java_out = IsaToJava.move_active_calchead_out(xml_out);
1240 /*PIDE*/ return_val = java_out.getPosition();
1241 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1243 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1247 /*PIDE*/bridge_.log(1, "-->ISA: " + "moveUp " + sml_id + " " + p.toSMLString() + ";");
1248 /*PIDE*/xml_in = JavaToIsa.move_up(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);
1249 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1250 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.MOVE_UP, xml_in);
1252 /*PIDE*/IntPosition java_out = null;
1253 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1254 /*PIDE*/ java_out = IsaToJava.move_calchead_out(xml_out);
1255 /*PIDE*/ return_val = java_out.getPosition();
1256 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1258 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1260 /*---------------------------------------------------------------------------*/
1264 // /----- these methods are designed for a visitor of the CalcTree ------------\
1265 // (with a iteratorID > 1), e.g. a teacher watching the student.
1266 /** MATH_ENGINE: val moveCalcHead : calcID -> pos' -> XML.tree
1267 * does not exist in isac-java, see val moveActiveCalcHead */
1269 /** MATH_ENGINE: val moveDown : calcID -> pos' -> XML.tree
1270 * does not exist in isac-java, see val moveActiveDown */
1272 /** MATH_ENGINE: val val moveLevelDown : calcID -> pos' -> XML.tree
1273 * does not exist in isac-java, see val moveActiveLevelDown */
1275 /** MATH_ENGINE: val moveLevelUp : calcID -> pos' -> XML.tree
1276 * does not exist in isac-java, see val moveActiveLevelUp */
1278 /** MATH_ENGINE: val moveRoot : calcID -> XML.tree
1279 * does not exist in isac-java, see val moveActiveRoot */
1281 /** MATH_ENGINE: val moveUp : calcID -> pos' -> XML.tree
1282 * does not exist in isac-java, see val moveActiveUp */
1283 // \----- these methods are designed for a visitor of the CalcTree ------------/
1286 * @see isac.bridge.IBridgeRMI#getElement(int, int)
1287 * MATH_ENGINE: val refFormula : calcID -> pos' -> XML.tree
1289 public ICalcElement getElement(int javaCalcID, Position p) {
1290 ICalcElement return_val = null;
1291 /*---------------------------------------------------------------------------*/
1292 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
1293 //*TTY*/ "(*getElement*)refFormula @calcid@ " + p.toSMLString() + ";", false);
1294 //*TTY*/if (wrapper == null) return_val = null;
1295 //*TTY*/return_val = (ICalcElement) wrapper.getResponse();
1296 /*---------------------------------------------------------------------------*/
1297 /*PIDE*/int sml_calcid = ((Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID))).intValue();
1298 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*getElement*)refFormula " + sml_calcid
1299 /*PIDE*/ + " " + p.toSMLString() + ";");
1301 /*PIDE*/XML.Tree xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_calcid)), p);
1302 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1303 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.REF_FORMULA, xml_in);
1305 /*PIDE*/IntFormHead java_out = null;
1306 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1307 /*PIDE*/ java_out = IsaToJava.ref_formula_out(xml_out);
1308 /*PIDE*/ return_val = (ICalcElement)java_out.getFormHead();
1309 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1311 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1312 /*---------------------------------------------------------------------------*/
1317 * @see isac.bridge.IBridgeRMI#getFormula(int, int)
1318 * @deprecated in favour of getElement.
1319 * ... WN150812: never used although it is in IBridgeRMI !!
1321 * MATH_ENGINE: val refFormula : calcID -> pos' -> XML.tree
1323 public ICalcElement getFormula(int calcTreeID, Position p) throws RemoteException {
1324 ICalcElement return_val = null;
1325 /*---------------------------------------------------------------------------*/
1326 //*TTY*/ResponseWrapper wrapper = interpretSML(calcTreeID,
1327 //*TTY*/ "(*getFormula*)refFormula @calcid@ " + p.toSMLString() + ";", false);
1328 //*TTY*/if (wrapper == null) return_val = null;
1329 //*TTY*/else return_val = (ICalcElement) wrapper.getResponse();
1330 /*---------------------------------------------------------------------------*/
1331 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calcTreeID));
1332 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*getFormula*)refFormula " + sml_id + " " + p.toSMLString() + ";");
1334 /*PIDE*/XML.Tree xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), p);
1335 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1336 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.REF_FORMULA, xml_in);
1338 /*PIDE*/IntFormHead java_out = null;
1339 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1340 /*PIDE*/ java_out = IsaToJava.ref_formula_out(xml_out);
1341 /*PIDE*/ return_val = (ICalcElement)java_out.getFormHead();
1342 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1344 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1345 /*---------------------------------------------------------------------------*/
1349 /** MATH_ENGINE: val refineProblem : calcID -> pos' -> guh -> XML.tree
1350 * see notes WN150824 */
1351 public Context refineProblem(int javaCalcID, Context context, Position pos) throws RemoteException {
1352 Context return_val = null;
1353 /*---------------------------------------------------------------------------*/
1354 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
1355 //*TTY*/ "refineProblem @calcid@ " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";", false);
1356 //*TTY*/if(wrapper == null) return null;
1357 //*TTY*/return_val = (Context) wrapper.getResponse();
1358 /*---------------------------------------------------------------------------*/
1359 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1360 /*PIDE*/bridge_.log(1, "-->ISA: " + "refineProblem " + sml_id + " " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";");
1362 /*PIDE*/XML.Tree xml_in = JavaToIsa.refine_pbl(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
1363 /*PIDE*/ pos, context.getKEStoreKey().toString() + "\"");
1364 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1365 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.REFINE_PBL, xml_in);
1367 /*PIDE*/IntContext java_out = null;
1368 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1369 /*PIDE*/ java_out = IsaToJava.refine_pbl_out(xml_out);
1370 /*PIDE*/ return_val = java_out.getContext();
1371 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1373 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1374 /*---------------------------------------------------------------------------*/
1378 /** MATH_ENGINE: val replaceFormula : calcID -> cterm' -> XML.tree */
1379 public CEvent replaceFormula(int id, CalcFormula f) {
1380 CEvent return_val = null;
1381 /*---------------------------------------------------------------------------*/
1382 //*TTY*/ResponseWrapper wrapper = null;
1383 //*TTY*/wrapper = interpretSML(id, "replaceFormula @calcid@ \"" + f.toSMLString() + "\";", false);
1384 //*TTY*/if (wrapper == null) return_val = null;
1385 //*TTY*/else return_val = (CEvent) wrapper.getResponse();
1386 /*---------------------------------------------------------------------------*/
1387 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
1388 /*PIDE*/bridge_.log(1, "-->ISA: " + "replaceFormula " + sml_id + " \"" + f.toSMLString() + "\";");
1390 /*PIDE*/XML.Tree xml_in = JavaToIsa.replace_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)), f.getFormula());
1391 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1392 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.REPLACE_FORM, xml_in);
1394 /*PIDE*/IntCEvent java_out = null;
1395 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1396 /*PIDE*/ java_out = IsaToJava.replace_form_out(xml_out);
1397 /*PIDE*/ return_val = java_out.getCEvent();
1398 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1400 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1401 /*---------------------------------------------------------------------------*/
1405 /** MATH_ENGINE: val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
1406 * only implemented in Math_Engine */
1408 /** MATH_ENGINE: val resetCalcHead : calcID -> XML.tree */
1410 * @see isac.interfaces.IToCalc#resetCalcHead()
1412 public CalcHead resetCalcHead(int calc_tree_id) throws RemoteException {
1413 CalcHead return_val = null;
1414 /*---------------------------------------------------------------------------*/
1415 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id, "resetCalcHead @calcid@;", false);
1416 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1417 /*---------------------------------------------------------------------------*/
1418 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1419 /*PIDE*/bridge_.log(1, "-->ISA: " + "resetCalcHead " + sml_id + ";");
1421 /*PIDE*/XML.Tree xml_in = JavaToIsa.reset_calchead(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1422 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1423 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.RESET_CALCHEAD, xml_in);
1425 /*PIDE*/IntCalcHead java_out = null;
1426 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1427 /*PIDE*/ java_out = IsaToJava.reset_calchead_out(xml_out);
1428 /*PIDE*/ return_val = java_out.getCalcHead();
1429 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1431 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1432 /*---------------------------------------------------------------------------*/
1436 /** MATH_ENGINE: val setContext : calcID -> pos' -> guh -> XML.tree */
1437 /* The status of this method is unclear:
1439 ** There is no use-case and no test
1440 ** The code is NOT used when showing the contexts
1441 * of thy, pbl, met, exp for example Biegelinie.
1442 ** The code is not deleted, nevertheless, because there is
1443 * code in isabisac: interface#setContext
1445 * So the changes for "isabelle tty" --> libisabelle adapt to the XML
1446 * sent from isabisac interface#setContext > autocalculateOK2xml.
1448 public CChanged setContext(int javaCalcID, ContextTheory context, Position pos ) throws RemoteException {
1449 CChanged return_val = null;
1450 /*---------------------------------------------------------------------------*/
1451 //*TTY*/ResponseWrapper wrapper = interpretSML(javaCalcID,
1452 //*TTY*/ "setContext @calcid@ " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";", false);
1453 //*TTY*/if(wrapper == null) return_val = null;
1454 //*TTY*/else return_val = (CChanged) wrapper.getResponse();
1455 /*---------------------------------------------------------------------------*/
1456 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(javaCalcID));
1457 /*PIDE*/bridge_.log(1, "-->ISA: " + "setContext " + sml_id + " " + pos.toSMLString() + " \"" + context.getKEStoreKey().toString() + "\";");
1459 /*PIDE*/XML.Tree xml_in = JavaToIsa.set_ctxt(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
1460 /*PIDE*/ pos, context.getKEStoreKey().toString() + "\"");
1461 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1462 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.SET_CTXT, xml_in);
1464 /*PIDE*/IntCEvent java_out = null;
1465 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1466 /*PIDE*/ java_out = IsaToJava.set_ctxt_out(xml_out);
1467 /*PIDE*/ return_val = (CChanged) java_out.getCEvent();
1468 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1470 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1471 /*---------------------------------------------------------------------------*/
1476 * @see isac.interfaces.IToCalc#setMethod()
1478 * MATH_ENGINE: val setMethod : calcID -> metID -> XML.tree
1480 public CalcHead setMethod(int calc_tree_id, MethodID id) throws RemoteException {
1481 CalcHead return_val = null;
1482 /*---------------------------------------------------------------------------*/
1483 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
1484 //*TTY*/ "setMethod @calcid@ " + id.toSMLString() + ";", false);
1485 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1486 /*---------------------------------------------------------------------------*/
1487 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1488 /*PIDE*/bridge_.log(1, "-->ISA: " + "setMethod " + sml_id + " " + id.toSMLString() + ";");
1490 /*PIDE*/XML.Tree xml_in = JavaToIsa.set_met(new scala.math.BigInt(BigInteger.valueOf(sml_id)), id.getID());
1491 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1492 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.SET_MET, xml_in);
1494 /*PIDE*/IntCalcHead java_out = null;
1495 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1496 /*PIDE*/ java_out = IsaToJava.set_met_out(xml_out);
1497 /*PIDE*/ return_val = java_out.getCalcHead();
1498 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1500 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1501 /*---------------------------------------------------------------------------*/
1505 /** MATH_ENGINE: val setNextTactic : calcID -> tac -> XML.tree */
1506 public int setNextTactic(int id, Tactic tactic) {
1507 int return_val = 4711;
1508 /*---------------------------------------------------------------------------*/
1509 //*TTY*/ResponseWrapper wrapper = interpretSML(id,
1510 //*TTY*/ "setNextTactic @calcid@ (" + tactic.toSMLString() + ");", false);
1511 //*TTY*/if (wrapper == null) return_val = -1;//WN050223 response ... MESSAGE not parsed
1512 //*TTY*/if (wrapper.getResponse() == null) { return_val = 0; //Everything is ok
1513 //*TTY*/} else { return_val = -1; } //An Error occcured
1514 /*---------------------------------------------------------------------------*/
1515 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(id));
1516 /*PIDE*/bridge_.log(1, "-->ISA: " + "setNextTactic " + sml_id + " (" + tactic.toSMLString() + ");");
1518 /*PIDE*/XML.Tree xml_in = JavaToIsa.set_next_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), tactic);
1519 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1520 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.SET_NEXT_TAC, xml_in);
1522 /*PIDE*/if (!IsaToJava.is_syserror(xml_out)) {
1523 IsaToJava.set_next_tac_out(xml_out);
1524 /*PIDE*/ return_val = 0; //Everything is ok
1525 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1527 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_syserror: " + xml_out);
1529 /*---------------------------------------------------------------------------*/
1534 * @see isac.interfaces.IToCalc#setProblem()
1536 * MATH_ENGINE: val setProblem : calcID -> pblID -> XML.tree
1538 public CalcHead setProblem(int calc_tree_id, ProblemID id) throws RemoteException {
1539 CalcHead return_val = null;
1540 /*---------------------------------------------------------------------------*/
1541 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
1542 //*TTY*/ "setProblem @calcid@ " + id.toSMLString() + ";", false);
1543 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1544 /*---------------------------------------------------------------------------*/
1545 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1546 /*PIDE*/bridge_.log(1, "-->ISA: " + "setProblem " + sml_id + " " + id.toSMLString() + ";");
1548 /*PIDE*/XML.Tree xml_in = JavaToIsa.set_met(new scala.math.BigInt(BigInteger.valueOf(sml_id)), id.getID());
1549 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1550 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.SET_PBL, xml_in);
1552 /*PIDE*/IntCalcHead java_out = null;
1553 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1554 /*PIDE*/ java_out = IsaToJava.set_met_out(xml_out);
1555 /*PIDE*/ return_val = java_out.getCalcHead();
1556 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1558 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1559 /*---------------------------------------------------------------------------*/
1564 * @see isac.interfaces.IToCalc#setTheory()
1566 * TODO/WN150812: use implementation in Math_Engine.
1567 * MATH_ENGINE: val setTheory : calcID -> thyID -> XML.tree
1569 public CalcHead setTheory(int calc_tree_id, String thy_id)
1570 throws RemoteException {
1571 CalcHead return_val = null;
1572 Position pos = null;
1573 /*---------------------------------------------------------------------------*/
1574 //*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1575 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
1576 //*TTY*/ "(*setTheory*)setNextTactic @calcid@ (Specify_Theory \"" + thy_id + "\");", false);
1577 //*TTY*/wrapper = interpretSML(calc_tree_id,
1578 //*TTY*/ "(*setTheory*)autoCalculate @calcid@ (Step 1);", false);
1579 //*TTY*///drop the CalcChanged returned by autoCalculate
1580 //*TTY*/wrapper = interpretSML(calc_tree_id,
1581 //*TTY*/ "(*setTheory*)getActiveFormula @calcid@ ;", false);
1582 //*TTY*/pos = moveSuccess(wrapper);
1583 //*TTY*/wrapper = interpretSML(calc_tree_id,
1584 //*TTY*/ "(*setTheory*)refFormula @calcid@ " + pos.toSMLString() + ";", false);
1585 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1587 /*---------------------------------------------------------------------------*/
1588 //---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1589 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1591 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)setNextTactic " + sml_id + " (Specify_Theory \"" + thy_id + "\");");
1592 /*PIDE*/SimpleTactic tac = new SimpleTactic("Specify_Theory", thy_id + "\"");
1593 /*PIDE*/XML.Tree xml_in = JavaToIsa.set_next_tac(new scala.math.BigInt(BigInteger.valueOf(sml_id)), tac);
1594 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1595 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.SET_NEXT_TAC, xml_in);
1596 /*PIDE*/bridge_.log(1, "<--ISA: message not sent to Dialog ... " + xml_out);
1598 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)autoCalculate " + sml_id + " (Step 1);");
1599 /*PIDE*/xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
1600 /*PIDE*/ "Step", new scala.math.BigInt(BigInteger.valueOf(1)));
1601 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1602 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.AUTO_CALC, xml_in);
1603 /*PIDE*/bridge_.log(1, "<--ISA: CalcChanged not sent to Dialog ... " + xml_out);
1605 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)getActiveFormula " + sml_id + ";");
1606 /*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1607 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ACTIVE_FORM, xml_in);
1608 /*PIDE*/IntPosition java_out = null;
1609 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1610 /*PIDE*/ java_out = IsaToJava.get_active_form_out(xml_out);
1611 /*PIDE*/ pos = java_out.getPosition();
1612 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1614 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1616 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*setTheory*)refFormula " + sml_id + " " + pos.toSMLString() + ";");
1617 /*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);//^^pos.setKind("DUMMY")
1618 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1619 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.REF_FORMULA, xml_in);
1621 /*PIDE*/IntFormHead java_out2 = null;
1622 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1623 /*PIDE*/ java_out2 = IsaToJava.ref_formula_out(xml_out);
1624 /*PIDE*/ return_val = (CalcHead)java_out2.getFormHead();
1625 /*PIDE*/bridge_.log(1, "<--ISA: " + xml_out);
1627 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1628 /*PIDE*///\---End hack
1629 /*---------------------------------------------------------------------------*/
1633 /***********************************************************************
1634 * Below are methods not contained in MATH_ENGINE, rather
1635 * they composed from other methods in Math_Engine.
1639 * @see isac.interfaces.IToCalc#completeCalcHead()
1641 public CalcHead completeCalcHead(int calc_tree_id) {
1642 CalcHead return_val = null;
1643 Position pos = null;
1644 /*---------------------------------------------------------------------------*/
1645 //*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1646 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
1647 //*TTY*/ "(*completeCalcHead*)autoCalculate @calcid@ CompleteCalcHead;", false);
1648 //*TTY*///drop the CalcChanged returned by autoCalculate
1649 //*TTY*/wrapper = interpretSML(calc_tree_id,
1650 //*TTY*/ "(*completeCalcHead*)getActiveFormula @calcid@ ;", false);
1651 //*TTY*/pos = moveSuccess(wrapper);
1652 //*TTY*/wrapper = interpretSML(calc_tree_id,
1653 //*TTY*/ "(*completeCalcHead*)refFormula @calcid@ " + pos.toSMLString() + ";", false);
1654 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1655 //*TTY*///\---End hack
1656 /*---------------------------------------------------------------------------*/
1657 //---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1658 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1660 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeCalcHead*)autoCalculate " + sml_id + "CompleteCalcHead;");
1661 /*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
1662 /*PIDE*/ "CompleteCalcHead", new scala.math.BigInt(BigInteger.valueOf(0)));
1663 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1664 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.AUTO_CALC, xml_in);
1666 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1667 IsaToJava.auto_calc_out(xml_out);
1668 /*PIDE*/// return_val = java_out.getCEvent();
1669 /*PIDE*/bridge_.log(1, "<--ISA: not sent to Dialog ... " + xml_out);
1671 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1674 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeCalcHead*)getActiveFormula " + sml_id + ";");
1675 /*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1676 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1677 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ACTIVE_FORM, xml_in);
1679 /*PIDE*/IntPosition java_out2 = null;
1680 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1681 /*PIDE*/ java_out2 = IsaToJava.get_active_form_out(xml_out);
1682 /*PIDE*/ pos = java_out2.getPosition();
1683 /*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);
1685 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1688 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeCalcHead*)refFormula " + sml_id + pos.toSMLString() + ";");
1689 /*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);
1690 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1691 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.REF_FORMULA, xml_in);
1693 /*PIDE*/IntFormHead java_out3 = null;
1694 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1695 /*PIDE*/ java_out3 = IsaToJava.ref_formula_out(xml_out);
1696 /*PIDE*/ return_val = (CalcHead)java_out3.getFormHead();
1697 /*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);
1699 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1700 /*PIDE*///\---End hack
1701 /*---------------------------------------------------------------------------*/
1706 * @see isac.interfaces.IToCalc#completeModel() WN050809 push this method
1707 * through to the SML-kernel
1709 public CalcHead completeModel(int calc_tree_id) throws RemoteException {
1710 CalcHead return_val = null;
1711 Position pos = null;
1712 /*---------------------------------------------------------------------------*/
1713 //*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1714 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
1715 //*TTY*/ "(*completeModel*)autoCalculate @calcid@ CompleteModel;", false);
1716 //*TTY*///drop the CalcChanged returned by autoCalculate
1717 //*TTY*/wrapper = interpretSML(calc_tree_id,
1718 //*TTY*/ "(*completeModel*)getActiveFormula @calcid@ ;", false);
1719 //*TTY*/pos = moveSuccess(wrapper);
1720 //*TTY*/wrapper = interpretSML(calc_tree_id,
1721 //*TTY*/ "(*completeModel*)refFormula @calcid@ " + pos.toSMLString() + ";", false);
1722 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1724 /*---------------------------------------------------------------------------*/
1725 //---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1726 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1728 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeModel*)autoCalculate " + sml_id + " CompleteModel;");
1729 /*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
1730 /*PIDE*/ "CompleteModel", new scala.math.BigInt(BigInteger.valueOf(0)));
1731 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1732 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.AUTO_CALC, xml_in);
1734 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1735 IsaToJava.set_met_out(xml_out);
1736 /*PIDE*/bridge_.log(1, "<--ISA: not sent to Dialog = " + xml_out);
1738 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1741 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeModel*)getActiveFormula " + sml_id + ";");
1742 /*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1743 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1744 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ACTIVE_FORM, xml_in);
1746 /*PIDE*/IntPosition java_out2 = null;
1747 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1748 /*PIDE*/ java_out2 = IsaToJava.get_active_form_out(xml_out);
1749 /*PIDE*/ pos = java_out2.getPosition();
1750 /*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);
1752 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1754 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*completeModel*)refFormula " + sml_id + " " + pos.toSMLString() + ";");
1755 /*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);
1756 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1757 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.REF_FORMULA, xml_in);
1759 /*PIDE*/IntFormHead java_out3 = null;
1760 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1761 /*PIDE*/ java_out3 = IsaToJava.ref_formula_out(xml_out);
1762 /*PIDE*/ return_val = (CalcHead)java_out3.getFormHead();
1763 /*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);
1765 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1766 /*PIDE*///\---End hack
1767 /*---------------------------------------------------------------------------*/
1772 * @see isac.interfaces.IToCalc#nextSpecify() WN050809 push this method
1773 * through to the SML-kernel.
1775 public CalcHead nextSpecify(int calc_tree_id) throws RemoteException {
1776 CalcHead return_val = null;
1777 Position pos = null;
1778 /*---------------------------------------------------------------------------*/
1779 //*TTY*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1780 //*TTY*/ResponseWrapper wrapper = interpretSML(calc_tree_id,
1781 //*TTY*/ "(*nextSpecify*)autoCalculate @calcid@ (Step 1);", false);
1782 //*TTY*///drop the CalcChanged returned by autoCalculate
1783 //*TTY*/wrapper = interpretSML(calc_tree_id,
1784 //*TTY*/ "(*nextSpecify*)getActiveFormula @calcid@ ;", false);
1785 //*TTY*/pos = moveSuccess(wrapper);
1786 //*TTY*/wrapper = interpretSML(calc_tree_id,
1787 //*TTY*/ "(*nextSpecify*)refFormula @calcid@ " + pos.toSMLString() + ";", false);
1788 //*TTY*/return_val = (CalcHead) wrapper.getResponse();
1789 //*TTY*///\---End hack
1790 /*---------------------------------------------------------------------------*/
1791 /*PIDE*/int sml_id = (Integer) java_calcid_to_smlcalcid_.get(new Integer(calc_tree_id));
1792 /*PIDE*///---FIXXXME.WN050809 hack until setTheory pushed into SML-kernel
1794 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*nextSpecify*)autoCalculate " + sml_id + " (Step 1);");
1795 /*PIDE*/XML.Tree xml_in = JavaToIsa.auto_calculate(new scala.math.BigInt(BigInteger.valueOf(sml_id)),
1796 /*PIDE*/ "Step", new scala.math.BigInt(BigInteger.valueOf(1)));
1797 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1798 /*PIDE*/XML.Tree xml_out = connection_to_kernel_.invoke(IsacOperations.AUTO_CALC, xml_in);
1800 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1801 IsaToJava.set_met_out(xml_out);
1802 /*PIDE*/bridge_.log(1, "<--ISA: not sent to Dialog = " + xml_out);
1804 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1807 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*nextSpecify*)getActiveFormula " + sml_id + ";");
1808 /*PIDE*/xml_in = JavaToIsa.get_active_form(new scala.math.BigInt(BigInteger.valueOf(sml_id)));
1809 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.GET_ACTIVE_FORM, xml_in);
1811 /*PIDE*/IntPosition java_out2 = null;
1812 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1813 /*PIDE*/ java_out2 = IsaToJava.get_active_form_out(xml_out);
1814 /*PIDE*/ pos = java_out2.getPosition();
1815 /*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);
1817 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1820 /*PIDE*/bridge_.log(1, "-->ISA: " + "(*nextSpecify*)refFormula " + sml_id + pos.toSMLString() + ";");
1821 /*PIDE*/xml_in = JavaToIsa.ref_formula(new scala.math.BigInt(BigInteger.valueOf(sml_id)), pos);//^^pos.setKind("DUMMY")
1822 /*PIDE*/bridge_.log(1, "-->ISA: " + xml_in);
1823 /*PIDE*/xml_out = connection_to_kernel_.invoke(IsacOperations.REF_FORMULA, xml_in);
1825 /*PIDE*/IntFormHead java_out3 = null;
1826 /*PIDE*/if (!IsaToJava.is_message(xml_out)) {
1827 /*PIDE*/ java_out3 = IsaToJava.ref_formula_out(xml_out);
1828 /*PIDE*/ return_val = (CalcHead)java_out3.getFormHead();
1829 /*PIDE*/bridge_.log(1, "<--ISA: used locally ... " + xml_out);
1831 /*PIDE*/ bridge_.log(1, "<--ISA: IsaToJava.is_message: " + xml_out);
1832 /*PIDE*///\---End hack
1833 /*---------------------------------------------------------------------------*/
1837 /***********************************************************************
1838 * Below are methods not implemented in MATH_ENGINE at all,
1839 * or only very fragmentarily.
1840 * WN150812 here are also methods, where the status is not clarified.
1841 * Some methods seem to be replaced by similar ones.
1842 * TODO: review IBridgeRMI, MathEngine, etc.
1846 * @see isac.interfaces.ICalcIterator#tryMatchMethod(MethodID)
1847 * @deprecated WN150812: not impl. in Math_Engine.
1849 public Match initMatchMethod(int javaCalcID) throws RemoteException {
1850 ResponseWrapper wrapper = interpretSML(javaCalcID,
1851 "initMatchMethod @calcid@ ;", false);
1852 Object response = wrapper.getResponse();
1853 CalcHead ch = (CalcHead) response;
1854 Match m = new Match(ch.getSpecification().getProblem(), ch
1855 .getStatusString(), ch.getHeadLine(), ch.getModel());
1860 * @see isac.interfaces.ICalcIterator#tryMatchProblem(HierarchyKey)
1861 * @deprecated WN150812: not impl. in Math_Engine.
1863 public Match initMatchProblem(int javaCalcID) {
1864 ResponseWrapper wrapper = interpretSML(javaCalcID,
1865 "initMatchProblem @calcid@ ;", false);
1866 Object response = wrapper.getResponse();
1867 CalcHead ch = (CalcHead) response;
1868 Match m = new Match(ch.getSpecification().getProblem(), ch
1869 .getStatusString(), ch.getHeadLine(), ch.getModel());
1874 * @deprecated in favour of getFormula
1875 * WN150812: but used frequently ?!
1877 public boolean moveFormula(int javaCalcID, int iteratorID) {
1878 interpretSML(javaCalcID,
1879 "moveFormula @calcid@ " + iteratorID + ";", false);
1880 return true;//WN041208 moveSuccess(wrapper);
1883 /** WN150812 unused ? */
1884 private Position moveSuccess(ResponseWrapper wrapper) {
1885 if (wrapper == null)
1888 Object r = wrapper.getResponse();
1889 if (r instanceof CMessage)
1890 return null;//TODO.WN041209 handle messages
1892 Position p = (Position) wrapper.getResponse();
1899 * @deprecated in favour of getTactic
1900 * WN150812: but used frequently ?!
1902 public boolean moveTactic(int javaCalcID, int iteratorID) {
1903 interpretSML(javaCalcID,
1904 "moveTactic @calcid@ " + iteratorID + ";", false);
1905 return true;//WN041208 moveSuccess(wrapper);
1909 * @see isac.interfaces.ICalcIterator#tryMatchMethod(MethodID)
1910 * @deprecated is not impl. in math-engine !!!
1912 public Match tryMatchMethod(int javaCalcID, MethodID keStoreID)
1913 throws RemoteException {
1914 ResponseWrapper wrapper = interpretSML(javaCalcID,
1915 "tryMatchMethod @calcid@ " + keStoreID.toSMLString() + ";",
1917 Object response = wrapper.getResponse();
1918 CalcHead ch = (CalcHead) response;
1919 Match m = new Match(ch.getSpecification().getProblem(), ch
1920 .getStatusString(), ch.getHeadLine(), ch.getModel());
1924 /** enforced by IBridgeRMI, WN150812: exp-, met-, pbl-, thy-contexts all work --
1925 * -- see: CChanged setContext(int, ContextTheory, ... */
1927 public CalcHead setContext(int javaCalcID, ContextMethod context, Position pos) throws RemoteException {
1931 /** enforced by IBridgeRMI, WN150812: exp-, met-, pbl-, thy-contexts all work --
1932 * -- see: CChanged setContext(int, ContextTheory, ...
1933 * This method changed role with ^^^^^^^^^^^^^^^^ during "isabelle tty" --> libisabelle
1936 public CalcHead setContext(int javaCalcID, ContextProblem context, Position pos) throws RemoteException {
1941 * @see isac.interfaces.ICalcIterator#tryMatchProblem(HierarchyKey)
1943 * WN150812: tryMatchProblem, trymatch only partially implemented in Math_Engine
1945 public Match tryMatchProblem(int javaCalcID, ProblemID problemID) {
1946 ResponseWrapper wrapper = interpretSML(javaCalcID,
1947 "tryMatchProblem @calcid@ " + problemID.toSMLString() + ";",
1949 Object response = wrapper.getResponse();
1950 CalcHead ch = (CalcHead) response;
1951 Match m = new Match(ch.getSpecification().getProblem(), ch
1952 .getStatusString(), ch.getHeadLine(), ch.getModel());
1957 * @see isac.interfaces.ICalcIterator#tryRefineProblem(HierarchyKey)
1958 * @deprecated in favour of refineProblem.
1960 public Match tryRefineProblem(int javaCalcID, ProblemID problemID) {
1961 ResponseWrapper wrapper = interpretSML(javaCalcID,
1962 "tryRefineProblem @calcid@ " + problemID.toSMLString() + ";",
1964 Object response = wrapper.getResponse();
1965 CalcHead ch = (CalcHead) response;
1966 Match m = new Match(ch.getSpecification().getProblem(), ch
1967 .getStatusString(), ch.getHeadLine(), ch.getModel());
1971 /***********************************************************************
1972 * Below are methods for restoring Isabelle/Isac after a crash.
1973 * This never worked, is to be deleted and
1974 * to be reconsidered with introduction of libisabelle.
1978 * This method is used when the kernel crashes and the CalcTrees need to be
1979 * entered again to the kernel to restore the previous state. The
1980 * Java-CalcIDs stay the same
1982 public void restoreExistingCalcTrees() {
1983 bridge_.log(1, "---- entering restoreExistingCalcTrees");
1984 Iterator<?> it = java_calcid_to_smlcalcid_.keySet().iterator();
1985 // keySet = javaCalcIDs
1988 while (it.hasNext()) {
1989 //bridge.log(1, "1");
1990 //int i = ((Integer)it.next()).intValue();
1991 javaCalcID = ((Integer) it.next()).intValue();
1992 //bridge.log(1, "2");
1993 v = saveCalcTree(javaCalcID);
1994 //bridge.log(1, "3");
1995 this.restoreToSML(javaCalcID, v);
1997 bridge_.log(1, "---- done restoreExistingCalcTrees");
2000 private void restoreToSML(int javaCalcID, Vector v) {
2001 Iterator<String> it = ((Vector) v.clone()).iterator();
2002 String s = (String) it.next();
2003 newCalculation(javaCalcID, s, null/*never worked*/, true);
2004 //javaCalcIDtoSmlCalcID.put(new Integer(javaCalcID), new
2005 // Integer(smlCalcID));
2006 //int smlID = ((Integer)javaCalcIDtoSmlCalcID.get(new
2007 // Integer(calcID))).intValue();
2008 while (it.hasNext()) {
2009 s = (String) it.next();
2010 interpretSML(javaCalcID, s, true);
2015 * Save a calcTree for later restoring (probably to another SML Kernel)
2018 * the ID of the calcTree
2019 * @return a vector containing strings. This is representatation of the
2020 * status of the calcTree
2022 @SuppressWarnings("unchecked")
2023 public Vector<String> saveCalcTree(int calcTreeID) {
2024 this.bridge_.log(1, "----------------begin saving calcTree "
2025 + calcTreeID + "------------");
2026 return (Vector<String>) inputs_.get(new Integer(calcTreeID));