1.1 --- a/TODO.md	Mon Dec 11 17:26:30 2023 +0100
     1.2 +++ b/TODO.md	Sat Dec 30 06:22:52 2023 +0100
     1.3 @@ -41,10 +41,14 @@
     1.4     Proposals for a solution are in test/../Test_VSCode_Example.thy
     1.5     in subsubsection ‹Start Example with a CAS_Cmd›
     1.6  
     1.7 +* WN: cut out Calc.state_pre, Calc.state_post; only Ctree.state shall remain
     1.8 +  ?or could that be reasonable also together with Isabelle/PIDE?
     1.9  
    1.10  ***** priority of WN items is top down, most urgent/simple on top
    1.11  
    1.12  * WN: 
    1.13 +* WN: cut out Ctree_Basic.ets: a step will never return several internal steps in the future
    1.14 +* WN: rm Ctree_Basic.envp
    1.15  * WN: I_Model: review/rename seek_ppc, overwrite_ppc
    1.16  * WN: replace I_Model.feedb_values -> val get_values = Pre_Conds.get_values
    1.17  * WN: replace I_Model.descriptor with fun descr_exists: descriptor -> feedback -> bool

     2.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml	Mon Dec 11 17:26:30 2023 +0100
     2.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml	Sat Dec 30 06:22:52 2023 +0100
     2.3 @@ -128,23 +128,17 @@
     2.4    by the initial template, where the items are displayed with hints for the input format.
     2.5  *)
     2.6  datatype i_model_feedback = 
     2.7 -  Cor of (descriptor * (* correct input: descriptor, see Input_Descript.thy *)
     2.8 -     (values))                (* set of values for list-types: for decding
     2.9 -                                 Inc the values packed out from the list;
    2.10 -                                 They are packed back to an isalist for envs    *)
    2.11 -| Syn of TermC.as_string (* syntax error kept for P_Model.switch_pbl_met    *)
    2.12 -| Inc of (descriptor * values) (* see Cor                                   *)
    2.13 -| Sup of (descriptor * values) (* superfluous; input not found in O_Model.T *)
    2.14 +  Cor of (descriptor *   (* correct input: descriptor, see Input_Descript.thy *)
    2.15 +    values)              (* set of values for list-types: for decding
    2.16 +                            Inc the values packed out from the list;
    2.17 +                            They are packed back to an isalist for envs       *)
    2.18 +| Syn of TermC.as_string (* syntax error kept for P_Model.switch_pbl_met      *)
    2.19 +| Inc of (descriptor * values) (* see Cor                                     *)
    2.20 +| Sup of (descriptor * values) (* superfluous; input not found in O_Model.T   *)
    2.21  val feedback_empty = Syn "i_model_empty"
    2.22  
    2.23  
    2.24  type i_model_single = 
    2.25 -  int *             (* sequence of input, 0 = untouched, drop with PIDE ?  *)
    2.26 -  variants *        (* pointers to variants given in Formalise.model       *)
    2.27 -  bool *            (* input on this item is not/complete                  *)
    2.28 -  m_field *         (* #Given | #Find | #Relate                            *)
    2.29 -  i_model_feedback; (* variables and values, see above                     *)
    2.30 -type i_model_single = 
    2.31    int *                     (* sequence of input, 0 = untouched, drop with PIDE ? *)
    2.32    variants *                (* pointers to variants given in Formalise.model      *)
    2.33    bool *                    (* this item is not/complete, completed by O_Model.T  *)
    2.34 @@ -153,7 +147,6 @@
    2.35      Position.T);            (* for pushing feedback back to PIDE                  *)
    2.36  
    2.37  type i_model = i_model_single list;
    2.38 -type i_model = i_model_single list;
    2.39  
    2.40  (*shift to i-model.sml ?*)
    2.41  val i_model_empty = (0, [], false, "i_model_empty", (feedback_empty, Position.none));