# HG changeset patch
# User Walther Neuper <wneuper@ist.tugraz.at>
# Date 1481721625 -3600
# Node ID c988bdecd7be629f02795c41ae72dfeadb123a25
# Parent  aab874fdd910f0d691deeec8dd4ca9bb20c32c20
signature for redesigned mout

diff -r aab874fdd910 -r c988bdecd7be src/Tools/isac/Interpret/generate.sml
--- a/src/Tools/isac/Interpret/generate.sml	Wed Dec 14 10:45:41 2016 +0100
+++ b/src/Tools/isac/Interpret/generate.sml	Wed Dec 14 14:20:25 2016 +0100
@@ -2,45 +2,35 @@
    use"generate.sml";
    *)
 signature CALC_TREE =
-sig (*vvv request into signature is incremental *)
-  (* for calchead.sml *)
+sig (*vvv request into signature is incremental with *.sml *)
+  (* for calchead.sml --------------------------------------------------------------  vvv *)
   type taci
   val e_taci : taci
-  datatype edit = EdUndef | Protect | Write
-  eqtype indent
-  datatype nest = Closed | Nundef | Open
   datatype pblmet = Method of metID | Problem of pblID | Upblmet
-  datatype inout =
-     Error_ of string
-  | FormKF of cellID * edit * indent * nest * cterm'
-  | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) 
-  | RefineKF of match list
+  datatype mout =
+    EmptyMout
+  | Error' of string
+  | FormKF of cterm'
+  | PpcKF of pblmet * item ppc
   | RefinedKF of pblID * (itm list * (bool * term) list)
-  datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
   val generate1 : theory -> tac_ -> istate * Proof.context ->
-    posel list * pos_ -> ptree -> pos' * pos' list * mout * ptree
+    pos' -> ptree -> pos' * pos' list * mout * ptree (* for calchead.sml ^^^ *)
+  val init_istate : tac -> term -> istate (* for solve.sml *)
   val init_pbl : (string * (term * 'a)) list -> itm list
   val init_pbl' : (string * (term * term)) list -> itm list
-  (* for appl.sml *)
-  (* for script.sml *)
-  (* for solve.sml *)
-  val generate_hard : theory -> tac_ -> pos * pos_ -> ptree -> pos' * pos' list * mout * ptree
-  val init_istate : tac -> term -> istate
-  (* for inform.sml *)
-  val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos')
-  (* for mathengine.sml *)
-  val generate : (tac * tac_ * ((posel list * pos_) * (istate * Proof.context))) list ->
-     ptree * pos' list * pos' -> ptree * pos' list * pos'
-  (* for interface.sml *)
-  val generate_inconsistent_rew :
-     subs option * thm'' ->
-     term -> istate * Proof.context -> pos * pos_ -> ptree -> ptree * (posel list * pos_)
+  val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos') (* for inform.sml *)
+  val generate_hard : (* for solve.sml *)
+    theory -> tac_ -> pos' -> ptree -> pos' * pos' list * mout * ptree
+  val generate : (tac * tac_ * (pos' * (istate * Proof.context))) list ->
+    ptree * pos' list * pos' -> ptree * pos' list * pos' (* for mathengine.sml *)
+  val generate_inconsistent_rew : subs option * thm'' -> term -> istate * Proof.context ->
+    pos' -> ptree -> ptree * pos' (* for interface.sml *)
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end
 
 (**)
-structure Ctree(*: CALC_TREE*) =
+structure Ctree(**): CALC_TREE(**) =
 (**)
 struct
 (* initialize istate for Detail_Set *)