1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed Dec 14 10:45:41 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Wed Dec 14 14:20:25 2016 +0100
     1.3 @@ -2,45 +2,35 @@
     1.4     use"generate.sml";
     1.5     *)
     1.6  signature CALC_TREE =
     1.7 -sig (*vvv request into signature is incremental *)
     1.8 -  (* for calchead.sml *)
     1.9 +sig (*vvv request into signature is incremental with *.sml *)
    1.10 +  (* for calchead.sml --------------------------------------------------------------  vvv *)
    1.11    type taci
    1.12    val e_taci : taci
    1.13 -  datatype edit = EdUndef | Protect | Write
    1.14 -  eqtype indent
    1.15 -  datatype nest = Closed | Nundef | Open
    1.16    datatype pblmet = Method of metID | Problem of pblID | Upblmet
    1.17 -  datatype inout =
    1.18 -     Error_ of string
    1.19 -  | FormKF of cellID * edit * indent * nest * cterm'
    1.20 -  | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) 
    1.21 -  | RefineKF of match list
    1.22 +  datatype mout =
    1.23 +    EmptyMout
    1.24 +  | Error' of string
    1.25 +  | FormKF of cterm'
    1.26 +  | PpcKF of pblmet * item ppc
    1.27    | RefinedKF of pblID * (itm list * (bool * term) list)
    1.28 -  datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
    1.29    val generate1 : theory -> tac_ -> istate * Proof.context ->
    1.30 -    posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
    1.31 +    pos' -> ptree -> pos' * pos' list * mout * ptree (* for calchead.sml ^^^ *)
    1.32 +  val init_istate : tac -> term -> istate (* for solve.sml *)
    1.33    val init_pbl : (string * (term * 'a)) list -> itm list
    1.34    val init_pbl' : (string * (term * term)) list -> itm list
    1.35 -  (* for appl.sml *)
    1.36 -  (* for script.sml *)
    1.37 -  (* for solve.sml *)
    1.38 -  val generate_hard : theory -> tac_ -> pos * pos_ -> ptree -> pos' * pos' list * mout * ptree
    1.39 -  val init_istate : tac -> term -> istate
    1.40 -  (* for inform.sml *)
    1.41 -  val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos')
    1.42 -  (* for mathengine.sml *)
    1.43 -  val generate : (tac * tac_ * ((posel list * pos_) * (istate * Proof.context))) list ->
    1.44 -     ptree * pos' list * pos' -> ptree * pos' list * pos'
    1.45 -  (* for interface.sml *)
    1.46 -  val generate_inconsistent_rew :
    1.47 -     subs option * thm'' ->
    1.48 -     term -> istate * Proof.context -> pos * pos_ -> ptree -> ptree * (posel list * pos_)
    1.49 +  val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos') (* for inform.sml *)
    1.50 +  val generate_hard : (* for solve.sml *)
    1.51 +    theory -> tac_ -> pos' -> ptree -> pos' * pos' list * mout * ptree
    1.52 +  val generate : (tac * tac_ * (pos' * (istate * Proof.context))) list ->
    1.53 +    ptree * pos' list * pos' -> ptree * pos' list * pos' (* for mathengine.sml *)
    1.54 +  val generate_inconsistent_rew : subs option * thm'' -> term -> istate * Proof.context ->
    1.55 +    pos' -> ptree -> ptree * pos' (* for interface.sml *)
    1.56  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.57  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.58  end
    1.59  
    1.60  (**)
    1.61 -structure Ctree(*: CALC_TREE*) =
    1.62 +structure Ctree(**): CALC_TREE(**) =
    1.63  (**)
    1.64  struct
    1.65  (* initialize istate for Detail_Set *)