|
wneuper@4848
|
1 |
package isac.bridge;
|
|
wneuper@4848
|
2 |
|
|
walther@5239
|
3 |
import edu.tum.cs.isabelle.*;
|
|
walther@5239
|
4 |
import edu.tum.cs.isabelle.api.XML;
|
|
wneuper@4848
|
5 |
|
|
wneuper@4848
|
6 |
public class IsacOperations {
|
|
wneuper@4848
|
7 |
// for Test_PIDE.java
|
|
wneuper@4848
|
8 |
public static final Operation<String, String> HELLO =
|
|
wneuper@4848
|
9 |
IsacOperationsScala.Hello();
|
|
wneuper@4848
|
10 |
|
|
wneuper@4848
|
11 |
public static final Operation<String, String> TESTSTR =
|
|
wneuper@4848
|
12 |
IsacOperationsScala.Teststr();
|
|
wneuper@4848
|
13 |
|
|
wneuper@4848
|
14 |
public static final Operation<scala.math.BigInt, XML.Tree> TESTIT =
|
|
wneuper@4848
|
15 |
IsacOperationsScala.Testit();
|
|
wneuper@4851
|
16 |
public static final Operation<XML.Tree, XML.Tree> TEST_TERM_TRANSFER =
|
|
wneuper@4851
|
17 |
IsacOperationsScala.TestTermTransfer();
|
|
wneuper@4853
|
18 |
public static final Operation<String, XML.Tree> TEST_TERM_ONE_WAY =
|
|
wneuper@4853
|
19 |
IsacOperationsScala.TestTermOneWay();
|
|
wneuper@4885
|
20 |
public static final Operation<String, XML.Tree> SCALATERM_OF_STRING =
|
|
wneuper@4885
|
21 |
IsacOperationsScala.ScalaTermOfString();
|
|
wneuper@4848
|
22 |
|
|
wneuper@4848
|
23 |
// Protoco.thy operation_setup for all isabisac's Math_Engine --------
|
|
wneuper@4848
|
24 |
public static final Operation<XML.Tree, XML.Tree> APPEND_FORM =
|
|
wneuper@4848
|
25 |
IsacOperationsScala.appendFormula();
|
|
wneuper@4848
|
26 |
public static final Operation<XML.Tree, XML.Tree> AUTO_CALC =
|
|
wneuper@4848
|
27 |
IsacOperationsScala.autoCalculate();
|
|
wneuper@4848
|
28 |
public static final Operation<XML.Tree, XML.Tree> APPLY_TAC =
|
|
wneuper@4848
|
29 |
IsacOperationsScala.applyTactic();
|
|
wneuper@4848
|
30 |
public static final Operation<XML.Tree, XML.Tree> CALC_TREE =
|
|
wneuper@4848
|
31 |
IsacOperationsScala.CalcTree();
|
|
wneuper@4848
|
32 |
public static final Operation<XML.Tree, XML.Tree> CHECK_CTXT =
|
|
wneuper@4848
|
33 |
IsacOperationsScala.checkContext();
|
|
wneuper@4848
|
34 |
public static final Operation<scala.math.BigInt, XML.Tree> DEL_CALC =
|
|
wneuper@4848
|
35 |
IsacOperationsScala.DEconstrCalcTree();
|
|
wneuper@4848
|
36 |
public static final Operation<XML.Tree, XML.Tree> FETCH_APPL_TACS =
|
|
wneuper@4848
|
37 |
IsacOperationsScala.fetchApplicableTactics();
|
|
wneuper@4848
|
38 |
public static final Operation<XML.Tree, XML.Tree> FETCH_PROP_TAC =
|
|
wneuper@4848
|
39 |
IsacOperationsScala.fetchProposedTactic();
|
|
wneuper@4848
|
40 |
public static final Operation<XML.Tree, XML.Tree> FIND_FILL_PATTS =
|
|
wneuper@4848
|
41 |
IsacOperationsScala.findFillpatterns();
|
|
wneuper@4848
|
42 |
public static final Operation<XML.Tree, XML.Tree> GET_ACC_ASMS =
|
|
wneuper@4848
|
43 |
IsacOperationsScala.getAccumulatedAsms();
|
|
wneuper@4848
|
44 |
public static final Operation<XML.Tree, XML.Tree> GET_ACTIVE_FORM =
|
|
wneuper@4848
|
45 |
IsacOperationsScala.getActiveFormula();
|
|
wneuper@4848
|
46 |
public static final Operation<XML.Tree, XML.Tree> GET_ASMS =
|
|
wneuper@4848
|
47 |
IsacOperationsScala.getAssumptions();
|
|
wneuper@4848
|
48 |
public static final Operation<XML.Tree, XML.Tree> GET_FORMULAE =
|
|
wneuper@4848
|
49 |
IsacOperationsScala.getFormulaeFromTo();
|
|
wneuper@4848
|
50 |
public static final Operation<XML.Tree, XML.Tree> GET_TAC =
|
|
wneuper@4848
|
51 |
IsacOperationsScala.getTactic();
|
|
wneuper@4848
|
52 |
public static final Operation<XML.Tree, XML.Tree> INIT_CTXT =
|
|
wneuper@4848
|
53 |
IsacOperationsScala.initContext();
|
|
wneuper@4848
|
54 |
public static final Operation<XML.Tree, XML.Tree> INPUT_FILL_FORM =
|
|
wneuper@4848
|
55 |
IsacOperationsScala.inputFillFormula();
|
|
wneuper@4848
|
56 |
public static final Operation<XML.Tree, XML.Tree> INTER_STEPS =
|
|
wneuper@4848
|
57 |
IsacOperationsScala.interSteps();
|
|
wneuper@4848
|
58 |
public static final Operation<scala.math.BigInt, XML.Tree> ITERATOR =
|
|
wneuper@4848
|
59 |
IsacOperationsScala.Iterator();
|
|
wneuper@4848
|
60 |
public static final Operation<scala.math.BigInt, XML.Tree> MODEL_PBL =
|
|
wneuper@4848
|
61 |
IsacOperationsScala.modelProblem();
|
|
wneuper@4848
|
62 |
public static final Operation<XML.Tree, XML.Tree> MODIFY_CALCHEAD =
|
|
wneuper@4848
|
63 |
IsacOperationsScala.modifyCalcHead();
|
|
wneuper@4848
|
64 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ACTIVE_CALCHEAD =
|
|
wneuper@4848
|
65 |
IsacOperationsScala.moveActiveCalcHead();
|
|
wneuper@4848
|
66 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ACTIVE_DOWN =
|
|
wneuper@4848
|
67 |
IsacOperationsScala.moveActiveDown();
|
|
wneuper@4848
|
68 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ACTIVE_FORM =
|
|
wneuper@4848
|
69 |
IsacOperationsScala.moveActiveFormula();
|
|
wneuper@4848
|
70 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ACTIVE_LEVDN =
|
|
wneuper@4848
|
71 |
IsacOperationsScala.moveActiveLevelDown();
|
|
wneuper@4848
|
72 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ACTIVE_LEVUP =
|
|
wneuper@4848
|
73 |
IsacOperationsScala.moveActiveLevelUp();
|
|
wneuper@4848
|
74 |
public static final Operation<scala.math.BigInt, XML.Tree> MOVE_ACTIVE_ROOT =
|
|
wneuper@4848
|
75 |
IsacOperationsScala.moveActiveRoot();
|
|
wneuper@4848
|
76 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ACTIVE_UP =
|
|
wneuper@4848
|
77 |
IsacOperationsScala.moveActiveUp();
|
|
wneuper@4848
|
78 |
public static final Operation<XML.Tree, XML.Tree> MOVE_CALCHEAD =
|
|
wneuper@4848
|
79 |
IsacOperationsScala.moveCalcHead();
|
|
wneuper@4848
|
80 |
public static final Operation<XML.Tree, XML.Tree> MOVE_DOWN =
|
|
wneuper@4848
|
81 |
IsacOperationsScala.moveDown();
|
|
wneuper@4848
|
82 |
public static final Operation<XML.Tree, XML.Tree> MOVE_LEVDN =
|
|
wneuper@4848
|
83 |
IsacOperationsScala.moveLevelDown();
|
|
wneuper@4848
|
84 |
public static final Operation<XML.Tree, XML.Tree> MOVE_LEVUP =
|
|
wneuper@4848
|
85 |
IsacOperationsScala.moveLevelUp();
|
|
wneuper@4848
|
86 |
public static final Operation<XML.Tree, XML.Tree> MOVE_ROOT =
|
|
wneuper@4848
|
87 |
IsacOperationsScala.moveRoot();
|
|
wneuper@4848
|
88 |
public static final Operation<XML.Tree, XML.Tree> MOVE_UP =
|
|
wneuper@4848
|
89 |
IsacOperationsScala.moveUp();
|
|
wneuper@4848
|
90 |
public static final Operation<XML.Tree, XML.Tree> REF_FORMULA =
|
|
wneuper@4848
|
91 |
IsacOperationsScala.refFormula();
|
|
wneuper@4848
|
92 |
public static final Operation<XML.Tree, XML.Tree> REFINE_PBL =
|
|
wneuper@4848
|
93 |
IsacOperationsScala.refineProblem();
|
|
wneuper@4848
|
94 |
public static final Operation<XML.Tree, XML.Tree> REPLACE_FORM =
|
|
wneuper@4848
|
95 |
IsacOperationsScala.replaceFormula();
|
|
wneuper@4848
|
96 |
public static final Operation<XML.Tree, XML.Tree> REQUEST_FILL_FORM =
|
|
wneuper@4848
|
97 |
IsacOperationsScala.requestFillformula();
|
|
wneuper@4848
|
98 |
public static final Operation<XML.Tree, XML.Tree> RESET_CALCHEAD =
|
|
wneuper@4848
|
99 |
IsacOperationsScala.resetCalcHead();
|
|
wneuper@4848
|
100 |
public static final Operation<XML.Tree, XML.Tree> SET_CTXT =
|
|
wneuper@4848
|
101 |
IsacOperationsScala.setContext();
|
|
wneuper@4848
|
102 |
public static final Operation<XML.Tree, XML.Tree> SET_MET =
|
|
wneuper@4848
|
103 |
IsacOperationsScala.setMethod();
|
|
wneuper@4848
|
104 |
public static final Operation<XML.Tree, XML.Tree> SET_NEXT_TAC =
|
|
wneuper@4848
|
105 |
IsacOperationsScala.setNextTactic();
|
|
wneuper@4848
|
106 |
public static final Operation<XML.Tree, XML.Tree> SET_PBL =
|
|
wneuper@4848
|
107 |
IsacOperationsScala.setProblem();
|
|
wneuper@4848
|
108 |
public static final Operation<XML.Tree, XML.Tree> SET_THY =
|
|
wneuper@4848
|
109 |
IsacOperationsScala.setTheory();
|
|
wneuper@4848
|
110 |
|
|
wneuper@4848
|
111 |
|
|
wneuper@4848
|
112 |
}
|