1.1 --- a/src/sml/ME/mathengine.sml	Wed Oct 19 17:24:10 2005 +0200
     1.2 +++ b/src/sml/ME/mathengine.sml	Wed Oct 19 19:14:45 2005 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  
     1.5  
     1.6  (*
     1.7 -structure mathengine : MATHENGINE =
     1.8 +structure MathEngine : MATHENGINE =
     1.9  struct
    1.10  *)
    1.11  fun get_pblID (pt, (p,_):pos') =
    1.12 @@ -433,6 +433,7 @@
    1.13  	      | ("not-applicable",_) => (pt, p)
    1.14  	      | ("end-of-calculation", (_, _, ptp)) => ptp
    1.15  	      | ("failure",_) => raise error "sys-error";
    1.16 +	val _= writeln("### me after locatetac");
    1.17  	val (_, ts) = 
    1.18  (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
    1.19     *)
    1.20 @@ -443,16 +444,22 @@
    1.21  	       | ("no-fmz-spec",_) => raise error "no-fmz-spec"
    1.22  	       | ("end-of-calculation", (ts, _, _)) => ("",ts))
    1.23  	    handle _ => raise error "sys-error";
    1.24 +	val _= writeln("### me after step");
    1.25  	val tac = case ts of ((tac,_,_)::_) => tac 
    1.26  			   | _ => if p = ([],Res) then End_Proof'
    1.27  				  else Empty_Tac;
    1.28        (*form output comes from locatetac*)
    1.29 -    in (p:pos',[]:NEW, TESTg_form (pt, p), 
    1.30 -	(tac2IDstr tac, tac):tac'_, Sundef, pt) end;
    1.31 -(*
    1.32 +	val _= writeln("### me after tac")
    1.33 +	val xxx = (p:pos',[]:NEW, TESTg_form (pt, p), 
    1.34 +	(tac2IDstr tac, tac):tac'_, Sundef, pt)
    1.35 +    in writeln("### me in in"); xxx end;
    1.36 +
    1.37 +(*for quick test-print-out, until 'type inout' is removed*)
    1.38 +fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
    1.39 +
    1.40 +(*------------------------------------------------------------------
    1.41  end
    1.42  
    1.43 -open mathengine;
    1.44 -*)
    1.45 +open MathEngine;
    1.46 +------------------------------------------------------------------*)
    1.47  
    1.48 -fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';