51 "~~~~~ fun do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
51 "~~~~~ fun do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
52 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*) |
52 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*) |
53 tacis; (*= []*) |
53 tacis; (*= []*) |
54 member op = [Pbl,Met] p_; (*= false*) |
54 member op = [Pbl,Met] p_; (*= false*) |
55 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
55 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
56 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
56 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
57 val thy' = get_obj g_domID pt (par_pblobj pt p); |
57 val thy' = get_obj g_domID pt (par_pblobj pt p); |
58 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; |
58 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; |
59 |
59 |
60 val Next_Step (_, _, Check_elementwise' _) = |
60 val Next_Step (_, _, Check_elementwise' _) = |
61 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
61 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); |