69 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
69 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
70 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
70 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
71 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
71 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
72 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
72 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
73 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
73 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
74 (** ) |
|
75 val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; |
74 val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; |
76 ( **) |
75 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ continue AFTER previous step 'me' ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"; |
77 (*//---------------- adhoc inserted ------------------------------------------------\\* ) |
|
78 see TOODOO.1 in test/../evaluate.sml |
|
79 ( *\\---------------- adhoc inserted ------------------------------------------------//*) |
|
80 |
|
81 (*//---------------- continue AFTER previous step "me" -----------------------------\\* ) |
|
82 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ continue AFTER previous step "me" ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"; |
|
83 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = |
76 "~~~~~ fun me, args:"; val (tac, (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = |
84 (nxt''''', p''''', [], pt'''''); |
77 (nxt''''', p''''', [], pt'''''); |
85 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p) |
78 val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p) |
86 val (pt, p) = ptp; |
79 val (pt, p) = ptp; |
87 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) = |
80 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) = |
96 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt; |
89 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt; |
97 |
90 |
98 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*) |
91 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*) |
99 case tac of Or_to_List' _ => () |
92 case tac of Or_to_List' _ => () |
100 | _ => error "Or_to_List broken ?" |
93 | _ => error "Or_to_List broken ?" |
101 ( *\\---------------- continue AFTER previous step "me" -----------------------------//*) |
|
102 |
94 |
103 |
95 |
104 "----------- check thy in CalcTreeTEST ------------------"; |
96 "----------- check thy in CalcTreeTEST ------------------"; |
105 "----------- check thy in CalcTreeTEST ------------------"; |
97 "----------- check thy in CalcTreeTEST ------------------"; |
106 "----------- check thy in CalcTreeTEST ------------------"; |
98 "----------- check thy in CalcTreeTEST ------------------"; |