334 in (false, pI, hdl, pbl, pre) end |
334 in (false, pI, hdl, pbl, pre) end |
335 | SOME (pI, (pbl, pre)) => |
335 | SOME (pI, (pbl, pre)) => |
336 (true, pI, hdl, pbl, pre) |
336 (true, pI, hdl, pbl, pre) |
337 end; |
337 end; |
338 |
338 |
339 (* val (pt, (pos as (p,p_):pos')) = (pt, ip); |
|
340 *) |
|
341 fun detailstep pt (pos as (p,p_):pos') = |
339 fun detailstep pt (pos as (p,p_):pos') = |
342 let val nd = get_nd pt p |
340 let |
343 val cn = children nd |
341 val nd = get_nd pt p |
344 in if null cn |
342 val cn = children nd |
345 then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] |
343 in |
346 then detailrls pt pos |
344 if null cn |
347 else ("no-Rewrite_Set...", EmptyPtree, e_pos') |
345 then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] |
348 else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*), |
346 then detailrls pt pos |
349 (p @ [length (children (get_nd pt p))], Res) ) |
347 else ("no-Rewrite_Set...", EmptyPtree, e_pos') |
350 end; |
348 else ("donesteps", pt, |
351 |
349 (p @ [length (children (get_nd pt p))], Res) ) |
|
350 end; |
352 |
351 |
353 |
352 |
354 (***. for mathematics authoring on sml-toplevel; no XML .***) |
353 (***. for mathematics authoring on sml-toplevel; no XML .***) |
355 |
354 |
356 type NEW = int list; |
355 type NEW = int list; |