1.1 --- a/src/sml/FE-interface/interface.sml Fri Feb 11 17:06:17 2005 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Fri Feb 11 18:15:10 2005 +0100
1.3 @@ -147,9 +147,9 @@
1.4 @see #TACTICS_ALL
1.5 @see #TACTICS_CURRENT_THEORY
1.6 @see #TACTICS_CURRENT_METHOD ..the only impl.WN.040307.*)
1.7 -fun fetchApplicableTactics cI scope =
1.8 +fun fetchApplicableTactics cI (p:pos') (*scope*) =
1.9 let val ((pt, _), _) = get_calc cI
1.10 - val p = get_pos cI 1
1.11 + (*val p = get_pos cI 1*)
1.12 in (applicabletacticsOK cI (sel_rules pt p))
1.13 handle _ => sysERROR2xml cI "syserror in getApplicableTactics" end;
1.14
1.15 @@ -158,12 +158,15 @@
1.16 val (_, _, asms) = pt_extract (pt, p)
1.17 in getasmsOK2xml cI asms end)
1.18 handle _ => sysERROR2xml cI "syserror in getAssumptions";
1.19 -(*
1.20 +
1.21 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
1.22 fun getAccumulatedAsms cI (p:pos') =
1.23 (let val ((pt, _), _) = get_calc cI
1.24 - in accuasmsOK2xml cI (get_assumptions_ pt p) end)
1.25 - handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms" end;
1.26 -*)
1.27 + val ass = map fst (get_assumptions_ pt p)
1.28 + in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
1.29 + getasmsOK2xml cI ass end)
1.30 + handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
1.31 +
1.32
1.33 (*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
1.34 refFormula might become involved in far-off errors !!!*)
2.1 --- a/src/sml/ROOT.ML Fri Feb 11 17:06:17 2005 +0100
2.2 +++ b/src/sml/ROOT.ML Fri Feb 11 18:15:10 2005 +0100
2.3 @@ -75,7 +75,7 @@
2.4
2.5 *)
2.6
2.7 - val version_kernel = "sml-050210b";
2.8 + val version_kernel = "sml-050211c-menu-finished";
2.9
2.10 print_depth 3;
2.11
3.1 --- a/src/sml/systest/FE-interface.sml Fri Feb 11 17:06:17 2005 +0100
3.2 +++ b/src/sml/systest/FE-interface.sml Fri Feb 11 18:15:10 2005 +0100
3.3 @@ -823,6 +823,7 @@
3.4 moveActiveDown 1;
3.5 moveActiveDown 1; (*-1 + x = 0*);
3.6
3.7 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
3.8 interSteps 1 ([2],Res);
3.9
3.10 moveActiveUp 1;
3.11 @@ -847,7 +848,8 @@
3.12 "--------- getTactic, fetchApplicableTactics ---------------------";
3.13 "--------- getTactic, fetchApplicableTactics ---------------------";
3.14 states:=[];
3.15 - CalcTree
3.16 + CalcTree(**)
3.17 +
3.18 [(["equality (x+1=2)", "solveFor x","solutions L"],
3.19 ("Test.thy",
3.20 ["sqroot-test","univariate","equation","test"],
3.21 @@ -857,12 +859,14 @@
3.22 val ((pt,_),_) = get_calc 1;
3.23 show_pt pt;
3.24
3.25 - fetchApplicableTactics 1 3
3.26 - (*TACTICS_CURRENT_METHOD^^^ the only one impl.WN.040307*);
3.27 - moveActiveUp 1;
3.28 - moveActiveUp 1;
3.29 - moveActiveUp 1;
3.30 - fetchApplicableTactics 1 3;
3.31 + (*UC\label{SOLVE:HIDE:getTactic}*)
3.32 + getTactic 1 ([1],Res);
3.33 + getTactic 1 ([2],Res);
3.34 + getTactic 1 ([],Res);
3.35 +
3.36 +(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
3.37 + fetchApplicableTactics 1 ([],Frm) ;
3.38 + fetchApplicableTactics 1 ([3,1],Frm);
3.39
3.40
3.41 "--------- getAssumptions, getAccumulatedAsms --------------------";
3.42 @@ -878,9 +882,12 @@
3.43 val ((pt,_),_) = get_calc 1;
3.44 show_pt pt;
3.45
3.46 +(*UC\label{SOLVE:HELP:assumptions}*)
3.47 getAssumptions 1 ([3], Res);
3.48 -
3.49 -
3.50 +getAssumptions 1 ([5], Res);
3.51 +(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
3.52 +getAccumulatedAsms 1 ([3], Res);
3.53 +getAccumulatedAsms 1 ([5], Res);
3.54
3.55
3.56 "--------- arbitrary combinations of steps -----------------------";
4.1 --- a/src/sml/xmlsrc/datatypes.sml Fri Feb 11 17:06:17 2005 +0100
4.2 +++ b/src/sml/xmlsrc/datatypes.sml Fri Feb 11 18:15:10 2005 +0100
4.3 @@ -57,6 +57,7 @@
4.4 (* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
4.5 *)
4.6
4.7 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
4.8 fun posform2xml j (p:pos', term) =
4.9 (indt j ^ "<POSFORM>\n" ^
4.10 pos'2xml (j+i) ("POSITION", p) ^
5.1 --- a/src/sml/xmlsrc/interface-xml.sml Fri Feb 11 17:06:17 2005 +0100
5.2 +++ b/src/sml/xmlsrc/interface-xml.sml Fri Feb 11 18:15:10 2005 +0100
5.3 @@ -125,17 +125,20 @@
5.4 \@@@@@end@@@@@");
5.5 (* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
5.6 *)
5.7 +
5.8 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
5.9 fun getaccuasmsOK2xml cI asms =
5.10 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
5.11 \<GETACCUMULATEDASMS>\n\
5.12 \ <CALCID> "^string_of_int cI^" </CALCID>\n\
5.13 - \ <POSASMLIST>\n"^
5.14 - posforms2xml (i+i) asms^
5.15 - " </POSASMLIST>\n\
5.16 + \ <ASMLIST>\n"^
5.17 + formulae2xml (i+i) asms^
5.18 + " </ASMLIST>\n\
5.19 \</GETACCUMULATEDASMS>\n\
5.20 \@@@@@end@@@@@");
5.21 (* getaccuasmsOK2xml 333 [(([1],Res), str2term "1+1=2"),
5.22 (([2],Res), str2term "1+1+1=3")];
5.23 + getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
5.24 *)
5.25
5.26 fun getintervalOK (cI:calcID) fs =