equal
deleted
inserted
replaced
159 setnexttactic2xml cI "end-of-calculation" |
159 setnexttactic2xml cI "end-of-calculation" |
160 | ("failure",_) => sysERROR2xml cI "failure" |
160 | ("failure",_) => sysERROR2xml cI "failure" |
161 end; |
161 end; |
162 |
162 |
163 (*. apply a tactic at a position and update the calc-tree if applicable .*) |
163 (*. apply a tactic at a position and update the calc-tree if applicable .*) |
|
164 (* val (cI, ip, tac) = (1, p, hd appltacs); |
|
165 *) |
164 fun applyTactic (cI:calcID) ip tac = |
166 fun applyTactic (cI:calcID) ip tac = |
165 let val ((pt, _), _) = get_calc cI |
167 let val ((pt, _), _) = get_calc cI |
166 val p = get_pos cI 1 |
168 val p = get_pos cI 1 |
167 in case locatetac tac (pt, ip) of |
169 in case locatetac tac (pt, ip) of |
168 (* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip); |
170 (* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip); |