1.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Dec 12 18:08:13 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Dec 14 09:37:01 2016 +0100
1.3 @@ -10,7 +10,7 @@
1.4 datatype appl = Appl of tac_ | Notappl of string
1.5 val nxt_specify_init_calc : fmz -> calcstate
1.6 val specify : tac_ -> pos' -> cid -> ptree ->
1.7 - (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac * safe * ptree
1.8 + (posel list * pos_) * ((posel list * pos_) * istate) * Ctree.mout * tac * safe * ptree
1.9 val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
1.10 val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
1.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
1.12 @@ -69,9 +69,9 @@
1.13 *)
1.14 type calcstate =
1.15 (ptree * pos') * (* the calc-state to which the tacis could be applied *)
1.16 - (taci list) (* ev. several (hidden) steps;
1.17 + (Ctree.taci list) (* ev. several (hidden) steps;
1.18 in REVERSE order: first tac_ to apply is last_elem *)
1.19 -val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]) : calcstate;
1.20 +val e_calcstate = ((EmptyPtree, e_pos'), [Ctree.e_taci]) : calcstate;
1.21
1.22 (*the state used during one calculation within the mathengine; it contains
1.23 a list of [tac,istate](="tacis") which generated the the calc-state;
1.24 @@ -83,14 +83,14 @@
1.25 because the tacis hold enought information for efficiently rebuilding
1.26 this state just by "fun generate ".*)
1.27 type calcstate' =
1.28 - taci list * (* cas. several (hidden) steps;
1.29 - in REVERSE order: first tac_ to apply is last_elem*)
1.30 - pos' list * (* a "continuous" sequence of pos', deleted by application of taci list*)
1.31 - (ptree * pos') (* the calc-state resulting from the application of tacis*)
1.32 -val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.33 + Ctree.taci list * (* cas. several (hidden) steps;
1.34 + in REVERSE order: first tac_ to apply is last_elem *)
1.35 + pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
1.36 + (ptree * pos') (* the calc-state resulting from the application of tacis *)
1.37 +val e_calcstate' = ([Ctree.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.38
1.39 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
1.40 -fun f_mout thy (Form' (FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
1.41 +fun f_mout thy (Ctree.Form' (Ctree.FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
1.42 | f_mout _ _ = error "f_mout: not called with formula";
1.43
1.44 (* is the calchead complete ? *)
1.45 @@ -606,8 +606,8 @@
1.46
1.47 (* output the headline to a ppc *)
1.48 fun header p_ pI mI =
1.49 - case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1.50 - | Met => Method mI
1.51 + case p_ of Pbl => Ctree.Problem (if pI = e_pblID then [] else pI)
1.52 + | Met => Ctree.Method mI
1.53 | pos => error ("header called with "^ pos_2str pos)
1.54
1.55 fun specify_additem sel (ct, _) (p, Met) _ pt =
1.56 @@ -630,7 +630,7 @@
1.57 | "#Find" => Add_Find' (ct, met')
1.58 | "#Relate"=> Add_Relation'(ct, met')
1.59 | str => error ("specify_additem: uncovered case with " ^ str)
1.60 - val (p, Met, pt') = case generate1 thy arg (Uistate, ctxt) (p, Met) pt of
1.61 + val (p, Met, pt') = case Ctree.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
1.62 ((p, Met), _, _, pt') => (p, Met, pt')
1.63 | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
1.64 val pre' = check_preconds thy prls pre met'
1.65 @@ -639,8 +639,8 @@
1.66 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.67 ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.68 in ((p, p_), ((p, p_), Uistate),
1.69 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.70 - (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1.71 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,
1.72 + (Ctree.Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1.73 end
1.74 | Err msg =>
1.75 let
1.76 @@ -649,7 +649,7 @@
1.77 val (p_, nxt) =
1.78 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.79 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.80 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.81 + in ((p,p_), ((p,p_),Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end
1.82 end
1.83 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
1.84 let
1.85 @@ -671,7 +671,7 @@
1.86 | "#Find" => Add_Find' (ct, pbl')
1.87 | "#Relate"=> Add_Relation'(ct, pbl')
1.88 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
1.89 - val ((p, Pbl), _, _, pt') = generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.90 + val ((p, Pbl), _, _, pt') = Ctree.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.91 val pre = check_preconds thy prls where_ pbl'
1.92 val pb = foldl and_ (true, map fst pre)
1.93 val (p_, nxt) =
1.94 @@ -679,7 +679,7 @@
1.95 val ppc = if p_= Pbl then pbl' else met
1.96 in
1.97 ((p, p_), ((p, p_), Uistate),
1.98 - Form' (PpcKF (0, EdUndef, (length p), Nundef,
1.99 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,
1.100 (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')
1.101 end
1.102 | Err msg =>
1.103 @@ -689,7 +689,7 @@
1.104 val (p_, nxt) =
1.105 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.106 (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.107 - in ((p, p_), ((p, p_), Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.108 + in ((p, p_), ((p, p_), Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end
1.109 end
1.110
1.111 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
1.112 @@ -707,11 +707,11 @@
1.113 case mI' of
1.114 ["no_met"] =>
1.115 (([], Pbl), (([], Pbl), Uistate),
1.116 - Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.117 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.118 Refine_Tacitly pI', Safe, pt)
1.119 | _ =>
1.120 (([], Pbl), (([], Pbl), Uistate),
1.121 - Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.122 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.123 Model_Problem, Safe, pt)
1.124 end
1.125 (* ONLY for STARTING modeling phase *)
1.126 @@ -727,12 +727,12 @@
1.127 val pre = check_preconds thy prls where_ pbl
1.128 val pb = foldl and_ (true, map fst pre)
1.129 val ((p, _), _, _, pt) =
1.130 - generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.131 + Ctree.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.132 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.133 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.134 in
1.135 ((p, Pbl), ((p, p_), Uistate),
1.136 - Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1.137 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1.138 nxt, Safe, pt)
1.139 end
1.140 (* called only if no_met is specified *)
1.141 @@ -744,19 +744,19 @@
1.142 val {met, thy,...} = get_pbt pIre
1.143 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.144 val ((p,_), _, _, pt) =
1.145 - generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.146 + Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.147 val (pbl, pre, _) = ([], [], false)
1.148 in ((p, Pbl), (pos, Uistate),
1.149 - Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1.150 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1.151 Model_Problem, Safe, pt)
1.152 end
1.153 | specify (Refine_Problem' rfd) pos _ pt =
1.154 let
1.155 val ctxt = get_ctxt pt pos
1.156 val (pos, _, _, pt) =
1.157 - generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.158 + Ctree.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.159 in
1.160 - (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Problems (RefinedKF rfd), Model_Problem, Safe, pt)
1.161 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.Problems (Ctree.RefinedKF rfd), Model_Problem, Safe, pt)
1.162 end
1.163 (*WN110515 initialise ctxt again from itms and add preconds*)
1.164 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
1.165 @@ -767,7 +767,7 @@
1.166 | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.167 val thy = assoc_thy dI
1.168 val (p, Pbl, pt) =
1.169 - case generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
1.170 + case Ctree.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
1.171 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
1.172 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.173 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
1.174 @@ -776,7 +776,7 @@
1.175 (#ppc o get_met) mI'') (dI, pI, mI);
1.176 in
1.177 ((p,Pbl), (pos,Uistate),
1.178 - Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
1.179 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI, itms2itemppc dI'' itms pre))),
1.180 nxt, Safe, pt)
1.181 end
1.182 (*WN110515 initialise ctxt again from itms and add preconds*)
1.183 @@ -794,12 +794,12 @@
1.184 val met = if met = [] then pbl else met
1.185 val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris
1.186 val (pos, _, _, pt) =
1.187 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.188 + Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.189 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
1.190 ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
1.191 in
1.192 (pos, (pos,Uistate),
1.193 - Form' (PpcKF (0, EdUndef, length p, Nundef, (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.194 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.195 nxt, Safe, pt)
1.196 end
1.197 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.198 @@ -828,16 +828,16 @@
1.199 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.200 in
1.201 ((p, p_), (pos, Uistate),
1.202 - Form'(PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.203 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.204 nxt, Safe, pt)
1.205 end
1.206 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.207 let
1.208 - val ((p, p_), _, _, pt) = generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.209 + val ((p, p_), _, _, pt) = Ctree.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.210 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.211 in
1.212 ((p,p_), (pos,Uistate),
1.213 - Form' (PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.214 + Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.215 nxt, Safe, pt)
1.216 end
1.217 end
1.218 @@ -863,7 +863,7 @@
1.219 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.220 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.221 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
1.222 - val (p, Pbl, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
1.223 + val (p, Pbl, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
1.224 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
1.225 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.226 in
1.227 @@ -892,7 +892,7 @@
1.228 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.229 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.230 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
1.231 - val (p, Met, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
1.232 + val (p, Met, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
1.233 ((p, Met), c, _, pt') => (p, Met, c, pt')
1.234 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.235 in
1.236 @@ -967,7 +967,7 @@
1.237 val thy = assoc_thy dI
1.238 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.239 val {cas, ppc, ...} = get_pbt pI
1.240 - val pbl = init_pbl ppc (* fill in descriptions *)
1.241 + val pbl = Ctree.init_pbl ppc (* fill in descriptions *)
1.242 (*----------------if you think, this should be done by the Dialog
1.243 in the java front-end, search there for WN060225-modelProblem----*)
1.244 val (pbl, met) = case cas of
1.245 @@ -975,7 +975,7 @@
1.246 | _ => complete_mod_ (oris, mpc, ppc, probl)
1.247 (*----------------------------------------------------------------*)
1.248 val tac_ = Model_Problem' (pI, pbl, met)
1.249 - val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
1.250 + val (pos,c,_,pt) = Ctree.generate1 thy tac_ (Uistate, ctxt) pos pt
1.251 in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
1.252 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.253 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1.254 @@ -996,7 +996,7 @@
1.255 val mI = if length met = 0 then e_metID else hd met
1.256 val thy = assoc_thy dI
1.257 val (pos, c, _, pt) =
1.258 - generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1.259 + Ctree.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1.260 in
1.261 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.262 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.263 @@ -1015,7 +1015,7 @@
1.264 NONE => ([], [], ptp)
1.265 | SOME rfd =>
1.266 let
1.267 - val (pos,c,_,pt) = generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.268 + val (pos,c,_,pt) = Ctree.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.269 in
1.270 ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.271 end
1.272 @@ -1030,10 +1030,10 @@
1.273 val {ppc,where_,prls,...} = get_pbt pI
1.274 val pbl =
1.275 if pI' = e_pblID andalso pI = e_pblID
1.276 - then (false, (init_pbl ppc, []))
1.277 + then (false, (Ctree.init_pbl ppc, []))
1.278 else match_itms_oris thy probl (ppc,where_,prls) oris
1.279 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.280 - val (c, pt) = case generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.281 + val (c, pt) = case Ctree.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.282 ((_, Pbl), c, _, pt) => (c, pt)
1.283 | _ => error ""
1.284 in
1.285 @@ -1053,7 +1053,7 @@
1.286 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1.287 val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris
1.288 val (pos, c, _, pt) =
1.289 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.290 + Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.291 in
1.292 ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
1.293 end
1.294 @@ -1061,7 +1061,7 @@
1.295 let
1.296 val ctxt = get_ctxt pt pos
1.297 val (pos, c, _, pt) =
1.298 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.299 + Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.300 in (*FIXXXME: check if pbl can still be parsed*)
1.301 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
1.302 (pt, pos))
1.303 @@ -1069,7 +1069,7 @@
1.304 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
1.305 let
1.306 val ctxt = get_ctxt pt pos
1.307 - val (pos, c, _, pt) = generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.308 + val (pos, c, _, pt) = Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.309 in (*FIXXXME: check if met can still be parsed*)
1.310 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
1.311 end
1.312 @@ -1092,7 +1092,7 @@
1.313 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
1.314 ([], (dI,pI,mI), hdl)
1.315 val pt = update_spec pt [] (dI, pI, mI)
1.316 - val pits = init_pbl' ppc
1.317 + val pits = Ctree.init_pbl' ppc
1.318 val pt = update_pbl pt [] pits
1.319 in ((pt, ([] , Pbl)), []) : calcstate end
1.320 else
1.321 @@ -1104,7 +1104,7 @@
1.322 val (pt, _) =
1.323 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1.324 val pt = update_spec pt [] (dI, pI, mI)
1.325 - val mits = init_pbl' ppc
1.326 + val mits = Ctree.init_pbl' ppc
1.327 val pt = update_met pt [] mits
1.328 in ((pt, ([], Met)), []) end
1.329 else (* new example, pepare for interactive modeling *)