1.1 --- a/src/Tools/isac/Specify/specify.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/specify.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -3,8 +3,6 @@
     1.4    val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
     1.5    val do_all: Calc.T -> Calc.T 
     1.6    val finish_phase: Calc.T -> Calc.T
     1.7 -  val finish_phase_PIDEnote: Proof.context -> O_Model.T * References.T -> I_Model.T * References.T -> 
     1.8 -    I_Model.T * I_Model.T
     1.9  
    1.10    val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
    1.11      (Model_Def.m_field * TermC.as_string) option
    1.12 @@ -80,8 +78,8 @@
    1.13      val cdI = if dI = ThyC.id_empty then dI' else dI;
    1.14      val cpI = if pI = Problem.id_empty then pI' else pI;
    1.15      val cmI = if mI = MethodC.id_empty then mI' else mI;
    1.16 -    val {ppc = pbt, prls, where_, ...} = Problem.from_store_PIDE ctxt cpI;
    1.17 -    val {ppc = mpc, ...} = MethodC.from_store_PIDE ctxt cmI
    1.18 +    val {ppc = pbt, prls, where_, ...} = Problem.from_store ctxt cpI;
    1.19 +    val {ppc = mpc, ...} = MethodC.from_store ctxt cmI
    1.20      val (preok, _) = Pre_Conds.check prls where_ pbl 0;
    1.21    in
    1.22      if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
    1.23 @@ -115,7 +113,7 @@
    1.24  fun for_method_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
    1.25    let
    1.26      val cmI = if mI = MethodC.id_empty then mI' else mI;
    1.27 -    val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI;    (*..MethodC ?*)
    1.28 +    val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)
    1.29      val (preok, _) = Pre_Conds.check prls pre pbl 0;
    1.30    in
    1.31      (case find_first (I_Model.is_error o #5) met of
    1.32 @@ -164,10 +162,10 @@
    1.33      val (i_model, m_patt) =
    1.34         if p_ = Pos.Met then
    1.35           (met,
    1.36 -           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
    1.37 +           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #ppc)
    1.38         else
    1.39           (pbl,
    1.40 -           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store_PIDE ctxt |> #ppc)
    1.41 +           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #ppc)
    1.42      in
    1.43        case I_Model.check_single ctxt m_field oris i_model m_patt ct of
    1.44          I_Model.Add i_single => (*..union old input *)
    1.45 @@ -194,23 +192,13 @@
    1.46  	  | _ => raise ERROR "finish_phase: unvered case get_obj"
    1.47    	val (_, pI, mI) = References.select_input ospec spec
    1.48    	val ctxt = Ctree.get_ctxt pt pos
    1.49 -  	val mpc = (#ppc o MethodC.from_store_PIDE ctxt) mI
    1.50 -  	val ppc = (#ppc o Problem.from_store_PIDE ctxt) pI
    1.51 +  	val mpc = (#ppc o MethodC.from_store ctxt) mI
    1.52 +  	val ppc = (#ppc o Problem.from_store ctxt) pI
    1.53    	val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
    1.54      val pt = Ctree.update_pblppc pt p pits
    1.55  	  val pt = Ctree.update_metppc pt p mits
    1.56    in (pt, (p, Pos.Met)) end
    1.57  
    1.58 -(*an unclarified remainder of the transition from sessions to PIDE with ctxt*)
    1.59 -fun finish_phase_PIDEnote ctxt (o_model, o_refs) (problem_model, refs) =
    1.60 -  let
    1.61 -  	val (_, pI, mI) = References.select_input o_refs refs
    1.62 -  	val method_pattern = (#ppc o MethodC.from_store_PIDE ctxt) mI
    1.63 -  	val problem_pattern = (#ppc o Problem.from_store_PIDE ctxt) pI
    1.64 -  	val (problem_model, method_model) =
    1.65 -      I_Model.complete_method (o_model, method_pattern, problem_pattern, problem_model)
    1.66 -  in (problem_model, method_model) end
    1.67 -
    1.68  (* do all specification in one single step:
    1.69     complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
    1.70     oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
    1.71 @@ -222,7 +210,7 @@
    1.72          => (pors, dI, pI, mI)
    1.73      | _ => raise ERROR "do_all: uncovered case get_obj"
    1.74      val ctxt = Ctree.get_ctxt pt pos
    1.75 -	  val {ppc, ...} = MethodC.from_store_PIDE ctxt mI
    1.76 +	  val {ppc, ...} = MethodC.from_store ctxt mI
    1.77      val (_, vals) = O_Model.values' pors
    1.78  	  val ctxt = ContextC.initialise dI vals
    1.79      val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),