1.1 --- a/src/Tools/isac/Specify/i-model.sml	Sun Dec 10 07:56:02 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sun Dec 10 17:35:07 2023 +0100
     1.3 @@ -50,7 +50,6 @@
     1.4    val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
     1.5    val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
     1.6      TermC.as_string -> add_single
     1.7 -  (*probably unused in PIDE, thus-----v----v*)
     1.8    val add_single: theory -> single_POS -> T_POS -> T_POS
     1.9  
    1.10    val make_tactic: m_field -> TermC.as_string * T_POS -> Tactic.T
    1.11 @@ -58,8 +57,10 @@
    1.12    val descriptor: feedback -> descriptor
    1.13    val descriptor_POS: feedback_POS -> descriptor
    1.14    val values: feedback -> values option
    1.15 +  val get_values: T_POS -> values list
    1.16    val o_model_values: feedback -> values
    1.17 -  val values_POS': feedback_POS -> values
    1.18 +  val feedb_values: feedback_POS -> values
    1.19 +  val order_by_patt:  Model_Pattern.T -> T_POS ->T_POS
    1.20    val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
    1.21    val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
    1.22    val is_notyet_input: Proof.context -> T_POS -> O_Model.values -> O_Model.single ->
    1.23 @@ -275,10 +276,28 @@
    1.24    | o_model_values (Sup (_, ts)) = ts
    1.25    | o_model_values (Mis _) = []
    1.26    | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
    1.27 -fun values_POS' (Cor_POS (_, ts)) = ts
    1.28 -  | values_POS' (Syn_POS _) = raise ERROR "values_POS' NOT for Syn_POS"
    1.29 -  | values_POS' (Inc_POS (_, ts)) = ts
    1.30 -  | values_POS' (Sup_POS (_, ts)) = ts
    1.31 +(*RN feedb_vals'*)
    1.32 +fun feedb_values (Cor_POS (_, ts)) = ts
    1.33 +  | feedb_values (Syn_POS _) = raise ERROR "feedb_values NOT for Syn_POS"
    1.34 +  | feedb_values (Inc_POS (_, ts)) = ts
    1.35 +  | feedb_values (Sup_POS (_, ts)) = ts
    1.36 +
    1.37 +(*assumption: i_model has filtered max_vnt*)
    1.38 +local
    1.39 + fun order_by_pa i_model (_, (descr, _ )) =
    1.40 +   case find_first (fn (_, _, _, _, (feedb, _)) => descr = descriptor_POS feedb) i_model of
    1.41 +     SOME i_single => [i_single]
    1.42 +   | NONE => []
    1.43 +in
    1.44 +  fun order_by_patt model_patt i_model = model_patt |> map (order_by_pa i_model) |> flat
    1.45 +end
    1.46 +fun feedb_vals (Cor_POS (_, ts)) = [ts]
    1.47 +  | feedb_vals (Syn_POS _) = []
    1.48 +  | feedb_vals (Inc_POS (_, ts)) = [ts]
    1.49 +  | feedb_vals (Sup_POS (_, ts)) = [ts]
    1.50 +fun get_values i_model =
    1.51 +  map (fn (_, _, _, _, (feedb, _)) => feedb_vals feedb) i_model
    1.52 +  |> flat
    1.53  
    1.54  fun descr_pairs_to_string ctxt equal_descr_pairs =
    1.55  (map (fn (a, b) => pair (Model_Pattern.single_to_string ctxt a) (single_to_string_POS ctxt b)
    1.56 @@ -301,7 +320,7 @@
    1.57  (*update the itm_ already input, all..from ori*)
    1.58  fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) = 
    1.59    let 
    1.60 -    val ts' = union op = (values_POS' feedb) ts;
    1.61 +    val ts' = union op = (feedb_values feedb) ts;
    1.62      val complete = if eq_set op = (ts', all) then true else false
    1.63    in
    1.64      case feedb of
    1.65 @@ -327,7 +346,7 @@
    1.66            f = f' andalso d = (descriptor_POS feedb)) itms of
    1.67          SOME (_, _, _, _, (feedb, _)) =>
    1.68            let
    1.69 -            val ts' = inter op = (values_POS' feedb) ts
    1.70 +            val ts' = inter op = (feedb_values feedb) ts
    1.71            in
    1.72              if subset op = (ts, ts') 
    1.73              then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
    1.74 @@ -473,7 +492,7 @@
    1.75      if Model_Def.is_list_descr descr
    1.76      then
    1.77        let
    1.78 -        val already_input = feedb |> values_POS'
    1.79 +        val already_input = feedb |> feedb_values
    1.80          val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
    1.81          val ts = already_input @ [hd miss]
    1.82        in