1.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Jan 17 13:47:19 2020 +0100
     1.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Jan 17 14:10:10 2020 +0100
     1.3 @@ -9,19 +9,19 @@
     1.4    type NEW (* TODO: refactor "fun me" with calcstate and remove *)
     1.5    val me : Tactic.input -> Ctree.pos' -> NEW -> Ctree.ctree ->
     1.6      Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
     1.7 -  val autocalc : Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list ->
     1.8 -    Solve.auto -> string * Ctree.pos' list * (Ctree.state)
     1.9 +  val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list ->
    1.10 +    Solve.auto -> string * Ctree.pos' list * (Calc.T)
    1.11    val locatetac :
    1.12 -    Tactic.input -> Ctree.state -> string * (Generate.taci list * Ctree.pos' list * (Ctree.state))
    1.13 +    Tactic.input -> Calc.T -> string * (Generate.taci list * Ctree.pos' list * (Calc.T))
    1.14    val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
    1.15  
    1.16    val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
    1.17    val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
    1.18    val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list
    1.19    val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
    1.20 -  val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    1.21 -  val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    1.22 -  val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    1.23 +  val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    1.24 +  val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    1.25 +  val set_theory : Rule.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    1.26    val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
    1.27  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.28    val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
    1.29 @@ -30,8 +30,8 @@
    1.30    type nxt_
    1.31    datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
    1.32    val loc_solve_ : Tactic.T -> Ctree.ctree *  Ctree.pos' -> lOc_
    1.33 -  val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
    1.34 -  val TESTg_form : Ctree.state -> Generate.mout
    1.35 +  val loc_specify_ : Tactic.T -> Calc.T -> lOc_
    1.36 +  val TESTg_form : Calc.T -> Generate.mout
    1.37  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.38  
    1.39  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)