signature SPECIFY =

 sig

   val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)

   val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->

     Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input

   val do_all: Calc.T -> Calc.T 

   val finish_phase: Calc.T -> Calc.T

   val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->

     (Model_Def.m_field * TermC.as_string) option

   val item_to_add': theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->

     (Model_Def.m_field * TermC.as_string) option

 (*TODO: vvvvvvvvvvvvvv unify code*)

   val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post

   val by_tactic': string -> TermC.as_string -> Calc.T -> string * Calc.state_post

 (*TODO: ^^^^^^^^^^^^^^ unify code*)

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   (*NONE*)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

 structure Specify(**): SPECIFY(**) =

 struct

 (**)

 (*

   select an item in oris, notyet input in itms 

   (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)

 args of item_to_add'

   thy : for?

   oris: from formalization 'type fmz', structured for efficient access 

   pbt : the problem-pattern to be matched with oris in order to get itms

   itms: already input items

 *)

 fun item_to_add' thy [] pbt itms = (*root (only) ori...fmz=[]*)

     let

       fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0

       fun is_elem itms (_, (d, _)) = 

         case find_first (test_d d) itms of SOME _ => true | NONE => false

     in

       case filter_out (is_elem itms) pbt of

         (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))

       | _ => NONE

     end

   | item_to_add' thy oris _ itms =

     let

 (*OLD*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"

 (*OLD*)fun testi_vt v itm = Library.member op= (#2 (itm : I_Model.single)) v

       fun test_id ids r = Library.member op= ids (#1 (r : O_Model.single))

       fun test_subset itm (_, _, _, d, ts) = 

         (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)

       fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false

         | false_and_not_Sup (_, _, false, _, _) = true

         | false_and_not_Sup _ = false

       val v = if itms = [] then 1 else I_Model.max_vt itms

       val vors = if v = 0 then oris else filter (testr_vt v) oris  (* oris..vat *)

       val vits =

         if v = 0

         then itms                                 (* because of dsc without dat *)

   	    else filter (testi_vt v) itms;                             (* itms..vat *)

       val icl = filter false_and_not_Sup vits;                    (* incomplete *)

     in

       if icl = [] then

         case filter_out (test_id (map #1 vits)) vors of

           [] => NONE

         | miss => SOME (O_Model.getr_ct thy (hd miss))

       else

         case find_first (test_subset (hd icl)) vors of

           NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"

         | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))

     end

 (* preliminary doubling of code, ONLY difference SHALL BE in fun testr_vt *)

 fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)

     let

       fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0

       fun is_elem itms (_, (d, _)) = 

         case find_first (test_d d) itms of SOME _ => true | NONE => false

     in

       case filter_out (is_elem itms) pbt of

         (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))

       | _ => NONE

     end

   | item_to_add thy oris _ itms =

     let

 (*NEW*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v (*andalso (#3 ori) <> "#undef"*)

 (*OLD* )fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"

 ( *OLD*)fun testi_vt v itm = Library.member op= (#2 (itm : I_Model.single)) v

       fun test_id ids r = Library.member op= ids (#1 (r : O_Model.single))

       fun test_subset itm (_, _, _, d, ts) = 

         (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)

       fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false

         | false_and_not_Sup (_, _, false, _, _) = true

         | false_and_not_Sup _ = false

       val v = if itms = [] then 1 else I_Model.max_vt itms

       val vors = if v = 0 then oris else filter (testr_vt v) oris  (* oris..vat *)

       val vits =

         if v = 0

         then itms                                 (* because of dsc without dat *)

   	    else filter (testi_vt v) itms;                             (* itms..vat *)

       val icl = filter false_and_not_Sup vits;                    (* incomplete *)

     in

       if icl = [] then

         case filter_out (test_id (map #1 vits)) vors of

           [] => NONE

         | miss => SOME (O_Model.getr_ct thy (hd miss))

       else

         case find_first (test_subset (hd icl)) vors of

           NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"

         | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))

     end

 (*TODO: unify*)

 fun find_next_step (pt, (p, p_)) =

   let

 (*OLD*)val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = 

 (*OLD*)  case Ctree.get_obj I pt p of

 (*OLD*)    pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),

 (*OLD*)	  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)

 (*OLD*)  | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"

 (*OLD*)in

 (*OLD*)  if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then

 (*OLD*)

 (*NEW* )val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _), probl = pbl,

 (*NEW*)  spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));

 (*NEW*)in

 (*NEW*)  if Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin then

 ( *NEW*)

       case mI' of

         ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))

       | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))

     else

       let 

         (*NEW* ) References.select (dI', pI', mI') (dI, pI, mI) ( *NEW*)

         val cpI = if pI = Problem.id_empty then pI' else pI;

   	    val cmI = if mI = Method.id_empty then mI' else mI;

   	    val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;

   	    val pre = Pre_Conds.check' "thy 100820" prls where_ pbl;

   	    val preok = foldl and_ (true, map fst pre);

   	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)

         val mpc = (#ppc o Method.from_store) cmI

       in

         case p_ of

 		    (*vvvvvvv---------------------------*)

           Pos.Pbl =>

           (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))

            else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))

            else

              case find_first (I_Model.is_error o #5) pbl of

       	       SOME (_, _, _, fd, itm_) =>

       	         ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory

       	           (if dI = ThyC.id_empty then dI' else dI)) fd itm_))

       	     | NONE => 

       	       (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of

       	          SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))

       	        | NONE => (*pbl-items complete*)

       	          if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))

       	          else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))

       		        else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))

       		        else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))

       		        else

       			        case find_first (I_Model.is_error o #5) met of

       			          SOME (_, _, _, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))

       			        | NONE => 

       			          (case item_to_add (ThyC.get_theory dI) oris mpc met of

       				          SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)

       				        | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))))

 		    (*vvvvvvv---------------------------*)

         | Pos.Met =>

           (case find_first (I_Model.is_error o #5) met of

             SOME (_,_,_, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))

           | NONE => 

             case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of

       	      SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)

             | NONE => 

       	      (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))

       	       else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))

       		     else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))

       		     else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))

         | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)

       end

   end

 (* 

   TODO: unify code with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met

    determine the next step of specification;

    not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))

    eg. in rootpbl 'no_met': 

 args:

   preok          predicates are _all_ ok (and problem matches completely)

   oris           immediately from formalization 

   (dI',pI',mI')  specification coming from author/parent-problem

   (pbl,          item lists specified by user

    met)          -"-, tacitly completed by copy_probl

   (dI,pI,mI)     specification explicitly done by the user

   (pbt, mpc)     problem type, guard of method

 *)

 		(*--------------vvvvvvv *)

 fun find_next_step' Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) = 

     (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')

      else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')

      else

        case find_first (I_Model.is_error o #5) pbl of

 	       SOME (_, _, _, fd, itm_) =>

 	         (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)

 	     | NONE => 

 	       (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of

 	          SOME (fd, ct') => (Pos.Pbl, P_Model.mk_additem fd ct')

 	        | NONE => (*pbl-items complete*)

 	          if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')

 	          else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')

 		        else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')

 		        else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')

 		        else

 			        case find_first (I_Model.is_error o #5) met of

 			          SOME (_, _, _, fd, itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_)

 			        | NONE => 

 			          (case item_to_add (ThyC.get_theory dI) oris mpc met of

 				          SOME (fd, ct') => (Pos.Met, P_Model.mk_additem fd ct') (*30.8.01: pre?!?*)

 				        | NONE => (Pos.Met, Tactic.Apply_Method mI))))

 		(*--------------vvvvvvv *)

   | find_next_step' Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) = 

     (case find_first (I_Model.is_error o #5) met of

       SOME (_,_,_,fd,itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)

     | NONE => 

       case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of

 	      SOME (fd,ct') => (Pos.Met, P_Model.mk_additem fd ct')

       | NONE => 

 	      (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')

 	       else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')

 		     else if not preok then (Pos.Met, Tactic.Specify_Method mI)

 		     else (Pos.Met, Tactic.Apply_Method mI)))

   | find_next_step' p _ _ _ _ _ _ = raise ERROR ("find_next_step': uncovered case with " ^ Pos.pos_2str p)

 fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) = 

       let

         val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)

         val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI

         val cpI = if pI = Problem.id_empty then pI' else pI

         val cmI = if mI = Method.id_empty then mI' else mI

         val {ppc, pre, prls, ...} = Method.from_store cmI

       in 

         case I_Model.check_single ctxt sel oris met ppc ct of

           I_Model.Add itm =>  (*..union old input *)

     	      let

               val met' = I_Model.add_single thy itm met

               val tac' = I_Model.get_tac sel (ct, met')

     	        val (p, pt') =

     	         case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of

     	          ((p, Pos.Met), _, _, pt') => (p, pt')

     	        | _ => raise ERROR "by_tactic': uncovered case of generate1"

     	        val pre' = Pre_Conds.check' thy prls pre met'

     	        val pb = foldl and_ (true, map fst pre')

     	        val (p_, _) = find_next_step' Pos.Met pb oris (dI',pI',mI') (pbl,met') 

     	            ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);

     	      in 

               ("ok", ([], [], (pt', (p, p_))))

             end

         | I_Model.Err msg =>

     	      let

               val pre' = Pre_Conds.check' thy prls pre met

     	        val pb = foldl and_ (true, map fst pre')

     	        val (p_, _) = find_next_step' Pos.Met pb oris (dI',pI',mI') (pbl,met) 

     	          ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);

     	      in

               (msg, ([], [], (pt, (p, p_))))

     	      end

       end

   | by_tactic' sel ct (pt, pos as (p, _(*Frm, Pbl*))) =

       let

         val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)

         val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI

         val cpI = if pI = Problem.id_empty then pI' else pI

         val cmI = if mI = Method.id_empty then mI' else mI

         val {ppc, where_, prls, ...} = Problem.from_store cpI

       in

         case I_Model.check_single ctxt sel oris pbl ppc ct of

           I_Model.Add itm => (*..union old input *)

 	          let

 	            val pbl' = I_Model.add_single thy itm pbl

               val tac' = I_Model.get_tac sel (ct, pbl')

 	            val (p, pt') =

 	              case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

   	              ((p, Pos.Pbl), _, _, pt') => (p, pt')

   	            | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"

   	            (* only for getting final p_ ..*)

 	            val pre = Pre_Conds.check' thy prls where_ pbl';

 	            val pb = foldl and_ (true, map fst pre);

 	            val (p_, _) = find_next_step' Pos.Pbl pb oris (dI',pI',mI')

 	              (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);

 	          in

               ("ok", ([], [], (pt', (p, p_))))

             end

         | I_Model.Err msg =>

 	          let

               val pre = Pre_Conds.check' thy prls where_ pbl

 	            val pb = foldl and_ (true, map fst pre)

 	            val (p_, _(*Tactic.input*)) = find_next_step' Pos.Pbl pb oris (dI', pI', mI')

 	              (pbl, met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)

 	          in

             (msg, ([], [], (pt, (p, p_))))

 	          end

       end

 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}

   -- for input from scratch*)

 fun by_tactic_input' sel ct (ptp as (pt, (p, Pos.Pbl))) = 

     let

       val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of

         Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>

            (oris, dI', pI', dI, pI, pbl, ctxt)

       | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"

       val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;

       val cpI = if pI = Problem.id_empty then pI' else pI;

     in

       case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of

 	      I_Model.Add itm (*..union old input *) =>

 	        let

 	          val pbl' = I_Model.add_single thy itm pbl

 	          val (tac, tac_) = case sel of

 		          "#Given" => (Tactic.Add_Given    ct, Tactic.Add_Given'   (ct, pbl'))

 		        | "#Find"  => (Tactic.Add_Find     ct, Tactic.Add_Find'    (ct, pbl'))

 		        | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))

 		        | sel => raise ERROR ("by_tactic_input': uncovered case of" ^ sel)

 		        val (p, c, pt') =

 		          case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

   		          ((p, Pos.Pbl), c, _, pt') =>  (p, c, pt')

   		        | _ => raise ERROR "by_tactic_input': uncovered case generate1"

 	        in

 	          ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))

           end	       

 	    | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..

                      FIXME ..and dont abuse a tactic for that purpose*)

 	        ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),

 	          (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp) 

     end

   | by_tactic_input' sel ct (ptp as (pt, (p, Pos.Met))) = 

     let

 (*NEW* ) *.specify_data ( *NEW*)

       val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of

         Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>

            (oris, dI', mI', dI, mI, met, ctxt)

       | _ => raise ERROR "by_tactic_input' Met: uncovered case get_obj"

 (*NEW* ) References.select ( *NEW*)

       val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;

       val cmI = if mI = Method.id_empty then mI' else mI;

     in 

       case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of

         I_Model.Add itm (*..union old input *) =>

 	        let

 	          val met' = I_Model.add_single thy itm met;

 	          val (tac,tac_) = case sel of

 		          "#Given" => (Tactic.Add_Given    ct, Tactic.Add_Given'   (ct, met'))

 		        | "#Find"  => (Tactic.Add_Find     ct, Tactic.Add_Find'    (ct, met'))

 		        | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))

 		        | sel => raise ERROR ("by_tactic_input' Met: uncovered case of" ^ sel)

 	          val (p, c, pt') =

 	            case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of

   	            ((p, Pos.Met), c, _, pt') => (p, c, pt')

   		        | _ => raise ERROR "by_tactic_input': uncovered case generate1 (WARNING WHY ?)"

 	        in

 	          ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))

 	        end

       | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)

     end

   | by_tactic_input' _ _ (_, p) = raise ERROR ("by_tactic_input' not impl. for" ^ Pos.pos'2str p)

 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris

   + met from fmz; assumes pos on PblObj, meth = []                    *)

 fun finish_phase (pt, pos as (p, p_)) =

   let

     val _ = if p_ <> Pos.Pbl 

 	    then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)

 	    else ()

 	  val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of

 	    Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)

 	  | _ => raise ERROR "finish_phase: unvered case get_obj"

   	val (_, pI, mI) = References.select ospec spec

   	val mpc = (#ppc o Method.from_store) mI

   	val ppc = (#ppc o Problem.from_store) pI

   	val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)

     val pt = Ctree.update_pblppc pt p pits

 	  val pt = Ctree.update_metppc pt p mits

   in (pt, (p, Pos.Met)) end

 (* do all specification in one single step:

    complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);

    oris and spec (incl. pbl-refinement) given from init_calc or SubProblem

 *)

 fun do_all (pt, (p, _)) =

   let

     val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of

       Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}

         => (pors, dI, pI, mI)

     | _ => raise ERROR "do_all: uncovered case get_obj"

 	  val {ppc, ...} = Method.from_store mI

     val (_, vals) = O_Model.values' pors

 	  val ctxt = ContextC.initialise dI vals

     val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),

       map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)

   in

     (pt, (p, Pos.Met))

   end

 (**)end(**)