diff -r 80ad50a9e541 -r b95f0dde56c1 test/Tools/isac/Interpret/script.sml
--- a/test/Tools/isac/Interpret/script.sml	Fri Sep 23 09:41:11 2011 +0200
+++ b/test/Tools/isac/Interpret/script.sml	Fri Sep 23 13:58:27 2011 +0200
@@ -6,12 +6,11 @@
 "table of contents -----------------------------------------------";
 "-----------------------------------------------------------------";
 "----------- WN0509 why does next_tac doesnt find Substitute -----";
-"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
 "----------- WN0509 Substitute 2nd part --------------------------";
 "----------- fun sel_appl_atomic_tacs ----------------------------";
 "----------- fun init_form, fun get_stac -------------------------";
 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
-"----------- x+1=2 set ctxt in Subproblem ------------------------";
+"----------- Take as 1st stac in script --------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
@@ -80,66 +79,6 @@
 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
 ---------------------------------------------------------------------*)
 
-"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
-"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
-"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
-(*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
-val fmz = ["Traegerlaenge L",
-	   "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
-	   "Biegelinie y",
-	   "RandbedingungenBiegung [y 0 = 0, y L = 0]",
-	   "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
-	   "FunktionsVariable x"];
-val (dI',pI',mI') =
-  ("Biegelinie",["MomentBestimmte","Biegelinien"],
-   ["IntegrierenUndKonstanteBestimmen"]);
-val p = e_pos'; val c = [];
-val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
-val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
-val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
-val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
-val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
-val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
-val (p,_,f,nxt,_,pt) = me nxt p c pt;
-val (p,_,f,nxt,_,pt) = me nxt p c pt;
-
-case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
-	  | _ => error "script.sml, doesnt find Substitute #2";
-
-(*========== inhibit exn AK110721 ================================================
-
-(* AK110722 f2str f is NOT working anywhere - deprecated?????*)
-
-(*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
-  (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised 
-            (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
-(*f2str f;
-  (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
-(* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
-  (* ERROR: exception Bind raised *)*)
-
- f;
- f2str;*)
-
-(* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
-(* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
-
-val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
-(* *** generate1: not impl.for Empty_Tac_  !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
-val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
-val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
-val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
-(*---------------------------------------------------------------------*)
-
-case nxt of (_, End_Proof') => () 
-	  | _ => error "script.sml, doesnt find Substitute #3";
-(*---------------------------------------------------------------------*)
-(*the reason, that next_tac didnt find the 2nd Substitute, was that
-  the Take inbetween was missing, and thus the 2nd Substitute was applied
-  the last formula in ctree, and not to argument from script*)
-========== inhibit exn AK110721 ================================================*)
-
-
 "----------- WN0509 Substitute 2nd part --------------------------";
 "----------- WN0509 Substitute 2nd part --------------------------";
 "----------- WN0509 Substitute 2nd part --------------------------";
@@ -419,6 +358,58 @@
 | _ => error "script.sml x+1=2 start SubProblem from script";
 
 
-"----------- x+1=2 set ctxt in Subproblem ------------------------";
-"----------- x+1=2 set ctxt in Subproblem ------------------------";
-"----------- x+1=2 set ctxt in Subproblem ------------------------";
+"----------- Take as 1st stac in script --------------------------";
+"----------- Take as 1st stac in script --------------------------";
+"----------- Take as 1st stac in script --------------------------";
+val p = e_pos'; val c = []; 
+val (p,_,f,nxt,_,pt) = 
+    CalcTreeTEST 
+        [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
+          ("Integrate", ["integrate","function"], ["diff","integration"]))];
+val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt;
+case nxt of (_, Apply_Method ["diff", "integration"]) => ()
+          | _ => error "integrate.sml -- me method [diff,integration] -- spec";
+"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
+
+"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
+"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
+val (mI,m) = mk_tac'_ tac;
+val Appl m = applicable_in p pt m;
+member op = specsteps mI (*false*);
+"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
+"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = 
+                            (m, (pt, pos));
+val {srls, ...} = get_met mI;
+        val PblObj {meth=itms, ...} = get_obj I pt p;
+        val thy' = get_obj g_domID pt p;
+        val thy = assoc_thy thy';
+        val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
+        val ini = init_form thy sc env;
+        val p = lev_dn p;
+ini = NONE; (*true*)
+            val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
+	            val d = e_rls (*FIXME: get simplifier from domID*);
+"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 
+	                     (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
+                   ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
+val thy = assoc_thy thy';
+l = [] orelse ((*init.in solve..Apply_Method...*)
+			         (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
+"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss), 
+                   (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = 
+                 ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
+ (*check: true*) term2str e = "Take (Integral f_f D v_v)";
+"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = 
+                           (ya, ((E , l@[L,R], a,v,S,b),ss), e);
+val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
+(*             val ctxt = get_ctxt pt (p,p_)
+exception PTREE "get_obj: pos = [0] does not exist" raised 
+(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
+
+