1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 07:28:13 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 08:25:40 2011 +0200
     1.3 @@ -183,16 +183,8 @@
     1.4  	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
     1.5      in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
     1.6  
     1.7 -(*.does a step forward; returns tactic used, ctree updated.
     1.8 -TODO.WN0512 redesign after specify-phase became more separated from solve-phase
     1.9 -arg ip: 
    1.10 -    calcstate
    1.11 -.*)
    1.12 -(* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
    1.13 -   val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);
    1.14 -   val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
    1.15 -   val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
    1.16 -   *)
    1.17 +(* does a step forward; returns tactic used, ctree updated.
    1.18 +TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
    1.19  fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
    1.20    let val pIopt = get_pblID (pt,ip);
    1.21    in
    1.22 @@ -223,24 +215,12 @@
    1.23  			           | cs => ("ok", cs)))
    1.24    end;
    1.25  
    1.26 -(*  (nxt_solve_ (pt,ip)) handle e => print_exn e ;
    1.27 -
    1.28 -   *)
    1.29 -
    1.30 -
    1.31 -
    1.32 -
    1.33  (*.does several steps within one calculation as given by "type auto";
    1.34     the steps may arbitrarily go into and leave different phases, 
    1.35     i.e. specify-phase and solve-phase.*)
    1.36  (*TODO.WN0512 ? redesign after the phases have been more separated
    1.37    at the fron-end in 05: 
    1.38    eg. CompleteCalcHead could be done by a separate fun !!!*)
    1.39 -(* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
    1.40 -   val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI);
    1.41 -   val (c, ip, cs as (ptp as (_,p),tacis), Step s) = 
    1.42 -       ([]:pos' list, pold, get_calc cI, auto);
    1.43 -   *) 
    1.44  fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
    1.45      if s <= 1
    1.46      then let val (str, (_, c', ptp)) = step ip cs;(*1*)
    1.47 @@ -413,8 +393,6 @@
    1.48    NEW loeschen, eigene Version von locatetac, step
    1.49    meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
    1.50  
    1.51 -(* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
    1.52 -   *)
    1.53  fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
    1.54    let 
    1.55      val (pt, p) =