1.1 --- a/src/Tools/isac/Frontend/interface.sml	Tue Jul 01 16:08:32 2014 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Tue Jul 01 16:10:52 2014 +0200
     1.3 @@ -239,8 +239,6 @@
     1.4      (let val ((pt,_),_) = get_calc cI
     1.5  	 val (form, tac, asms) = pt_extract (pt, p)
     1.6      in case tac of
     1.7 -(* val SOME ta = tac;
     1.8 -   *)
     1.9  	   SOME ta => gettacticOK2xml cI ta
    1.10  	 | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
    1.11       end)
    1.12 @@ -334,32 +332,22 @@
    1.13      sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\
    1.14  		    \i.e. last arg only impl. for false, _NOT_ true";
    1.15  
    1.16 -
    1.17 -(* val (cI, ip) = (1, ([1,9], Res));
    1.18 -   val (cI, ip) = (1, ([], Res));
    1.19 -   val (cI, ip) = (1, ([2], Res));
    1.20 -   val (cI, ip) = (1, ([3,1], Res));
    1.21 -   val (cI, ip) = (1, ([1,2,1], Res));
    1.22 -   *)
    1.23  fun interSteps cI ip =
    1.24 -    (let val ((pt,p), tacis) = get_calc cI
    1.25 -     in if (not o is_interpos) ip
    1.26 -	then interStepsERROR cI "only formulae with position (_,Res) \
    1.27 -				\may have intermediate steps above them"
    1.28 -	else let val ip' = lev_pred' pt ip
    1.29 -(* val (str, pt', lastpos) = detailstep pt ip;
    1.30 -   *)
    1.31 -	     in case detailstep pt ip of
    1.32 -		    ("detailrls", pt(*, pos'forms*), lastpos) =>
    1.33 -		    (upd_calc cI ((pt, p), tacis);
    1.34 -		     interStepsOK cI (*pos'forms*) ip' ip' lastpos)
    1.35 -		  | ("no-Rewrite_Set...", _, _) =>
    1.36 -		    sysERROR2xml cI "no Rewrite_Set..."
    1.37 -		  | (_, _(*, pos'formshds*), lastpos) =>
    1.38 -		    interStepsOK cI (*pos'formshds*) ip' ip' lastpos
    1.39 -	     end
    1.40 -     end)
    1.41 -    handle _ => sysERROR2xml cI "error in kernel";
    1.42 +  (let val ((pt,p), tacis) = get_calc cI
    1.43 +  in 
    1.44 +    if (not o is_interpos) ip
    1.45 +    then interStepsERROR cI ("only formulae with position (_,Res) " ^ 
    1.46 +      "may have intermediate steps above them")
    1.47 +    else 
    1.48 +      let val ip' = lev_pred' pt ip
    1.49 +      in case detailstep pt ip of
    1.50 +          ("detailrls", pt, lastpos) => (upd_calc cI ((pt, p), tacis);
    1.51 +            interStepsOK cI ip' ip' lastpos)
    1.52 +        | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
    1.53 +        | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
    1.54 +      end
    1.55 +  end)
    1.56 +  handle _ => sysERROR2xml cI "error in kernel";
    1.57  
    1.58  fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
    1.59      (let val ((pt,_),_) = get_calc cI

     2.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Tue Jul 01 16:08:32 2014 +0200
     2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Tue Jul 01 16:10:52 2014 +0200
     2.3 @@ -336,19 +336,18 @@
     2.4  	   (true, pI, hdl, pbl, pre) 
     2.5      end;
     2.6  
     2.7 -(* val (pt, (pos as (p,p_):pos')) = (pt, ip);
     2.8 -   *)
     2.9  fun detailstep pt (pos as (p,p_):pos') = 
    2.10 -    let val nd = get_nd pt p
    2.11 -	val cn = children nd
    2.12 -    in if null cn 
    2.13 -       then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
    2.14 -	    then detailrls pt pos
    2.15 -	    else ("no-Rewrite_Set...", EmptyPtree, e_pos')
    2.16 -       else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
    2.17 -	     (p @ [length (children (get_nd pt p))], Res) ) 
    2.18 -    end;
    2.19 -
    2.20 +  let 
    2.21 +    val nd = get_nd pt p
    2.22 +    val cn = children nd
    2.23 +  in 
    2.24 +    if null cn 
    2.25 +    then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
    2.26 +      then detailrls pt pos
    2.27 +      else ("no-Rewrite_Set...", EmptyPtree, e_pos')
    2.28 +    else ("donesteps", pt,
    2.29 +    (p @ [length (children (get_nd pt p))], Res) ) 
    2.30 +  end;
    2.31  
    2.32  
    2.33  (***. for mathematics authoring on sml-toplevel; no XML .***)

     3.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml	Tue Jul 01 16:08:32 2014 +0200
     3.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml	Tue Jul 01 16:10:52 2014 +0200
     3.3 @@ -306,7 +306,7 @@
     3.4  	     "<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
     3.5  	     "@@@@@end@@@@@");
     3.6  
     3.7 -fun interStepsOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =
     3.8 +fun interStepsOK (cI:calcID) (old:pos') (del:pos') (new:pos') =
     3.9      writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    3.10  	     "<INTERSTEPS>\n" ^
    3.11  	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^