179 fun fetchProposedTactic (cI:calcID) = |
179 fun fetchProposedTactic (cI:calcID) = |
180 (case step (get_pos cI 1) (get_calc cI) of |
180 (case step (get_pos cI 1) (get_calc cI) of |
181 ("ok", (tacis, _, _)) => |
181 ("ok", (tacis, _, _)) => |
182 let val _= upd_tacis cI tacis |
182 let val _= upd_tacis cI tacis |
183 val (tac,_,_) = last_elem tacis |
183 val (tac,_,_) = last_elem tacis |
184 in fetchproposedtacticOK2xml cI tac end |
184 in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end |
185 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless" |
185 | ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless" |
186 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec" |
186 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec" |
187 | ("end-of-calculation",_) => |
187 | ("end-of-calculation",_) => |
188 fetchproposedtacticERROR2xml cI "end-of-calculation") |
188 fetchproposedtacticERROR2xml cI "end-of-calculation") |
189 handle _ => sysERROR2xml cI "error in kernel"; |
189 handle _ => sysERROR2xml cI "error in kernel"; |