1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Wed May 20 12:52:09 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Sun May 24 16:05:36 2020 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    These additional arguments are partially handled by these hacks.
     1.5  *)
     1.6  fun hack_until_review_Specify_1 metID itms = 
     1.7 +(**)
     1.8    if metID = ["Biegelinien", "ausBelastung"]
     1.9    then itms @
    1.10      [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
    1.11 @@ -45,9 +46,10 @@
    1.12          [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
    1.13        (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
    1.14          [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
    1.15 -  else itms
    1.16 +  else (**) itms
    1.17  
    1.18  fun hack_until_review_Specify_2 metID itms = 
    1.19 +(**)
    1.20    if metID = ["IntegrierenUndKonstanteBestimmen2"]
    1.21    then itms @
    1.22      [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
    1.23 @@ -58,7 +60,7 @@
    1.24          [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
    1.25        (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
    1.26          [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
    1.27 -  else itms
    1.28 +  else (**) itms
    1.29  
    1.30  
    1.31  fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
    1.32 @@ -199,16 +201,12 @@
    1.33      (* called only if no_met is specified *)     
    1.34    | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
    1.35        let
    1.36 -(*      val (dI', ctxt) = case get_obj I pt p of
    1.37 -          PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
    1.38 -        | _ => raise ERROR "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
    1.39          val {met, thy,...} = Problem.from_store pIre
    1.40          val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)
    1.41          val ((p,_), _, _, pt) = 
    1.42  	        Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
    1.43              (Istate_Def.Uistate, ContextC.empty) (pt, pos)
    1.44  (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
    1.45 -(*     val (pbl, pre, _) = ([], [], false)*)
    1.46        in 
    1.47          ("ok", ([], [], (pt,(p, Pbl))))
    1.48        end
    1.49 @@ -237,19 +235,30 @@
    1.50      (*WN110515 initialise ctxt again from itms and add preconds*)
    1.51    | by_tactic (Tactic.Specify_Method' (mID, _, _)) (pt,pos as (p, _)) =
    1.52        let
    1.53 -        val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of
    1.54 -          PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
    1.55 -             (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
    1.56 -        | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
    1.57 -        val {ppc, pre, prls,...} = Method.from_store mID
    1.58 -        val thy = ThyC.get_theory dI
    1.59 -        val oris = O_Model.add thy ppc oris
    1.60 -        val met = if met = [] then pbl else met
    1.61 -        val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc, pre, prls) oris
    1.62 -        val itms = hack_until_review_Specify_1 mI' itms
    1.63 -        val (pos, _, _, pt) = 
    1.64 -	        Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
    1.65 -      in
    1.66 +(*OLD*) val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of
    1.67 +(*OLD*)   PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
    1.68 +(*OLD*)      (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
    1.69 +(*OLD*) | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
    1.70 +(*OLD*) val {ppc, pre, prls, ...} = Method.from_store mID
    1.71 +(*OLD*) val thy = ThyC.get_theory dI
    1.72 +(*OLD*) val oris = O_Model.add thy ppc oris
    1.73 +(*OLD*) val met = if met = [] then pbl else met (*nonsense, DEL ! ! ! ! ! ! ! ! ! ! ! ! ! ! !*)
    1.74 +(*OLD*) val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc, pre, prls) oris
    1.75 +(*OLD*) val itms = hack_until_review_Specify_1 mI' itms
    1.76 +(*OLD*) val (pos, _, _, pt) =
    1.77 +(*OLD*)   Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
    1.78 +(*NEW* )
    1.79 +(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
    1.80 +(*NEW*)   Calc.specify_data (pt, pos);
    1.81 +(*NEW*) val (dI, _, mID) = References.select o_refs refs;
    1.82 +(*NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
    1.83 +(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
    1.84 +(*NEW*) val (o_model', ctxt') = O_Model.complete_for_from m_patt o_model (root_model, ctxt)
    1.85 +(*NEW*) val thy = ThyC.get_theory dI
    1.86 +(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_meth (m_patt, pre, prls) o_model';
    1.87 +(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_meth))
    1.88 +(*NEW*)   (Istate_Def.Uistate, ctxt') (pt, pos)
    1.89 +( *NEW*)in
    1.90          ("ok", ([], [], (pt, pos)))
    1.91        end    
    1.92    | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p)  = Specify.by_tactic' "#Given" ct (pt, p)