80 let |
80 let |
81 val cpI = if pI = Problem.id_empty then pI' else pI; |
81 val cpI = if pI = Problem.id_empty then pI' else pI; |
82 val cmI = if mI = MethodC.id_empty then mI' else mI; |
82 val cmI = if mI = MethodC.id_empty then mI' else mI; |
83 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
83 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
84 val {model = mpc, ...} = MethodC.from_store ctxt cmI |
84 val {model = mpc, ...} = MethodC.from_store ctxt cmI |
85 val (preok, _) = Pre_Conds.check where_rls where_ pbl 0; |
85 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0; |
86 in |
86 in |
87 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then |
87 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then |
88 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) |
88 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) |
89 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then |
89 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then |
90 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI')) |
90 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI')) |
115 |
115 |
116 fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = |
116 fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = |
117 let |
117 let |
118 val cmI = if mI = MethodC.id_empty then mI' else mI; |
118 val cmI = if mI = MethodC.id_empty then mI' else mI; |
119 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; |
119 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; |
120 val (preok, _) = Pre_Conds.check where_rls where_ pbl 0; |
120 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0; |
121 in |
121 in |
122 (case find_first (I_Model.is_error o #5) met of |
122 (case find_first (I_Model.is_error o #5) met of |
123 SOME (_,_,_, fd, itm_) => |
123 SOME (_,_,_, fd, itm_) => |
124 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt |
124 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt |
125 (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) |
125 (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) |