1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 18 16:06:00 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Thu May 19 19:28:22 2011 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  		            | UNsafe cs' => ("unsafe-ok", cs')
     1.5  		            | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
     1.6  		                (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
     1.7 -                    (*for SEVER.tacs  user to ask ? *)
     1.8 +                    (*for SEVER.tacs user to ask ? *)
     1.9  	           end
    1.10        end;
    1.11  
    1.12 @@ -403,7 +403,7 @@
    1.13  	    | ("not-applicable",_) => (pt, p)
    1.14  	    | ("end-of-calculation", (_, _, ptp)) => ptp
    1.15  	    | ("failure",_) => error "sys-error";
    1.16 -	  val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
    1.17 +	  val (_, ts) = (*WN101102 TODO: locatetac + step create _same_ (pt,p) ?*)
    1.18  	    (case step p ((pt, e_pos'),[]) of
    1.19  		    ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
    1.20  	    | ("helpless",_) => ("helpless: cannot propose tac", [])
    1.21 @@ -414,8 +414,7 @@
    1.22        case ts of 
    1.23          tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end 
    1.24  		  | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
    1.25 -      (*form output comes from locatetac*)
    1.26 -  in (p:pos', []:NEW, TESTg_form (pt, p), 
    1.27 +  in (p:pos', []:NEW, TESTg_form (pt, p) (*form output comes from locatetac*), 
    1.28  	   (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
    1.29  
    1.30  (*for quick test-print-out, until 'type inout' is removed*)