1.1 --- a/src/Tools/isac/Frontend/interface.sml Sun May 15 11:32:41 2011 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Sun May 15 12:36:29 2011 +0200
1.3 @@ -400,74 +400,64 @@
1.4 handle _ => sysERROR2xml cI "error in kernel";
1.5
1.6
1.7 -(*.set the context determined on a knowledgebrowser to the current calc.*)
1.8 +(* set the UContext determined on a knowledgebrowser to the current calc *)
1.9 fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
1.10 - (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.11 - "thy_" =>
1.12 -(* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
1.13 - *)
1.14 - if member op = [Pbl,Met] p_
1.15 - then message2xml cI "thy-context not to calchead"
1.16 - else if ip = ([],Res) then message2xml cI "no thy-context at result"
1.17 - else if no_thycontext guh then message2xml cI ("no thy-context for '"^
1.18 - guh ^ "'")
1.19 - else let val (ptp as (pt,pold),_) = get_calc cI
1.20 - val is = get_istate pt ip
1.21 - val subs = subs_from is "dummy" guh
1.22 - val tac = guh2rewtac guh subs
1.23 - in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.24 - ("ok", (tacis, c, ptp as (_,p))) =>
1.25 -(* val (str, (tacis, c, ptp as (_,p))) = locatetac tac (pt, ip);
1.26 - *)
1.27 - (upd_calc cI ((pt,p), []);
1.28 - autocalculateOK2xml cI pold (if null c then pold
1.29 - else last_elem c) p)
1.30 - | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
1.31 - (upd_calc cI ((pt,p), []);
1.32 - autocalculateOK2xml cI pold (if null c then pold
1.33 - else last_elem c) p)
1.34 - | ("end-of-calculation",_) =>
1.35 - message2xml cI "end-of-calculation"
1.36 - | ("failure",_) => sysERROR2xml cI "failure"
1.37 - | ("not-applicable",_) => (*the rule comes from anywhere..*)
1.38 - (case applicable_in ip pt tac of
1.39 -
1.40 - Notappl e => message2xml cI ("'" ^ tac2str tac ^
1.41 - "' not-applicable")
1.42 - | Appl m =>
1.43 - let val (p,c,_,pt) = generate1 (assoc_thy"Isac")
1.44 - m (Uistate, e_ctxt) ip pt
1.45 - in upd_calc cI ((pt,p),[]);
1.46 - autocalculateOK2xml cI pold (if null c then pold
1.47 - else last_elem c) p
1.48 - end)
1.49 - end
1.50 -(* val (cI, ip as (_,p_), guh) = (1, pos, guh);
1.51 - *)
1.52 - | "pbl_" =>
1.53 - let val pI = guh2kestoreID guh
1.54 - val ((pt, _), _) = get_calc cI
1.55 - (*val ip as (_, p_) = get_pos cI 1*)
1.56 - in if member op = [Pbl, Met] p_
1.57 - then let val (pt, chd) = set_problem pI (pt, ip)
1.58 - in (upd_calc cI ((pt, ip), []);
1.59 - modifycalcheadOK2xml cI chd) end
1.60 - else sysERROR2xml cI "setContext for pbl requires ActiveFormula \
1.61 - \on CalcHead"
1.62 - end
1.63 -(* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin");
1.64 - *)
1.65 - | "met_" =>
1.66 - let val mI = guh2kestoreID guh
1.67 - val ((pt, _), _) = get_calc cI
1.68 - in if member op = [Pbl, Met] p_
1.69 - then let val (pt, chd) = set_method mI (pt, ip)
1.70 - in (upd_calc cI ((pt, ip), []);
1.71 - modifycalcheadOK2xml cI chd) end
1.72 - else sysERROR2xml cI "setContext for met requires ActiveFormula \
1.73 - \on CalcHead"
1.74 - end)
1.75 - handle _ => sysERROR2xml cI "error in kernel";
1.76 + (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.77 + "thy_" =>
1.78 + if member op = [Pbl,Met] p_
1.79 + then message2xml cI "thy-context not to calchead"
1.80 + else if ip = ([],Res) then message2xml cI "no thy-context at result"
1.81 + else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.82 + else
1.83 + let
1.84 + val (ptp as (pt, pold), _) = get_calc cI
1.85 + val is = get_istate pt ip
1.86 + val subs = subs_from is "dummy" guh
1.87 + val tac = guh2rewtac guh subs
1.88 + in
1.89 + case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.90 + ("ok", (tacis, c, ptp as (_,p))) =>
1.91 + (upd_calc cI ((pt,p), []);
1.92 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.93 + | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
1.94 + (upd_calc cI ((pt,p), []);
1.95 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.96 + | ("end-of-calculation",_) => message2xml cI "end-of-calculation"
1.97 + | ("failure",_) => sysERROR2xml cI "failure"
1.98 + | ("not-applicable",_) => (*the rule comes from anywhere..*)
1.99 + (case applicable_in ip pt tac of
1.100 + Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.101 + | Appl m =>
1.102 + let
1.103 + val (p,c,_,pt) =
1.104 + generate1 (assoc_thy "Isac") m (Uistate, e_ctxt(*WN150511*)) ip pt
1.105 + in upd_calc cI ((pt,p),[]);
1.106 + autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
1.107 + end)
1.108 + end
1.109 + | "pbl_" =>
1.110 + let
1.111 + val pI = guh2kestoreID guh
1.112 + val ((pt, _), _) = get_calc cI
1.113 + in
1.114 + if member op = [Pbl, Met] p_
1.115 + then
1.116 + let val (pt, chd) = set_problem pI (pt, ip)
1.117 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.118 + else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
1.119 + end
1.120 + | "met_" =>
1.121 + let
1.122 + val mI = guh2kestoreID guh
1.123 + val ((pt, _), _) = get_calc cI
1.124 + in
1.125 + if member op = [Pbl, Met] p_
1.126 + then
1.127 + let val (pt, chd) = set_method mI (pt, ip)
1.128 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.129 + else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
1.130 + end)
1.131 + handle _ => sysERROR2xml cI "error in kernel";
1.132
1.133
1.134 (*.specify the Method at the activeFormula and return a CalcHead
2.1 --- a/src/Tools/isac/Interpret/appl.sml Sun May 15 11:32:41 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Sun May 15 12:36:29 2011 +0200
2.3 @@ -594,59 +594,48 @@
2.4 ------------------*)
2.5
2.6 | applicable_in p pt (Apply_Assumption cts') =
2.7 - (error ("applicable_in: not impl. for "^
2.8 - (tac2str (Apply_Assumption cts'))))
2.9 + (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts'))))
2.10
2.11 (*'logical' applicability wrt. script in locate: Inconsistent?*)
2.12 | applicable_in (p,p_) pt (m as Take ct') =
2.13 - if member op = [Pbl,Met] p_
2.14 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
2.15 - else
2.16 - let val thy' = get_obj g_domID pt (par_pblobj pt p);
2.17 - in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
2.18 - SOME ct => Appl (Take' ct)
2.19 - | NONE => Notappl ("syntax error in "^ct'))
2.20 - end
2.21 + if member op = [Pbl,Met] p_
2.22 + then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
2.23 + else
2.24 + let val thy' = get_obj g_domID pt (par_pblobj pt p);
2.25 + in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
2.26 + SOME ct => Appl (Take' ct)
2.27 + | NONE => Notappl ("syntax error in " ^ ct'))
2.28 + end
2.29
2.30 | applicable_in p pt (Take_Inst ct') =
2.31 - error ("applicable_in: not impl. for "^
2.32 - (tac2str (Take_Inst ct')))
2.33 -
2.34 + error ("applicable_in: not impl. for " ^ tac2str (Take_Inst ct'))
2.35 | applicable_in p pt (Group (con, ints)) =
2.36 - error ("applicable_in: not impl. for "^
2.37 - (tac2str (Group (con, ints))))
2.38 + error ("applicable_in: not impl. for " ^ tac2str (Group (con, ints)))
2.39
2.40 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
2.41 if member op = [Pbl,Met] p_
2.42 - then (*maybe Apply_Method has already been done*)
2.43 - case get_obj g_env pt p of
2.44 - SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
2.45 - e_term, [], e_ctxt, subpbl domID pblID))
2.46 - | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
2.47 + then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
2.48 + case get_obj g_env pt p of
2.49 + SOME is =>
2.50 + Appl (Subproblem' ((domID, pblID, e_metID), [],
2.51 + e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
2.52 + | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
2.53 else (*somewhere later in the script*)
2.54 Appl (Subproblem' ((domID, pblID, e_metID), [],
2.55 - e_term, [], e_ctxt, subpbl domID pblID))
2.56 + e_term, [], e_ctxt, subpbl domID pblID))
2.57
2.58 | applicable_in p pt (End_Subproblem) =
2.59 - error ("applicable_in: not impl. for "^
2.60 - (tac2str (End_Subproblem)))
2.61 -
2.62 + error ("applicable_in: not impl. for " ^ tac2str End_Subproblem)
2.63 | applicable_in p pt (CAScmd ct') =
2.64 - error ("applicable_in: not impl. for "^
2.65 - (tac2str (CAScmd ct')))
2.66 -
2.67 + error ("applicable_in: not impl. for " ^ tac2str (CAScmd ct'))
2.68 | applicable_in p pt (Split_And) =
2.69 - error ("applicable_in: not impl. for "^
2.70 - (tac2str (Split_And)))
2.71 + error ("applicable_in: not impl. for " ^ tac2str Split_And)
2.72 | applicable_in p pt (Conclude_And) =
2.73 - error ("applicable_in: not impl. for "^
2.74 - (tac2str (Conclude_And)))
2.75 + error ("applicable_in: not impl. for " ^ tac2str Conclude_And)
2.76 | applicable_in p pt (Split_Or) =
2.77 - error ("applicable_in: not impl. for "^
2.78 - (tac2str (Split_Or)))
2.79 + error ("applicable_in: not impl. for " ^ tac2str Split_Or)
2.80 | applicable_in p pt (Conclude_Or) =
2.81 - error ("applicable_in: not impl. for "^
2.82 - (tac2str (Conclude_Or)))
2.83 + error ("applicable_in: not impl. for " ^ tac2str Conclude_Or)
2.84
2.85 | applicable_in (p,p_) pt (Begin_Trans) =
2.86 let
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Sun May 15 11:32:41 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sun May 15 12:36:29 2011 +0200
3.3 @@ -997,90 +997,82 @@
3.4 | pos => error ("header called with "^ pos_2str pos);
3.5
3.6
3.7 -fun specify_additem sel (ct,_) (p,Met) c pt =
3.8 - let
3.9 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
3.10 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
3.11 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
3.12 - (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
3.13 - val cpI = if pI = e_pblID then pI' else pI;
3.14 - val cmI = if mI = e_metID then mI' else mI;
3.15 - val {ppc,pre,prls,...} = get_met cmI;
3.16 - in case appl_add ctxt sel oris met ppc ct of
3.17 - Add itm (*..union old input *) =>
3.18 - let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
3.19 - *)
3.20 - val met' = insert_ppc thy itm met;
3.21 - (*val pt' = update_met pt p met';*)
3.22 - val ((p,Met),_,_,pt') =
3.23 - generate1 thy (case sel of
3.24 - "#Given" => Add_Given' (ct, met')
3.25 - | "#Find" => Add_Find' (ct, met')
3.26 - | "#Relate"=> Add_Relation'(ct, met'))
3.27 - (Uistate, e_ctxt) (p,Met) pt
3.28 - val pre' = check_preconds thy prls pre met'
3.29 - val pb = foldl and_ (true, map fst pre')
3.30 - (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
3.31 - val (p_,nxt) =
3.32 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
3.33 - ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
3.34 - in ((p,p_), ((p,p_),Uistate),
3.35 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
3.36 - (Method cmI, itms2itemppc thy met' pre'))),
3.37 - nxt,Safe,pt') end
3.38 - | Err msg =>
3.39 - let val pre' = check_preconds thy prls pre met
3.40 - val pb = foldl and_ (true, map fst pre')
3.41 - (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
3.42 - val (p_,nxt) =
3.43 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
3.44 - ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
3.45 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
3.46 - end
3.47 -(* val (p,_) = p;
3.48 - *)
3.49 -| specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
3.50 - let
3.51 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
3.52 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
3.53 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
3.54 - val cpI = if pI = e_pblID then pI' else pI;
3.55 - val cmI = if mI = e_metID then mI' else mI;
3.56 - val {ppc,where_,prls,...} = get_pbt cpI;
3.57 - in case appl_add ctxt sel oris pbl ppc ct of
3.58 - Add itm (*..union old input *) =>
3.59 - (* val Add itm = appl_add thy sel oris pbl ppc ct;
3.60 - *)
3.61 - let
3.62 - (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
3.63 - val pbl' = insert_ppc thy itm pbl
3.64 - val ((p,Pbl),_,_,pt') =
3.65 - generate1 thy (case sel of
3.66 - "#Given" => Add_Given' (ct, pbl')
3.67 - | "#Find" => Add_Find' (ct, pbl')
3.68 - | "#Relate"=> Add_Relation'(ct, pbl'))
3.69 - (Uistate, e_ctxt) (p,Pbl) pt
3.70 - val pre = check_preconds thy prls where_ pbl'
3.71 - val pb = foldl and_ (true, map fst pre)
3.72 - (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
3.73 - val (p_,nxt) =
3.74 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
3.75 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
3.76 - val ppc = if p_= Pbl then pbl' else met;
3.77 - in ((p,p_), ((p,p_),Uistate),
3.78 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
3.79 - (header p_ pI cmI,
3.80 - itms2itemppc thy ppc pre))), nxt,Safe,pt') end
3.81 +fun specify_additem sel (ct,_) (p, Met) c pt =
3.82 + let
3.83 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
3.84 + probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
3.85 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
3.86 + val cpI = if pI = e_pblID then pI' else pI;
3.87 + val cmI = if mI = e_metID then mI' else mI;
3.88 + val {ppc,pre,prls,...} = get_met cmI;
3.89 + in
3.90 + case appl_add ctxt sel oris met ppc ct of
3.91 + Add itm (*..union old input *) =>
3.92 + let
3.93 + val met' = insert_ppc thy itm met;
3.94 + val ((p, Met), _, _, pt') =
3.95 + generate1 thy (case sel of
3.96 + "#Given" => Add_Given' (ct, met')
3.97 + | "#Find" => Add_Find' (ct, met')
3.98 + | "#Relate"=> Add_Relation'(ct, met'))
3.99 + (Uistate, e_ctxt) (p, Met) pt
3.100 + val pre' = check_preconds thy prls pre met'
3.101 + val pb = foldl and_ (true, map fst pre')
3.102 + val (p_, nxt) =
3.103 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
3.104 + ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
3.105 + in ((p, p_), ((p, p_), Uistate),
3.106 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
3.107 + (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
3.108 + end
3.109 + | Err msg =>
3.110 + let
3.111 + val pre' = check_preconds thy prls pre met
3.112 + val pb = foldl and_ (true, map fst pre')
3.113 + val (p_, nxt) =
3.114 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
3.115 + ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
3.116 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
3.117 + end
3.118
3.119 - | Err msg =>
3.120 - let val pre = check_preconds thy prls where_ pbl
3.121 - val pb = foldl and_ (true, map fst pre)
3.122 - (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
3.123 - val (p_,nxt) =
3.124 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
3.125 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
3.126 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
3.127 - end;
3.128 + | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
3.129 + let
3.130 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
3.131 + probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
3.132 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
3.133 + val cpI = if pI = e_pblID then pI' else pI;
3.134 + val cmI = if mI = e_metID then mI' else mI;
3.135 + val {ppc,where_,prls,...} = get_pbt cpI;
3.136 + in
3.137 + case appl_add ctxt sel oris pbl ppc ct of
3.138 + Add itm (*..union old input *) =>
3.139 + let
3.140 + val pbl' = insert_ppc thy itm pbl
3.141 + val ((p, Pbl), _, _, pt') =
3.142 + generate1 thy (case sel of
3.143 + "#Given" => Add_Given' (ct, pbl')
3.144 + | "#Find" => Add_Find' (ct, pbl')
3.145 + | "#Relate"=> Add_Relation'(ct, pbl'))
3.146 + (Uistate, e_ctxt) (p,Pbl) pt
3.147 + val pre = check_preconds thy prls where_ pbl'
3.148 + val pb = foldl and_ (true, map fst pre)
3.149 + val (p_, nxt) =
3.150 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
3.151 + (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
3.152 + val ppc = if p_= Pbl then pbl' else met;
3.153 + in ((p,p_), ((p,p_),Uistate),
3.154 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
3.155 + (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
3.156 + end
3.157 + | Err msg =>
3.158 + let
3.159 + val pre = check_preconds thy prls where_ pbl
3.160 + val pb = foldl and_ (true, map fst pre)
3.161 + val (p_, nxt) =
3.162 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
3.163 + (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
3.164 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
3.165 + end;
3.166
3.167 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
3.168 let (* either """"""""""""""" all empty or complete *)
4.1 --- a/src/Tools/isac/Interpret/generate.sml Sun May 15 11:32:41 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Sun May 15 12:36:29 2011 +0200
4.3 @@ -260,18 +260,22 @@
4.4 (*generate 1 ppobj in ptree*)
4.5 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
4.6 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
4.7 - (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
4.8 - (Upblmet,itms2itemppc thy [][]))),
4.9 - case p_ of Pbl => update_pbl pt p itmlist
4.10 - | Met => update_met pt p itmlist)
4.11 + (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet, itms2itemppc thy [][]))),
4.12 + case p_ of
4.13 + Pbl => update_pbl pt p itmlist
4.14 + | Met => update_met pt p itmlist)
4.15 +
4.16 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
4.17 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.18 - case p_ of Pbl => update_pbl pt p itmlist
4.19 - | Met => update_met pt p itmlist)
4.20 + (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.21 + case p_ of
4.22 + Pbl => update_pbl pt p itmlist
4.23 + | Met => update_met pt p itmlist)
4.24 +
4.25 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
4.26 - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.27 - case p_ of Pbl => update_pbl pt p itmlist
4.28 - | Met => update_met pt p itmlist)
4.29 + (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
4.30 + case p_ of
4.31 + Pbl => update_pbl pt p itmlist
4.32 + | Met => update_met pt p itmlist)
4.33
4.34 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
4.35 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.1 --- a/test/Tools/isac/Test_Isac.thy Sun May 15 11:32:41 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Sun May 15 12:36:29 2011 +0200
5.3 @@ -109,6 +109,8 @@
5.4 ML {*
5.5 *}
5.6 ML {*
5.7 +val (p,p_) = ([], Frm):pos';
5.8 +Notappl (" not for pos " ^ pos'2str (p,p_))
5.9 *}
5.10 ML {*
5.11 *}