50 show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *) |
50 show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *) |
51 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
51 "~~~~~ fun step, 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_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
54 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
55 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
55 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
56 val thy' = get_obj g_domID pt (par_pblobj pt p); |
56 val thy' = get_obj g_domID pt (par_pblobj pt p); |
57 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
57 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
58 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), |
58 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), |
59 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
59 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
60 val ctxt = get_ctxt pt pos |
60 val ctxt = get_ctxt pt pos |