1.1 --- a/src/Tools/isac/Interpret/solve.sml	Tue May 03 16:23:07 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Wed May 04 09:01:10 2011 +0200
     1.3 @@ -408,19 +408,18 @@
     1.4     val (ptp as (pt, pos as (p,p_))) = (pt, pos);
     1.5     *)
     1.6  and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
     1.7 -    if e_metID = get_obj g_metID pt (par_pblobj pt p)
     1.8 -    then ([], [], (pt,(p,p_))):calcstate'
     1.9 -    else let val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.10 -	     val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.11 -	     val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
    1.12 -	 (*TODO here ^^^  return finished/helpless/ok !*)
    1.13 -	 (* val (tac_',is',(t',_)) = next_tac (thy',srls) (pt,pos) sc is;
    1.14 -	    *)
    1.15 -	 in case tac_ of
    1.16 -		End_Detail' _ => ([(End_Detail, 
    1.17 -				    End_Detail' (t,[(*FIXME.040215*)]), 
    1.18 -				    (pos, is))], [], (pt, pos))
    1.19 -	      | _ => nxt_solv tac_ is ptp end;
    1.20 +      if e_metID = get_obj g_metID pt (par_pblobj pt p)
    1.21 +      then ([], [], (pt,(p,p_))):calcstate'
    1.22 +      else 
    1.23 +        let 
    1.24 +          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.25 +	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    1.26 +	        val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
    1.27 +	        (*TODO here ^^^  return finished/helpless/ok !*)
    1.28 +	      in case tac_ of
    1.29 +		         End_Detail' _ => ([(End_Detail, End_Detail' (t,[(*FIXME.040215*)]), 
    1.30 +				       (pos, is))], [], (pt, pos))
    1.31 +	         | _ => nxt_solv tac_ is ptp end;
    1.32  
    1.33  (*.says how may steps of a calculation should be done by "fun autocalc".*)
    1.34  (*TODO.WN0512 redesign togehter with autocalc ?*)