1.1 --- a/src/Tools/isac/Specify/specify.sml	Mon Jun 01 16:11:05 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/specify.sml	Wed Jun 03 09:56:24 2020 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4      (Model_Def.m_field * TermC.as_string) option
     1.5  (*TODO: vvvvvvvvvvvvvv unify code*)
     1.6    val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post
     1.7 -  val by_tactic': string -> TermC.as_string -> Calc.T -> string * Calc.state_post
     1.8 +  val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
     1.9  (*TODO: ^^^^^^^^^^^^^^ unify code*)
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11    (*NONE*)
    1.12 @@ -132,48 +132,28 @@
    1.13          end
    1.14    end
    1.15  
    1.16 -fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) = 
    1.17 -      let
    1.18 -        val (met, oris, (dI', _, mI'), _, (dI, _, mI), ctxt) = Specification.get_data (pt, pos)
    1.19 -        val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
    1.20 -        val cmI = if mI = Method.id_empty then mI' else mI
    1.21 -        val {ppc, ...} = Method.from_store cmI
    1.22 -      in 
    1.23 -        case I_Model.check_single ctxt sel oris met ppc ct of
    1.24 -          I_Model.Add itm =>  (*..union old input *)
    1.25 -    	      let
    1.26 -              val met' = I_Model.add_single thy itm met
    1.27 -              val tac' = I_Model.get_tac sel (ct, met')
    1.28 -    	        val (p, pt') =
    1.29 -    	         case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
    1.30 -    	          ((p, Pos.Met), _, _, pt') => (p, pt')
    1.31 -    	        | _ => raise ERROR "by_tactic': uncovered case of generate1"
    1.32 -    	      in 
    1.33 -              ("ok", ([], [], (pt', (p, Pos.Met))))
    1.34 -            end
    1.35 -        | I_Model.Err msg => (msg, ([], [], (pt, (p, Pos.Met))))
    1.36 -      end
    1.37 -  | by_tactic' sel ct (pt, pos as (p, p_(*Frm, Pbl*))) =
    1.38 -      let
    1.39 -        val (_, oris, (dI', pI', _), pbl, (dI, pI, _), ctxt) = Specification.get_data (pt, pos)
    1.40 -        val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
    1.41 -        val cpI = if pI = Problem.id_empty then pI' else pI
    1.42 -        val {ppc,  ...} = Problem.from_store cpI
    1.43 -      in
    1.44 -        case I_Model.check_single ctxt sel oris pbl ppc ct of
    1.45 -          I_Model.Add itm => (*..union old input *)
    1.46 -	          let
    1.47 -	            val pbl' = I_Model.add_single thy itm pbl
    1.48 -              val tac' = I_Model.get_tac sel (ct, pbl')
    1.49 -	            val (p, pt') =
    1.50 -	              case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
    1.51 -  	              ((p, Pos.Pbl), _, _, pt') => (p, pt')
    1.52 -  	            | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"
    1.53 -	          in
    1.54 -              ("ok", ([], [], (pt', (p, p_))))
    1.55 -            end
    1.56 -        | I_Model.Err msg => (msg, ([], [], (pt, (p, p_))))
    1.57 -      end
    1.58 +fun by_Add_ m_field ct (pt, pos as (_, p_)) =
    1.59 +  let
    1.60 +    val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = Specification.get_data (pt, pos)
    1.61 +    val (i_model, m_patt) =
    1.62 +       if p_ = Pos.Met then
    1.63 +         (met,
    1.64 +           (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
    1.65 +       else
    1.66 +         (pbl,
    1.67 +           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store |> #ppc)
    1.68 +    in
    1.69 +      case I_Model.check_single ctxt m_field oris i_model m_patt ct of
    1.70 +        I_Model.Add i_single => (*..union old input *)
    1.71 +	        let
    1.72 +	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
    1.73 +            val tac' = I_Model.get_tac m_field (ct, i_model')
    1.74 +	          val  (_, _, _, pt') =  Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
    1.75 +	        in
    1.76 +            ("ok", ([], [], (pt', pos)))
    1.77 +          end
    1.78 +      | I_Model.Err msg => (msg, ([], [], (pt, pos)))
    1.79 +    end
    1.80  
    1.81  (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
    1.82    -- for input from scratch*)