1.1 --- a/src/Tools/isac/Specify/specification.sml	Thu May 14 15:06:18 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Thu May 14 16:08:41 2020 +0200
     1.3 @@ -63,8 +63,6 @@
     1.4  *)
     1.5  signature SPECIFICATION =
     1.6  sig
     1.7 -  type calcstate
     1.8 -  type calcstate'
     1.9  
    1.10    type T = Specification_Def.T
    1.11    val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
    1.12 @@ -103,11 +101,10 @@
    1.13    val is_error: I_Model.feedback -> bool
    1.14    val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
    1.15      I_Model.T * I_Model.T
    1.16 -  val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
    1.17 -  val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
    1.18 +  val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post
    1.19 +  val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
    1.20  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.21 -  val e_calcstate : Calc.T * State_Steps.T
    1.22 -  val e_calcstate' : calcstate'
    1.23 +  (*NONE*)
    1.24  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.25    val posterms2str: (Pos.pos' * term * 'a) list -> string
    1.26    val postermtacs2str: (Pos.pos' * term * Tactic.input option) list -> string
    1.27 @@ -143,38 +140,6 @@
    1.28  struct
    1.29  (**)
    1.30  
    1.31 -(** datatypes **)
    1.32 -
    1.33 -(* the state wich is stored after each step of calculation; it contains
    1.34 -   the calc-state and a list of [tac,istate](="tacis") to be applied next.
    1.35 -   the last_elem tacis is the first to apply to the calc-state and
    1.36 -   the (only) one shown to the front-end as the 'proposed tac'.
    1.37 -   the calc-state resulting from the application of tacis is not stored,
    1.38 -   because the tacis hold enough information for efficiently rebuilding
    1.39 -   this state just by "fun generate "
    1.40 -*)
    1.41 -type calcstate = 
    1.42 -  Calc.T *      (* the calc-state to which the tacis could be applied *)
    1.43 -  State_Steps.T (* ev. several (hidden) steps; 
    1.44 -                   in REVERSE order: first tac_ to apply is last_elem *)
    1.45 -val e_calcstate = ((Ctree.EmptyPtree, Pos.e_pos'), [State_Steps.single_empty]);
    1.46 -
    1.47 -(*the state used during one calculation within the mathengine; it contains
    1.48 -  a list of [tac,istate](="tacis") which generated the the calc-state;
    1.49 -  while this state's tacis are extended by each (internal) step,
    1.50 -  the calc-state is used for creating new nodes in the calc-tree
    1.51 -  (eg. applicable_in requires several particular nodes of the calc-tree)
    1.52 -  and then replaced by the the newly created;
    1.53 -  on leave of the mathengine the resuing calc-state is dropped anyway,
    1.54 -  because the tacis hold enought information for efficiently rebuilding
    1.55 -  this state just by "fun generate ".*)
    1.56 -type calcstate' = 
    1.57 -  State_Steps.T * (* cas. several (hidden) steps;
    1.58 -                       in REVERSE order: first tac_ to apply is last_elem                 *)
    1.59 -  Pos.pos' list *     (* a "continuous" sequence of pos', deleted by application of taci list *)     
    1.60 -  Calc.T          (* the calc-state resulting from the application of tacis               *)
    1.61 -val e_calcstate' = ([State_Steps.single_empty], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos')) : calcstate';
    1.62 -
    1.63  type T = Specification_Def.T;
    1.64  
    1.65  (* is the calchead complete ? *)