139 autocalculateOK2xml cI p (if null c then p' else last_elem c) p') |
139 autocalculateOK2xml cI p (if null c then p' else last_elem c) p') |
140 | (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str) |
140 | (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str) |
141 end; |
141 end; |
142 |
142 |
143 fun fetchProposedTactic cI = |
143 fun fetchProposedTactic cI = |
144 case \<^try>\<open> |
144 let |
145 (case Step.do_next (States.get_pos cI 1) (States.get_calc cI) of |
145 val pos = States.get_pos cI 1 |
146 ("ok", (tacis, _, _)) => |
146 val state_pre as ((pt, _), _) = States.get_calc cI |
147 let |
147 val ctxt = Ctree.get_ctxt pt pos |
148 val _ = States.upd_tacis cI tacis |
148 in |
149 val (tac, _, _) = last_elem tacis |
149 case \<^try>\<open> |
150 in |
150 (case Step.do_next pos state_pre of |
151 fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store |
151 ("ok", (tacis, _, _)) => |
152 (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge")) tac) |
152 let |
153 (*ctxt shall become an argument ^^^^^^^^ of fetchProposedTactic*) |
153 val _ = States.upd_tacis cI tacis |
154 end |
154 val (tac, _, _) = last_elem tacis |
155 | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless" |
155 in |
156 | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec" |
156 fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store ctxt tac) |
157 | ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation" |
157 end |
158 | _ => raise ERROR "fetchProposedTactic: undef.case") |
158 | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless" |
159 \<close> of |
159 | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec" |
160 SOME xml => xml |
160 | ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation" |
161 | NONE => sysERROR2xml cI "error in kernel 3"; |
161 | _ => raise ERROR "fetchProposedTactic: undef.case") |
|
162 \<close> of |
|
163 SOME xml => xml |
|
164 | NONE => sysERROR2xml cI "error in kernel 3" |
|
165 end; |
162 |
166 |
163 fun autoCalculate cI auto = (*Future.fork |
167 fun autoCalculate cI auto = (*Future.fork |
164 (fn () => (( *)let |
168 (fn () => (( *)let |
165 val pold = States.get_pos cI 1 |
169 val pold = States.get_pos cI 1 |
166 in |
170 in |
176 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p) |
180 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p) |
177 | (str, _, _) => autocalculateERROR2xml cI str |
181 | (str, _, _) => autocalculateERROR2xml cI str |
178 end (* ) *) |
182 end (* ) *) |
179 handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *); |
183 handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *); |
180 |
184 |
181 fun getTactic cI (p:pos') = |
185 fun getTactic cI (_: pos') = |
182 case \<^try>\<open> |
186 case \<^try>\<open> |
183 let |
187 let |
184 val ((pt, p), _) = States.get_calc cI |
188 val ((pt, p), _) = States.get_calc cI |
185 val ctxt = Ctree.get_ctxt_LI pt p |
189 val ctxt = Ctree.get_ctxt_LI pt p |
186 val (_, tac, _) = ME_Misc.pt_extract ctxt (pt, p) |
190 val (_, tac, _) = ME_Misc.pt_extract ctxt (pt, p) |
208 end |
212 end |
209 \<close> of |
213 \<close> of |
210 SOME xml => xml |
214 SOME xml => xml |
211 | NONE => sysERROR2xml cI "error in kernel 5"; |
215 | NONE => sysERROR2xml cI "error in kernel 5"; |
212 |
216 |
213 fun getAssumptions cI (p:pos') = |
217 fun getAssumptions cI (_: pos') = |
214 case \<^try>\<open> |
218 case \<^try>\<open> |
215 let |
219 let |
216 val ((pt, p), _) = States.get_calc cI |
220 val ((pt, p), _) = States.get_calc cI |
217 val ctxt = Ctree.get_ctxt_LI pt p |
221 val ctxt = Ctree.get_ctxt_LI pt p |
218 val (_, _, asms) = ME_Misc.pt_extract ctxt (pt, p) |
222 val (_, _, asms) = ME_Misc.pt_extract ctxt (pt, p) |