1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 04 14:07:51 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Thu May 05 09:23:32 2011 +0200
     1.3 @@ -111,29 +111,23 @@
     1.4  (*. locate a tactic in a script and apply it if possible .*)
     1.5  (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
     1.6  fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
     1.7 -(* val ptp as (pt, p) = (pt, p);
     1.8 -   val ptp as (pt, p) = (pt, ip);
     1.9 -   *)
    1.10    | locatetac tac (ptp as (pt, p)) =
    1.11 -    let val (mI,m) = mk_tac'_ tac;
    1.12 -    in case applicable_in p pt m of
    1.13 -	   Notappl e => ("not-applicable", ([],[],  ptp):calcstate')
    1.14 -	 | Appl m =>
    1.15 -(* val Appl m = applicable_in p pt m;
    1.16 -    *) 
    1.17 -	   let val x = if member op = specsteps mI
    1.18 -		       then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
    1.19 -	   in case x of 
    1.20 -		  ERror e => ("failure", ([], [], ptp))
    1.21 -		(*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
    1.22 -		| UNsafe cs' => ("unsafe-ok", cs')
    1.23 -		| Updated (cs' as (_,_,(_,p'))) =>
    1.24 -		  (*ev.SEVER.tacs like Begin_Trans*)
    1.25 -		  (if p' = ([],Res) then "end-of-calculation" else "ok", 
    1.26 -		   cs')(*for -"-  user to ask ? *)
    1.27 -	   end
    1.28 -    end;
    1.29 -
    1.30 +      let val (mI,m) = mk_tac'_ tac;
    1.31 +      in case applicable_in p pt m of
    1.32 +	         Notappl e => ("not-applicable", ([],[],  ptp):calcstate')
    1.33 +	       | Appl m =>
    1.34 +	           let 
    1.35 +               val x = if member op = specsteps mI
    1.36 +		             then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
    1.37 +	           in case x of 
    1.38 +		              ERror e => ("failure", ([], [], ptp))
    1.39 +		              (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
    1.40 +		            | UNsafe cs' => ("unsafe-ok", cs')
    1.41 +		            | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
    1.42 +		                (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
    1.43 +                    (*for SEVER.tacs  user to ask ? *)
    1.44 +	           end
    1.45 +      end;
    1.46  
    1.47  (*------------------------------------------------------------------
    1.48  fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)