1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -11,7 +11,10 @@
     1.4  
     1.5    val initialise: Proof.context -> Formalise.T ->
     1.6      term * term * References.T * O_Model.T * Proof.context
     1.7 +  val initialise_PIDE: theory -> Formalise.T ->
     1.8 +    term * term * References.T * O_Model.T * Proof.context
     1.9    val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T
    1.10 +  val nxt_specify_init_calc_PIDE: theory -> Formalise.T -> Calc.T * State_Steps.T
    1.11  end
    1.12  
    1.13  (**)
    1.14 @@ -246,6 +249,40 @@
    1.15      in
    1.16        (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
    1.17      end;
    1.18 +(*  initialise <-?-> nxt_specify_init_calc *)
    1.19 +fun initialise_PIDE thy (fmz, (_, pI, mI)) = 
    1.20 +    let
    1.21 +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
    1.22 +	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
    1.23 +	    val (pI, (pors, pctxt), mI) = 
    1.24 +	      if mI = ["no_met"] 
    1.25 +	      then 
    1.26 +          let 
    1.27 +(*old* )    val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
    1.28 +(*old*)     val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
    1.29 +( *new*)    val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
    1.30 +            val pI' = Refine.refine_ori' pctxt pors pI;
    1.31 +          in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
    1.32 +            (hd o #solve_mets o Problem.from_store ctxt) pI')
    1.33 +          end
    1.34 +	      else
    1.35 +	        let
    1.36 +(*old* )    val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
    1.37 +(*old*)     val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
    1.38 +(*old*)   in (pI, (pors, pctxt), mI) end;
    1.39 +( *new*)    val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
    1.40 +          in (pI, (pors, pctxt), mI) end;
    1.41 +	    val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
    1.42 +	    val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))
    1.43 +	    val hdl = case cas of
    1.44 +		    NONE => Auto_Prog.pblterm dI pI
    1.45 +		  | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
    1.46 +	    val hdlPIDE = case cas of
    1.47 +		    NONE => Auto_Prog.pblterm dI pI
    1.48 +		  | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
    1.49 +    in
    1.50 +      (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
    1.51 +    end;
    1.52  (*TODO: HOW RELATES nxt_specify_init_calc \<longleftrightarrow> initialise *)
    1.53  fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
    1.54      if pI <> []
    1.55 @@ -286,5 +323,44 @@
    1.56      in
    1.57        ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
    1.58      end
    1.59 -
    1.60 +fun nxt_specify_init_calc_PIDE thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
    1.61 +    if pI <> []
    1.62 +    then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
    1.63 +	    let
    1.64 +        val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI
    1.65 +	      val dI = if dI = "" then Context.theory_name thy else dI
    1.66 +	      val mI = if mI = [] then hd solve_mets else mI
    1.67 +	      val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
    1.68 +	      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
    1.69 +				  ([], (dI,pI,mI), hdl, ContextC.empty)
    1.70 +	      val pt = update_spec pt [] (dI, pI, mI)
    1.71 +	      val pits = I_Model.init model
    1.72 +	      val pt = update_pbl pt [] pits
    1.73 +	    in ((pt, ([] , Pbl)), []) end
    1.74 +    else 
    1.75 +      if mI <> [] 
    1.76 +      then (* from met-browser *)
    1.77 +	      let
    1.78 +          val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI
    1.79 +	        val dI = if dI = "" then "Isac_Knowledge" else dI
    1.80 +	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
    1.81 +	          ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
    1.82 +	        val pt = update_spec pt [] (dI, pI, mI)
    1.83 +	        val mits = I_Model.init model
    1.84 +	        val pt = update_met pt [] mits
    1.85 +	      in ((pt, ([], Met)), []) end
    1.86 +      else (* new example, pepare for interactive modeling *)
    1.87 +	      let
    1.88 +	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) 
    1.89 +	          ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
    1.90 +	      in ((pt, ([], Pbl)), []) end
    1.91 +  | nxt_specify_init_calc_PIDE thy (model, refs) = 
    1.92 +    let            (* both          ^^^^^  ^^^^^^^^^^^^  are either empty or complete *)
    1.93 +	    val (_, hdl, refs, pors, pctxt) = initialise_PIDE thy (model, refs)
    1.94 +      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
    1.95 +        (model, refs) (pors, refs, hdl, pctxt)
    1.96 +    in
    1.97 +      ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
    1.98 +    end
    1.99 + 
   1.100  (**)end(**)