3 import edu.tum.cs.isabelle._
4 import edu.tum.cs.isabelle.api.XML
6 object IsacOperationsScala {
8 def implicitly[I : Codec, O : Codec](name: String): Operation[I, O] =
9 Operation.simple(name, Codec[I], Codec[O])
12 val Hello = implicitly[String, String]("hello")
13 val Teststr = implicitly[String, String]("teststr")
14 val Testit = implicitly[scala.math.BigInt, XML.Tree]("testit")
15 val TestTermTransfer = implicitly[XML.Tree, XML.Tree]("test_term_transfer")
16 val TestTermOneWay = implicitly[String, XML.Tree]("test_term_one_way")
17 val ScalaTermOfString = implicitly[String, XML.Tree]("scalaterm_of_string")
19 // Protoco.thy operation_setup for all isabisac's Math_Engine --------
20 val appendFormula = implicitly[XML.Tree, XML.Tree]("append_form")
21 val autoCalculate = implicitly[XML.Tree, XML.Tree]("autocalculate")
22 val applyTactic = implicitly[XML.Tree, XML.Tree]("apply_tac")
23 val CalcTree = implicitly[XML.Tree, XML.Tree]("calctree")
24 val checkContext = implicitly[XML.Tree, XML.Tree]("check_ctxt")
26 val DEconstrCalcTree = implicitly[scala.math.BigInt, XML.Tree]("deconstrcalctree")
27 val fetchApplicableTactics = implicitly[XML.Tree, XML.Tree]("fetch_applicable_tacs")
28 val fetchProposedTactic = implicitly[XML.Tree, XML.Tree]("fetch_proposed_tac")
29 val findFillpatterns = implicitly[XML.Tree, XML.Tree]("find_fill_patts")
30 val getAccumulatedAsms = implicitly[XML.Tree, XML.Tree]("get_accumulated_asms")
32 val getActiveFormula = implicitly[XML.Tree, XML.Tree]("get_active_form")
33 val getAssumptions = implicitly[XML.Tree, XML.Tree]("get_asms")
34 val getFormulaeFromTo = implicitly[XML.Tree, XML.Tree]("getformulaefromto")
35 val getTactic = implicitly[XML.Tree, XML.Tree]("get_tac")
36 val initContext = implicitly[XML.Tree, XML.Tree]("init_ctxt")
38 val inputFillFormula = implicitly[XML.Tree, XML.Tree]("input_fill_form")
39 val interSteps = implicitly[XML.Tree, XML.Tree]("inter_steps")
40 val Iterator = implicitly[scala.math.BigInt, XML.Tree]("iterator")
41 val modelProblem = implicitly[scala.math.BigInt, XML.Tree]("model_pbl")
42 val modifyCalcHead = implicitly[XML.Tree, XML.Tree]("modify_calchead")
44 val moveActiveCalcHead = implicitly[XML.Tree, XML.Tree]("move_active_calchead")
45 val moveActiveDown = implicitly[XML.Tree, XML.Tree]("move_active_down")
46 val moveActiveFormula = implicitly[XML.Tree, XML.Tree]("move_active_form")
47 val moveActiveLevelDown = implicitly[XML.Tree, XML.Tree]("move_active_levdown")
48 val moveActiveLevelUp = implicitly[XML.Tree, XML.Tree]("move_active_levup")
50 val moveActiveRoot = implicitly[scala.math.BigInt, XML.Tree]("moveactiveroot")
51 val moveActiveUp = implicitly[XML.Tree, XML.Tree]("move_active_up")
52 val moveCalcHead = implicitly[XML.Tree, XML.Tree]("move_calchead")
53 val moveDown = implicitly[XML.Tree, XML.Tree]("move_down")
54 val moveLevelDown = implicitly[XML.Tree, XML.Tree]("move_levdn")
56 val moveLevelUp = implicitly[XML.Tree, XML.Tree]("move_levup")
57 val moveRoot = implicitly[XML.Tree, XML.Tree]("move_root")
58 val moveUp = implicitly[XML.Tree, XML.Tree]("move_up")
59 val refFormula = implicitly[XML.Tree, XML.Tree]("refformula")
60 val refineProblem = implicitly[XML.Tree, XML.Tree]("refine_pbl")
62 val replaceFormula = implicitly[XML.Tree, XML.Tree]("replace_form")
63 val requestFillformula = implicitly[XML.Tree, XML.Tree]("request_fill_form")
64 val resetCalcHead = implicitly[XML.Tree, XML.Tree]("reset_calchead")
65 val setContext = implicitly[XML.Tree, XML.Tree]("set_ctxt")
66 val setMethod = implicitly[XML.Tree, XML.Tree]("set_met")
68 val setNextTactic = implicitly[XML.Tree, XML.Tree]("set_next_tac")
69 val setProblem = implicitly[XML.Tree, XML.Tree]("set_pbl")
70 val setTheory = implicitly[XML.Tree, XML.Tree]("set_thy")
72 //-------------------------------------------------------------------
73 val UseThys = implicitly[List[String], Unit]("use_thys")