1.1 --- a/src/Tools/isac/Interpret/script.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -58,9 +58,9 @@
1.4 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
1.5
1.6 fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
1.7 - | rule2thm' r = raise error ("rule2thm': not defined for "^(rule2str r));
1.8 + | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
1.9 fun rule2rls' (Rls_ rls) = id_rls rls
1.10 - | rule2rls' r = raise error ("rule2rls': not defined for "^(rule2str r));
1.11 + | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
1.12
1.13 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
1.14 complicated with current t in rrlsstate.*)
1.15 @@ -110,7 +110,7 @@
1.16 | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
1.17 | go (L::p) (t1 $ t2) = go p t1
1.18 | go (R::p) (t1 $ t2) = go p t2
1.19 - | go l _ = raise error ("go: no "^(loc_2str l));
1.20 + | go l _ = error ("go: no "^(loc_2str l));
1.21 (*
1.22 > val t = (term_of o the o (parse thy)) "a+b";
1.23 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
1.24 @@ -217,10 +217,10 @@
1.25 *)
1.26 fun init_form thy (Script sc) env =
1.27 (case get_stac thy sc of
1.28 - NONE => NONE (*raise error ("init_form: no 1st stac in "^
1.29 + NONE => NONE (*error ("init_form: no 1st stac in "^
1.30 (Syntax.string_of_term (thy2ctxt thy) sc))*)
1.31 | SOME stac => SOME (subst_atomic env stac))
1.32 - | init_form _ _ _ = raise error "init_form: no match";
1.33 + | init_form _ _ _ = error "init_form: no match";
1.34
1.35 (* use"ME/script.sml";
1.36 use"script.sml";
1.37 @@ -238,7 +238,7 @@
1.38 | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term
1.39 | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
1.40 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
1.41 - | itr_arg thy t = raise error
1.42 + | itr_arg thy t = error
1.43 ("itr_arg not impl. for "^
1.44 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
1.45 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
1.46 @@ -294,7 +294,7 @@
1.47 (*.from penv in itm_ make args for script depending on type of description.*)
1.48 (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
1.49 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
1.50 -fun mk_arg thy d [] = raise error ("mk_arg: no data for "^
1.51 +fun mk_arg thy d [] = error ("mk_arg: no data for "^
1.52 (Syntax.string_of_term (thy2ctxt thy) d))
1.53 | mk_arg thy d [t] =
1.54 (case dsc_valT d of
1.55 @@ -302,10 +302,10 @@
1.56 | "nam" =>
1.57 [case t of
1.58 r as (Const ("op =",_) $ _ $ _) => r
1.59 - | _ => raise error
1.60 + | _ => error
1.61 ("mk_arg: dsc-typ 'nam' applied to non-equality "^
1.62 (Syntax.string_of_term (thy2ctxt thy) t))]
1.63 - | s => raise error ("mk_arg: not impl. for "^s))
1.64 + | s => error ("mk_arg: not impl. for "^s))
1.65
1.66 | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
1.67 (*
1.68 @@ -332,7 +332,7 @@
1.69 fun itm2arg itms (_,(d,_)) =
1.70 case find_first (test_dsc d) itms of
1.71 NONE =>
1.72 - raise error ("itms2args: '"^term2str d^"' not in itms")
1.73 + error ("itms2args: '"^term2str d^"' not in itms")
1.74 (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
1.75 penv postponed; presently penv holds already env for script*)
1.76 | SOME (_,_,_,_,itm_) => penvval_in itm_
1.77 @@ -354,7 +354,7 @@
1.78 fun oris2fmz_vals oris =
1.79 let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
1.80 ((term2str o comp_dts') (dsc, ts), last_elem ts)
1.81 - handle _ => raise error ("ori2fmz_env called with "^terms2str ts)
1.82 + handle _ => error ("ori2fmz_env called with "^terms2str ts)
1.83 in (split_list o (map ori2fmz_vals)) oris end;
1.84
1.85 (*detour necessary, because generate1 delivers a string-result*)
1.86 @@ -469,7 +469,7 @@
1.87 Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f))
1.88 end
1.89
1.90 - | stac2tac_ pt thy t = raise error
1.91 + | stac2tac_ pt thy t = error
1.92 ("stac2tac_ TODO: no match for "^
1.93 (Syntax.string_of_term (thy2ctxt thy) t));
1.94 (*
1.95 @@ -536,7 +536,7 @@
1.96 else (mk_and o (map fst)) (get_assumptions_ pt (p,Res))
1.97 in (bdv, pred) end
1.98 | rep_set thy _ _ set =
1.99 - raise error ("check_elementwise: no set "^ (*from script*)
1.100 + error ("check_elementwise: no set "^ (*from script*)
1.101 (Syntax.string_of_term (thy2ctxt thy) set));
1.102 (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}";
1.103 > val p = [];
1.104 @@ -794,7 +794,7 @@
1.105 | tac_2tac Empty_Tac_ = Empty_Tac
1.106
1.107 | tac_2tac m =
1.108 - raise error ("tac_2tac: not impl. for "^(tac_2str m));
1.109 + error ("tac_2tac: not impl. for "^(tac_2str m));
1.110
1.111
1.112
1.113 @@ -952,7 +952,7 @@
1.114 | rep_tac_ (Take' (t')) = (Erule, (e_term, t'))
1.115 | rep_tac_ (Substitute' (subst,t,t')) = (Erule, (t, t'))
1.116 | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
1.117 - | rep_tac_ m = raise error ("rep_tac_: not impl.for "^
1.118 + | rep_tac_ m = error ("rep_tac_: not impl.for "^
1.119 (tac_2str m));
1.120
1.121 (*"N.3.6.03------
1.122 @@ -1118,7 +1118,7 @@
1.123 assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
1.124 | ay => ay)
1.125 | ay =>(ay))
1.126 - | NasApp _ => raise error ("assy: FIXXXME ///must not return NasApp///")
1.127 + | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
1.128 | ay => (ay))
1.129
1.130 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
1.131 @@ -1154,7 +1154,7 @@
1.132 | (a', STac stac) =>
1.133 let (*val _=tracing("### assy, stac = "^term2str stac);*)
1.134 val p' = case p_ of Frm => p | Res => lev_on p
1.135 - | _ => raise error ("assy: call by "^
1.136 + | _ => error ("assy: call by "^
1.137 (pos'2str (p,p_)));
1.138 in case assod pt d m stac of
1.139 Ass (m,v') =>
1.140 @@ -1307,7 +1307,7 @@
1.141 astep_up y ((E, (drop_last l), a,v,S,b),ss)
1.142
1.143 | ass_up y iss t =
1.144 - raise error ("ass_up not impl for t= "^(term2str t))
1.145 + error ("ass_up not impl for t= "^(term2str t))
1.146 (* 9.6.03
1.147 val (ys as (_,_,Script sc,_), ss) =
1.148 ((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list);
1.149 @@ -1448,7 +1448,7 @@
1.150 else Steps (ScrState is, ss))
1.151
1.152 | NasApp _ (*[((E,l,a,v,S,bb),(m',f',pt',p',c'))] =>
1.153 - raise error ("locate_gen: should not have got NasApp, ets =")*)
1.154 + error ("locate_gen: should not have got NasApp, ets =")*)
1.155 => NotLocatable
1.156 | NasNap (_,_) =>
1.157 if l=[] then NotLocatable
1.158 @@ -1468,7 +1468,7 @@
1.159 NotLocatable))
1.160 end
1.161 | locate_gen _ m _ (sc,_) is =
1.162 - raise error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
1.163 + error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
1.164 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is));
1.165
1.166
1.167 @@ -1800,7 +1800,7 @@
1.168 | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
1.169
1.170 | nxt_up (thy,_) ptp scr E l ay t a v =
1.171 - raise error ("nxt_up not impl for "^
1.172 + error ("nxt_up not impl for "^
1.173 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t))
1.174
1.175 (* val (thy, ptp, (Script sc), E, l, ay, a, v)=
1.176 @@ -1871,7 +1871,7 @@
1.177 | Appy (m', scrst as (_,_,_,v,_,_)) => (m', ScrState scrst,
1.178 (v, Sundef))) (*next stac*)
1.179
1.180 - | next_tac _ _ _ is = raise error ("next_tac: not impl for "^
1.181 + | next_tac _ _ _ is = error ("next_tac: not impl for "^
1.182 (istate2str is));
1.183
1.184
1.185 @@ -1888,7 +1888,7 @@
1.186 and (formal) args in met*)
1.187 fun relate_args env [] [] = env
1.188 | relate_args env _ [] =
1.189 - raise error ("ERROR in creating the environment for '"
1.190 + error ("ERROR in creating the environment for '"
1.191 ^id_of_scr sc^"' from \nthe items of the guard of "
1.192 ^metID2str metID^",\n\
1.193 \formal arg(s), from the script,\
1.194 @@ -1901,7 +1901,7 @@
1.195 | relate_args env (a::aa) (f::ff) =
1.196 if type_of a = type_of f
1.197 then relate_args (env @ [(a, f)]) aa ff else
1.198 - raise error ("ERROR in creating the environment for '"
1.199 + error ("ERROR in creating the environment for '"
1.200 ^id_of_scr sc^"' from \nthe items of the guard of "
1.201 ^metID2str metID^",\n\
1.202 \different types of formal arg, from the script,\
1.203 @@ -1923,7 +1923,7 @@
1.204 fun from_pblobj_or_detail' thy' (p,p_) pt =
1.205 if member op = [Pbl,Met] p_
1.206 then case get_obj g_env pt p of
1.207 - NONE => raise error "from_pblobj_or_detail': no istate"
1.208 + NONE => error "from_pblobj_or_detail': no istate"
1.209 | SOME is =>
1.210 let val metID = get_obj g_metID pt p
1.211 val {srls,...} = get_met metID