1.1 --- a/src/Tools/isac/Frontend/interface.sml	Fri Aug 07 15:52:17 2015 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Sun Aug 09 10:00:11 2015 +0200
     1.3 @@ -11,23 +11,26 @@
     1.4  
     1.5  signature MATH_ENGINE =
     1.6    sig
     1.7 -    val CalcTree : fmz list -> XML.tree
     1.8 -    val DEconstrCalcTree : calcID -> XML.tree
     1.9 -    val Iterator : calcID -> XML.tree
    1.10 -    val IteratorTEST : calcID -> iterID
    1.11      val appendFormula : calcID -> cterm' -> XML.tree (*unit future*)
    1.12      val autoCalculate : calcID -> auto -> XML.tree (*unit future*)
    1.13 +    val applyTactic : calcID -> pos' -> tac -> XML.tree
    1.14 +    val CalcTree : fmz list -> XML.tree
    1.15      val checkContext : calcID -> pos' -> guh -> XML.tree
    1.16 +    val DEconstrCalcTree : calcID -> XML.tree
    1.17      val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree
    1.18      val fetchProposedTactic : calcID -> XML.tree
    1.19 -    val applyTactic : calcID -> pos' -> tac -> XML.tree
    1.20 +    val findFillpatterns : calcID -> errpatID -> XML.tree
    1.21      val getAccumulatedAsms : calcID -> pos' -> XML.tree
    1.22      val getActiveFormula : calcID -> XML.tree
    1.23      val getAssumptions : calcID -> pos' -> XML.tree
    1.24 -    val initContext : calcID -> ketype -> pos' -> XML.tree
    1.25      val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree
    1.26      val getTactic : calcID -> pos' -> XML.tree
    1.27 +    val initContext : calcID -> ketype -> pos' -> XML.tree
    1.28 +    val inputFillFormula: calcID -> string -> XML.tree
    1.29      val interSteps : calcID -> pos' -> XML.tree
    1.30 +    val Iterator : calcID -> XML.tree
    1.31 +    val IteratorTEST : calcID -> iterID
    1.32 +    val modelProblem : calcID -> XML.tree
    1.33      val modifyCalcHead : calcID -> icalhd -> XML.tree
    1.34      val moveActiveCalcHead : calcID -> XML.tree
    1.35      val moveActiveDown : calcID -> XML.tree
    1.36 @@ -44,18 +47,15 @@
    1.37      val moveRoot : calcID -> XML.tree
    1.38      val moveUp : calcID -> pos' -> XML.tree
    1.39      val refFormula : calcID -> pos' -> XML.tree
    1.40 +    val refineProblem : calcID -> pos' -> guh -> XML.tree
    1.41      val replaceFormula : calcID -> cterm' -> XML.tree
    1.42 +    val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
    1.43      val resetCalcHead : calcID -> XML.tree
    1.44 -    val modelProblem : calcID -> XML.tree
    1.45 -    val refineProblem : calcID -> pos' -> guh -> XML.tree
    1.46      val setContext : calcID -> pos' -> guh -> XML.tree
    1.47      val setMethod : calcID -> metID -> XML.tree
    1.48      val setNextTactic : calcID -> tac -> XML.tree
    1.49      val setProblem : calcID -> pblID -> XML.tree
    1.50      val setTheory : calcID -> thyID -> XML.tree
    1.51 -    val findFillpatterns : calcID -> errpatID -> XML.tree
    1.52 -    val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
    1.53 -    val inputFillFormula: calcID -> string -> XML.tree
    1.54  (*------------ for tests*)
    1.55  val encode: cterm' -> cterm'
    1.56  val encode_fmz: fmz -> fmz

     2.1 --- a/test/Pure/PIDE/xml.ML	Fri Aug 07 15:52:17 2015 +0200
     2.2 +++ b/test/Pure/PIDE/xml.ML	Sun Aug 09 10:00:11 2015 +0200
     2.3 @@ -2,10 +2,17 @@
     2.4     Author: Walther Neuper 1505
     2.5     (c) copyright due to lincense terms.
     2.6  *)
     2.7 +"------------------------------------------------------------------------------------------------";
     2.8 +"table of contents -----------------------------------------------------------------------------";
     2.9 +"------------------------------------------------------------------------------------------------";
    2.10 +"----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";
    2.11 +"------------------------------------------------------------------------------------------------";
    2.12 +"------------------------------------------------------------------------------------------------";
    2.13  
    2.14  "----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";
    2.15  "----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";
    2.16  "----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";
    2.17 +"see https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt";
    2.18  fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
    2.19    | xmlstr i (XML.Elem ((str, []), trees)) = 
    2.20      indent i ^ "<" ^ str ^ ">" ^ "\n" ^
    2.21 @@ -197,3 +204,4 @@
    2.22  xmlstr 0 result = "<CALCTREE>\n  <CALCID>\n    111\n  </CALCID>\n</CALCTREE>";
    2.23  writeln (xmlstr 0 result);
    2.24  
    2.25 +