1.1 --- a/src/Tools/isac/Specify/i-model.sml	Mon May 04 17:08:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Mon May 04 18:47:27 2020 +0200
     1.3 @@ -5,19 +5,15 @@
     1.4  
     1.5  signature MODEL_FOR_INTERACTION =
     1.6  sig
     1.7 -(*/------- to O_Model+I_ from ModelModel -------\*)
     1.8 -  type vats = Model_Def.vats
     1.9 -(*\------- to O_Model+I_ from ModelModel -------/*)
    1.10 -(*/------- to I_Model from Model -------\*)
    1.11 -  datatype itm_ = datatype Model_Def.itm_
    1.12 -  type itm = Model_Def.itm
    1.13 -  val e_itm : itm 
    1.14 -(*\------- to I_Model from Model -------/*)
    1.15 +  type variants = Model_Def.variants
    1.16  
    1.17 -  type T
    1.18 -  type single
    1.19 -
    1.20 +  type T = Model_Def.i_model
    1.21 +  type single = Model_Def.i_model_single
    1.22 +  datatype feedback = datatype Model_Def.i_model_feedback
    1.23 +  val empty : single 
    1.24 +                                               
    1.25  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.26 +  (* NONE *)
    1.27  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.28    (* NONE *)
    1.29  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.30 @@ -25,30 +21,12 @@
    1.31  
    1.32  structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
    1.33  struct
    1.34 -(*/------- to O_Model+I_ from Mode -------\*)
    1.35 -type vats =  Model_Def.vats;
    1.36 -(*\------- to O_Model+I_ from Model -------/*)
    1.37 -(*/------- to I_Model from Model -------\*)
    1.38 -(* the internal representation of a models' item
    1.39 -  4.9.01: not consistent:
    1.40 -  after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
    1.41 -  (involves 'is_error');
    1.42 -  bool in itm really necessary ???*)
    1.43 -datatype itm_ = datatype Model_Def.itm_;              (* internal state from fun parsitm                                 *)
    1.44  
    1.45 -(* data-type for working on pbl/met-ppc:
    1.46 -  in pbl initially holds descriptions (only) for user guidance *)
    1.47 -type itm = 
    1.48 -  int *        (* id  =0 .. untouched - descript (only) from init 
    1.49 -		              seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc?   *)
    1.50 -  vats *       (* variants - copy from ori                                                     *)
    1.51 -  bool *       (* input on this item is not/complete                                           *)
    1.52 -  string *     (* #Given | #Find | #Relate                                                     *)
    1.53 -  itm_;        (*                                                                              *)
    1.54 -val e_itm = (0, [], false, "e_itm", Syn "e_itm");
    1.55 -(*\------- to I_Model from Model -------/*)
    1.56 +type variants =  Model_Def.variants;
    1.57  
    1.58 -type T = Model_Def.itm list;
    1.59 -type single = Model_Def.itm;
    1.60 +type T = Model_Def.i_model_single list;
    1.61 +datatype feedback = datatype Model_Def.i_model_feedback;
    1.62 +type single = Model_Def.i_model_single;
    1.63 +val empty = Model_Def.i_model_empty;
    1.64  
    1.65  (**)end(**);
    1.66 \ No newline at end of file