diff -r a393bb9f5e9f -r 977788dfed26 test/Tools/isac/Interpret/script.sml
--- a/test/Tools/isac/Interpret/script.sml	Wed Mar 14 17:12:43 2012 +0100
+++ b/test/Tools/isac/Interpret/script.sml	Sat Mar 17 11:06:46 2012 +0100
@@ -11,6 +11,7 @@
 "----------- fun init_form, fun get_stac -------------------------";
 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
 "----------- Take as 1st stac in script --------------------------";
+"----------- 'trace_script' from outside 'fun me '----------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
@@ -399,3 +400,98 @@
 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
 
 
+"----------- 'trace_script' from outside 'fun me '----------------";
+"----------- 'trace_script' from outside 'fun me '----------------";
+"----------- 'trace_script' from outside 'fun me '----------------";
+val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
+val (dI',pI',mI') =
+   ("Test", ["sqroot-test","univariate","equation","test"],
+    ["Test","squ-equ-test-subpbl1"]);
+val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
+(*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
+
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+f2str f = "x + 1 = 2";          snd nxt = Rewrite_Set "norm_equation";
+val (p, p_) = p(* = ([1], Frm)*);
+val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
+val (env, loc_, curry_arg, res, Safe, true) = scrstate;
+  env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
+  loc_ = [];
+  curry_arg = NONE;
+  term2str res = "??.empty";                     (* scrstate before starting interpretation *)
+(*term2str (go loc_ sc) = "Script Solve_root_equation e_e v_v = ...*)
+
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify";
+val (p, p_) = p(* = ([1], Res)*);
+val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
+val (env, loc_, curry_arg, res, Safe, true) = scrstate;
+  env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
+  loc_ = [R, L, R, L, L, R, R];
+  curry_arg = SOME (str2term "e_e::bool");
+  term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *)
+term2str (go loc_ sc) = "Rewrite_Set norm_equation False";
+
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]);
+val (p, p_) = p(* = ([2], Res)*);
+val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
+val (env, loc_, curry_arg, res, Safe, false) = scrstate;
+  env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
+  loc_ = [R, L, R, L, R, R];
+  curry_arg = SOME (str2term "e_e::bool");
+  term2str res = "-1 + x = 0";           (* scrstate after Test_simplify, before Subproblem *)
+term2str (go loc_ sc) = "Rewrite_Set Test_simplify False";
+
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);     (*f2str f = exception Match; ...is a model, not a formula*)
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*)
+(*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
+
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv");
+val (p, p_) = p(* = ([3, 1], Frm)*);
+val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
+val (env, loc_, curry_arg, res, Safe, true) = scrstate;
+  env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
+  loc_ = [];
+  curry_arg = NONE;
+  term2str res = "??.empty";                     (* scrstate before starting interpretation *)
+(*term2str (go loc_ sc) = "Script Solve_linear e_e v_v = ...*)
+
+val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
+val (p'''', pt'''') = (p, pt);
+f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify";
+val (p, p_) = p(* = ([3, 1], Res)*);
+val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
+val (env, loc_, curry_arg, res, Safe, true) = scrstate;
+  env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
+  loc_ = [R, L, R, L, R, L, R];
+  curry_arg = SOME (str2term "e_e::bool");
+  term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
+term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
+
+