1.1 --- a/src/Tools/isac/Interpret/calchead.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -249,7 +249,7 @@
1.4
1.5 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
1.6 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
1.7 - | f_mout thy _ = raise error "f_mout: not called with formula";
1.8 + | f_mout thy _ = error "f_mout: not called with formula";
1.9
1.10
1.11 (*.is the calchead complete ?.*)
1.12 @@ -434,7 +434,7 @@
1.13 (* 30.1.00 ---
1.14 fun ct_in (Syn (c)) = c
1.15 | ct_in (Typ (c)) = c
1.16 - | ct_in _ = raise error "ct_in called for Cor .. Sup";
1.17 + | ct_in _ = error "ct_in called for Cor .. Sup";
1.18 --- *)
1.19
1.20 (*#############################################################*)
1.21 @@ -560,7 +560,7 @@
1.22 case find_first (test_subset (hd icl)) vors of
1.23 (* val SOME ori = find_first (test_subset (hd icl)) vors;
1.24 *)
1.25 - NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
1.26 + NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
1.27 | SOME ori => SOME (geti_ct thy ori (hd icl))
1.28 end
1.29 end;
1.30 @@ -571,12 +571,12 @@
1.31 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
1.32 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
1.33 | mk_delete thy str _ =
1.34 - raise error ("mk_delete: called with field '"^str^"'");
1.35 + error ("mk_delete: called with field '"^str^"'");
1.36 fun mk_additem "#Given" ct = Add_Given ct
1.37 | mk_additem "#Find" ct = Add_Find ct
1.38 | mk_additem "#Relate"ct = Add_Relation ct
1.39 | mk_additem str _ =
1.40 - raise error ("mk_additem: called with field '"^str^"'");
1.41 + error ("mk_additem: called with field '"^str^"'");
1.42
1.43
1.44
1.45 @@ -686,10 +686,10 @@
1.46 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
1.47 (id,vt,cl,sl,Cor (d,ts)):itm
1.48 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
1.49 - raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.50 + error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.51 " not not for Syn (s:cterm')")
1.52 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
1.53 - raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.54 + error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
1.55 " not not for Typ (s:cterm')")
1.56 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
1.57 (id,vt,cl,sl,Fal (d,ts))
1.58 @@ -721,8 +721,8 @@
1.59 (Cor _) =>
1.60 (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
1.61 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
1.62 - | (Syn c) => raise error ("ori_2itm wants to overwrite "^c)
1.63 - | (Typ c) => raise error ("ori_2itm wants to overwrite "^c)
1.64 + | (Syn c) => error ("ori_2itm wants to overwrite "^c)
1.65 + | (Typ c) => error ("ori_2itm wants to overwrite "^c)
1.66 | (Inc _) => if complete
1.67 then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
1.68 else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
1.69 @@ -790,7 +790,7 @@
1.70
1.71
1.72
1.73 -fun maxl [] = raise error "maxl of []"
1.74 +fun maxl [] = error "maxl of []"
1.75 | maxl (y::ys) =
1.76 let fun mx x [] = x
1.77 | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
1.78 @@ -973,7 +973,7 @@
1.79 fun matc thy ([]:pat list) _ (oris:preori list) = oris
1.80 | matc thy pbt [] _ =
1.81 (tracing (dashs 70);
1.82 - raise error ("actual arg(s) missing for '"^pats2str pbt
1.83 + error ("actual arg(s) missing for '"^pats2str pbt
1.84 ^"' i.e. should be 'copy-named' by '*_._'"))
1.85 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
1.86 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1.87 @@ -1019,7 +1019,7 @@
1.88 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
1.89 else ([1], field, dsc, [t])
1.90 )
1.91 - handle _ => raise error ("cpy_nam: for "^(term2str t));
1.92 + handle _ => error ("cpy_nam: for "^(term2str t));
1.93
1.94 (*.match the actual arguments of a SubProblem with a model-pattern
1.95 and create an ori list (in root-pbl created from formalization).
1.96 @@ -1063,7 +1063,7 @@
1.97 fun overwrite_ppc thy itm ppc =
1.98 let
1.99 fun repl ppc' (_,_,_,_,itm_) [] =
1.100 - raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
1.101 + error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
1.102 " not found")
1.103 | repl ppc' itm (p::ppc) =
1.104 if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
1.105 @@ -1106,7 +1106,7 @@
1.106 fun header p_ pI mI =
1.107 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1.108 | Met => Method mI
1.109 - | pos => raise error ("header called with "^ pos_2str pos);
1.110 + | pos => error ("header called with "^ pos_2str pos);
1.111
1.112
1.113
1.114 @@ -1395,7 +1395,7 @@
1.115 (* itms2itemppc thy [](*mpc*) pre
1.116 *)
1.117 | specify m' _ _ _ =
1.118 - raise error ("specify: not impl. for "^tac_2str m');
1.119 + error ("specify: not impl. for "^tac_2str m');
1.120
1.121 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1.122 val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1.123 @@ -1466,7 +1466,7 @@
1.124 *)
1.125 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1.126 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1.127 - handle _ => raise error ("ori2Coritm: dsc "^
1.128 + handle _ => error ("ori2Coritm: dsc "^
1.129 term2str d^
1.130 "in ori, but not in pbt")
1.131 ,ts))):itm;
1.132 @@ -1645,7 +1645,7 @@
1.133 (pt, pos)) end
1.134
1.135 | nxt_specif m' _ =
1.136 - raise error ("nxt_specif: not impl. for "^tac2str m');
1.137 + error ("nxt_specif: not impl. for "^tac2str m');
1.138
1.139 (*.get the values from oris; handle the term list w.r.t. penv.*)
1.140
1.141 @@ -1732,7 +1732,7 @@
1.142 (let val gf = (head_of given) $ formal;
1.143 val _ = cterm_of thy gf
1.144 in gf end)
1.145 - handle _ => raise error ("calchead.tag_form: " ^
1.146 + handle _ => error ("calchead.tag_form: " ^
1.147 Syntax.string_of_term (thy2ctxt thy) given ^
1.148 " .. " ^
1.149 Syntax.string_of_term (thy2ctxt thy) formal ^
1.150 @@ -1857,7 +1857,7 @@
1.151 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1.152 (*all stored in tac_ itms ^^^^^^^^^^*)
1.153 | nxt_model_pbl tac_ _ =
1.154 - raise error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1.155 + error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1.156 (* run subp_rooteq.sml ''
1.157 until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1.158 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1.159 @@ -1901,7 +1901,7 @@
1.160 in (pt, (p,Met):pos') end
1.161 ;
1.162 (*| complete_mod (pt, pos as (p, Met):pos') =
1.163 - raise error ("###complete_mod: only impl.for Pbl, called with "^
1.164 + error ("###complete_mod: only impl.for Pbl, called with "^
1.165 pos'2str pos);*)
1.166
1.167 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1.168 @@ -1926,19 +1926,19 @@
1.169 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1.170 if (is_pblobj o (get_obj I pt)) p
1.171 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1.172 - else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.173 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.174 | is_complete_mod (pt, pos as (p, Met)) =
1.175 if (is_pblobj o (get_obj I pt)) p
1.176 then (is_complete_mod_ o (get_obj g_met pt)) p
1.177 - else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.178 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.179 | is_complete_mod (_, pos) =
1.180 - raise error ("is_complete_mod called by "^pos'2str pos^
1.181 + error ("is_complete_mod called by "^pos'2str pos^
1.182 " (should be Pbl or Met)");
1.183
1.184 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1.185 fun is_complete_spec (pt, pos as (p,_): pos') =
1.186 if (not o is_pblobj o (get_obj I pt)) p
1.187 - then raise error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1.188 + then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1.189 else let val (dI,pI,mI) = get_obj g_spec pt p
1.190 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1.191 (*.complete empty items in specification from origin (pbl, met ev.refined);