equal
deleted
inserted
replaced
441 val cs = get_calc cI |
441 val cs = get_calc cI |
442 val pos = get_pos cI 1 |
442 val pos = get_pos cI 1 |
443 in |
443 in |
444 case Math_Engine.step pos cs of |
444 case Math_Engine.step pos cs of |
445 ("ok", cs') => |
445 ("ok", cs') => |
446 (case LucinNEW.locate_input_formula cs' (encode ifo) of |
446 (case Solve.inform cs' (encode ifo) of |
447 ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) => |
447 ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) => |
448 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
448 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
449 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p) |
449 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p) |
450 | ("same-formula", (_, c, ptp as (_, p))) => |
450 | ("same-formula", (_, c, ptp as (_, p))) => |
451 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
451 (upd_calc cI (ptp, []); upd_ipos cI 1 p; |
461 fun replaceFormula cI ifo = |
461 fun replaceFormula cI ifo = |
462 (let |
462 (let |
463 val ((pt, _), _) = get_calc cI |
463 val ((pt, _), _) = get_calc cI |
464 val p = get_pos cI 1 |
464 val p = get_pos cI 1 |
465 in |
465 in |
466 case LucinNEW.locate_input_formula (([], [], (pt, p)): Chead.calcstate') (encode ifo) of |
466 case Solve.inform (([], [], (pt, p)): Chead.calcstate')(encode ifo) of |
467 ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) => |
467 ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) => |
468 let |
468 let |
469 val unc = if null (fst p) then p else move_up [] pt p |
469 val unc = if null (fst p) then p else move_up [] pt p |
470 val _ = upd_calc cI (ptp', []) |
470 val _ = upd_calc cI (ptp', []) |
471 val _ = upd_ipos cI 1 p' |
471 val _ = upd_ipos cI 1 p' |