1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed May 11 07:28:13 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Wed May 11 08:25:40 2011 +0200
     1.3 @@ -1568,7 +1568,7 @@
     1.4  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
     1.5          val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
     1.6  				  (pors, (dI, pI, mI), hdl)
     1.7 -          (* val pt = update_env pt [] (SOME (e_istate, pctxt))  GOON.WN110506*)
     1.8 +          (* val pt = update_env pt [] (SOME (e_istate, pctxt)) GOON.WN110506*)
     1.9        in ((pt, ([], Pbl)), 
    1.10          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
    1.11        end;

     2.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 07:28:13 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 08:25:40 2011 +0200
     2.3 @@ -183,16 +183,8 @@
     2.4  	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
     2.5      in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
     2.6  
     2.7 -(*.does a step forward; returns tactic used, ctree updated.
     2.8 -TODO.WN0512 redesign after specify-phase became more separated from solve-phase
     2.9 -arg ip: 
    2.10 -    calcstate
    2.11 -.*)
    2.12 -(* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
    2.13 -   val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);
    2.14 -   val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
    2.15 -   val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
    2.16 -   *)
    2.17 +(* does a step forward; returns tactic used, ctree updated.
    2.18 +TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
    2.19  fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
    2.20    let val pIopt = get_pblID (pt,ip);
    2.21    in
    2.22 @@ -223,24 +215,12 @@
    2.23  			           | cs => ("ok", cs)))
    2.24    end;
    2.25  
    2.26 -(*  (nxt_solve_ (pt,ip)) handle e => print_exn e ;
    2.27 -
    2.28 -   *)
    2.29 -
    2.30 -
    2.31 -
    2.32 -
    2.33  (*.does several steps within one calculation as given by "type auto";
    2.34     the steps may arbitrarily go into and leave different phases, 
    2.35     i.e. specify-phase and solve-phase.*)
    2.36  (*TODO.WN0512 ? redesign after the phases have been more separated
    2.37    at the fron-end in 05: 
    2.38    eg. CompleteCalcHead could be done by a separate fun !!!*)
    2.39 -(* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
    2.40 -   val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI);
    2.41 -   val (c, ip, cs as (ptp as (_,p),tacis), Step s) = 
    2.42 -       ([]:pos' list, pold, get_calc cI, auto);
    2.43 -   *) 
    2.44  fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
    2.45      if s <= 1
    2.46      then let val (str, (_, c', ptp)) = step ip cs;(*1*)
    2.47 @@ -413,8 +393,6 @@
    2.48    NEW loeschen, eigene Version von locatetac, step
    2.49    meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
    2.50  
    2.51 -(* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
    2.52 -   *)
    2.53  fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
    2.54    let 
    2.55      val (pt, p) = 

     3.1 --- a/test/Tools/isac/Test_Isac.thy	Wed May 11 07:28:13 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed May 11 08:25:40 2011 +0200
     3.3 @@ -89,6 +89,42 @@
     3.4  *}
     3.5  
     3.6    use "Interpret/mstools.sml"       (*new 2010*)
     3.7 +
     3.8 +ML {*
     3.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    3.10 +val (dI',pI',mI') =
    3.11 +  ("Test", ["sqroot-test","univariate","equation","test"],
    3.12 +   ["Test","squ-equ-test-subpbl1"]);
    3.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    3.14 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    3.15 +val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
    3.16 +"~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
    3.17 +*}
    3.18 +ML {*
    3.19 +val pIopt = get_pblID (pt,ip);
    3.20 +ip = ([],Res) (*false*);
    3.21 +val SOME pI = pIopt;
    3.22 +member op = [Pbl,Met] p_
    3.23 +			                   andalso is_none (get_obj g_env pt (fst p))
    3.24 +*}
    3.25 +ML {*
    3.26 +*}
    3.27 +ML {*
    3.28 +*}
    3.29 +ML {*
    3.30 +step p ((pt, e_pos'),[]);
    3.31 +*}
    3.32 +ML {*
    3.33 +*}
    3.34 +ML {*
    3.35 +*}
    3.36 +ML {*
    3.37 +*}
    3.38 +ML {*
    3.39 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    3.40 +
    3.41 +*}
    3.42 +
    3.43    use "Interpret/ctree.sml"         (*!...see(25)*)
    3.44    use "Interpret/ptyps.sml"         (*    *)
    3.45  (*use "Interpret/generate.sml"        new 2011*)