418 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) = |
418 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) = |
419 (case (implode o (take_fromto 1 4) o explode) guh of |
419 (case (implode o (take_fromto 1 4) o explode) guh of |
420 "thy_" => |
420 "thy_" => |
421 (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify"); |
421 (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify"); |
422 *) |
422 *) |
423 if member op = p_ [Pbl,Met] |
423 if member op = [Pbl,Met] p_ |
424 then message2xml cI "thy-context not to calchead" |
424 then message2xml cI "thy-context not to calchead" |
425 else if ip = ([],Res) then message2xml cI "no thy-context at result" |
425 else if ip = ([],Res) then message2xml cI "no thy-context at result" |
426 else if no_thycontext guh then message2xml cI ("no thy-context for '"^ |
426 else if no_thycontext guh then message2xml cI ("no thy-context for '"^ |
427 guh ^ "'") |
427 guh ^ "'") |
428 else let val (ptp as (pt,pold),_) = get_calc cI |
428 else let val (ptp as (pt,pold),_) = get_calc cI |
490 fun setMethod (cI:calcID) (mI:metID) = |
490 fun setMethod (cI:calcID) (mI:metID) = |
491 (* val (cI, mI) = (1, ["Test","solve_linear"]); |
491 (* val (cI, mI) = (1, ["Test","solve_linear"]); |
492 *) |
492 *) |
493 (let val ((pt, _), _) = get_calc cI |
493 (let val ((pt, _), _) = get_calc cI |
494 val ip as (_, p_) = get_pos cI 1 |
494 val ip as (_, p_) = get_pos cI 1 |
495 in if member op = p_ [Pbl,Met] |
495 in if member op = [Pbl,Met] p_ |
496 then let val (pt, chd) = set_method mI (pt, ip) |
496 then let val (pt, chd) = set_method mI (pt, ip) |
497 in (upd_calc cI ((pt, ip), []); |
497 in (upd_calc cI ((pt, ip), []); |
498 modifycalcheadOK2xml cI chd) end |
498 modifycalcheadOK2xml cI chd) end |
499 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead" |
499 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead" |
500 end) |
500 end) |
504 containing the Model; special case of checkContext; |
504 containing the Model; special case of checkContext; |
505 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*) |
505 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*) |
506 fun setProblem (cI:calcID) (pI:pblID) = |
506 fun setProblem (cI:calcID) (pI:pblID) = |
507 (let val ((pt, _), _) = get_calc cI |
507 (let val ((pt, _), _) = get_calc cI |
508 val ip as (_, p_) = get_pos cI 1 |
508 val ip as (_, p_) = get_pos cI 1 |
509 in if member op = p_ [Pbl,Met] |
509 in if member op = [Pbl,Met] p_ |
510 then let val (pt, chd) = set_problem pI (pt, ip) |
510 then let val (pt, chd) = set_problem pI (pt, ip) |
511 in (upd_calc cI ((pt, ip), []); |
511 in (upd_calc cI ((pt, ip), []); |
512 modifycalcheadOK2xml cI chd) end |
512 modifycalcheadOK2xml cI chd) end |
513 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead" |
513 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead" |
514 end) |
514 end) |
518 special case of checkContext; |
518 special case of checkContext; |
519 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*) |
519 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*) |
520 fun setTheory (cI:calcID) (tI:thyID) = |
520 fun setTheory (cI:calcID) (tI:thyID) = |
521 (let val ((pt, _), _) = get_calc cI |
521 (let val ((pt, _), _) = get_calc cI |
522 val ip as (_, p_) = get_pos cI 1 |
522 val ip as (_, p_) = get_pos cI 1 |
523 in if member op = p_ [Pbl,Met] |
523 in if member op = [Pbl,Met] p_ |
524 then let val (pt, chd) = set_theory tI (pt, ip) |
524 then let val (pt, chd) = set_theory tI (pt, ip) |
525 in (upd_calc cI ((pt, ip), []); |
525 in (upd_calc cI ((pt, ip), []); |
526 modifycalcheadOK2xml cI chd) end |
526 modifycalcheadOK2xml cI chd) end |
527 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead" |
527 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead" |
528 end) |
528 end) |
735 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res)); |
735 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res)); |
736 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res)); |
736 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res)); |
737 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm)); |
737 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm)); |
738 *) |
738 *) |
739 fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') = |
739 fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') = |
740 ((if member op = p_ [Pbl,Met] |
740 ((if member op = [Pbl,Met] p_ |
741 then message2xml cI "thy-context not to calchead" |
741 then message2xml cI "thy-context not to calchead" |
742 else if pos = ([],Res) then message2xml cI "no thy-context at result" |
742 else if pos = ([],Res) then message2xml cI "no thy-context at result" |
743 else let val cs as (ptp as (pt,_),_) = get_calc cI |
743 else let val cs as (ptp as (pt,_),_) = get_calc cI |
744 in if exist_lev_on' pt pos |
744 in if exist_lev_on' pt pos |
745 then let val pos' = lev_on' pt pos |
745 then let val pos' = lev_on' pt pos |
797 (1, ([1], Res), "thy_isac_Test-rls-Test_simplify"); |
797 (1, ([1], Res), "thy_isac_Test-rls-Test_simplify"); |
798 *) |
798 *) |
799 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) = |
799 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) = |
800 (case (implode o (take_fromto 1 4) o explode) guh of |
800 (case (implode o (take_fromto 1 4) o explode) guh of |
801 "thy_" => |
801 "thy_" => |
802 if member op = p_ [Pbl,Met] |
802 if member op = [Pbl,Met] p_ |
803 then message2xml cI "thy-context not to calchead" |
803 then message2xml cI "thy-context not to calchead" |
804 else if pos = ([],Res) then message2xml cI "no thy-context at result" |
804 else if pos = ([],Res) then message2xml cI "no thy-context at result" |
805 else if no_thycontext guh then message2xml cI ("no thy-context for '"^ |
805 else if no_thycontext guh then message2xml cI ("no thy-context for '"^ |
806 guh ^ "'") |
806 guh ^ "'") |
807 else let val (ptp as (pt,_),_) = get_calc cI |
807 else let val (ptp as (pt,_),_) = get_calc cI |