1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -59,7 +59,7 @@
1.4 | "#Find" => #Find (ppc:'a ppc)
1.5 | "#With" => #With (ppc:'a ppc)
1.6 | "#Relate" => #Relate (ppc:'a ppc)
1.7 - | _ => raise error ("sel_ppc tried to select by '"^sel^"'");
1.8 + | _ => error ("sel_ppc tried to select by '"^sel^"'");
1.9
1.10 fun repl_sel_ppc sel
1.11 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
1.12 @@ -69,7 +69,7 @@
1.13 | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
1.14 | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
1.15 | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
1.16 - | _ => raise error ("repl_sel_ppc tried to select by '"^sel^"'");
1.17 + | _ => error ("repl_sel_ppc tried to select by '"^sel^"'");
1.18
1.19 fun add_sel_ppc thy sel
1.20 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
1.21 @@ -79,7 +79,7 @@
1.22 | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
1.23 | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
1.24 | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
1.25 - | _ => raise error ("add_sel_ppc tried to select by '"^sel^"'");
1.26 + | _ => error ("add_sel_ppc tried to select by '"^sel^"'");
1.27 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
1.28 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
1.29
1.30 @@ -98,7 +98,7 @@
1.31 then (hd, args)
1.32 else (e_term, [t]) (*??? 9.01 just copied*)
1.33 end)
1.34 - handle _ => raise error ("split_dsc: called with "^
1.35 + handle _ => error ("split_dsc: called with "^
1.36 (Syntax.string_of_term (thy2ctxt' "Isac") t));
1.37 (*
1.38 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
1.39 @@ -120,7 +120,7 @@
1.40 fun split_dsc' t =
1.41 (let val dsc $ var = t
1.42 in var end)
1.43 - handle _ => raise error ("split_dsc': called with "^term2str t);
1.44 + handle _ => error ("split_dsc': called with "^term2str t);
1.45
1.46 (*9.3.00*)
1.47 (* split a term into description and (id | structured variable)
1.48 @@ -128,7 +128,7 @@
1.49 fun split_did t =
1.50 (let val (hd,[arg]) = strip_comb t
1.51 in (hd,arg) end)
1.52 - handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
1.53 + handle _ => error ("split_did: doesn't match (hd,[arg]) for t = "
1.54 ^(Syntax.string_of_term (thy2ctxt' "Script") t));
1.55
1.56
1.57 @@ -198,7 +198,7 @@
1.58 else if d mem (get_dsc_in dscs "#Relate")
1.59 then ("#Relate",d,ts)
1.60 else ("#undef",d,ts);
1.61 -(* 28.1.00 raise error ("add_field: '"^
1.62 +(* 28.1.00 error ("add_field: '"^
1.63 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.64 "' not in ppc-description "); *)
1.65 ------9.3. *)
1.66 @@ -210,7 +210,7 @@
1.67 in case filter (eq d) pbt of
1.68 [(fi,(dsc,_))] => (fi,d,ts)
1.69 | [] => ("#undef",d,ts) (*may come with met.ppc*)
1.70 - | _ => raise error ("add_field: "^
1.71 + | _ => error ("add_field: "^
1.72 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.73 " more than once in pbt")
1.74 end;
1.75 @@ -225,10 +225,10 @@
1.76 case filter (eq d) mpc of
1.77 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
1.78 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
1.79 - (*raise error ("add_field': "^
1.80 + (*error ("add_field': "^
1.81 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.82 " not in met"*)
1.83 - | _ => raise error ("add_field': "^
1.84 + | _ => error ("add_field': "^
1.85 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.86 " more than once in met");
1.87 in (flat ((map (repl mpc)) ori)):ori list end;
1.88 @@ -236,7 +236,7 @@
1.89
1.90 (*.mark an element with the position within a plateau;
1.91 a plateau with length 1 is marked with 0 .*)
1.92 -fun mark eq [] = raise error "mark []"
1.93 +fun mark eq [] = error "mark []"
1.94 | mark eq xs =
1.95 let
1.96 fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
1.97 @@ -272,12 +272,12 @@
1.98 val it = [1,2,4] : int list
1.99 *)
1.100
1.101 -fun max [] = raise error "max of []"
1.102 +fun max [] = error "max of []"
1.103 | max (y::ys) =
1.104 let fun mx x [] = x
1.105 | mx x (y::ys) = if x < y then mx y ys else mx x ys;
1.106 in mx y ys end;
1.107 -fun gen_max _ [] = raise error "gen_max of []"
1.108 +fun gen_max _ [] = error "gen_max of []"
1.109 | gen_max ord (y::ys) =
1.110 let fun mx x [] = x
1.111 | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
1.112 @@ -301,7 +301,7 @@
1.113 fun replace_0 vm [0] = intsto vm
1.114 | replace_0 vm vs = vs;
1.115
1.116 -fun add_id [] = raise error "add_id []"
1.117 +fun add_id [] = error "add_id []"
1.118 | add_id xs =
1.119 let fun add n [] = []
1.120 | add n (x::xs) = (n,x) :: add (n+1) xs;
1.121 @@ -338,7 +338,7 @@
1.122 val ctopts = map (parse thy) fmz
1.123 val _= (*FIXME.WN060916 improve error report*)
1.124 if null (filter is_none ctopts) then ()
1.125 - else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
1.126 + else error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
1.127 val dts = map ((split_dts thy) o term_of o the) ctopts
1.128 val ori = map (add_field thy pbt) dts;
1.129 (* val ori = map (flat3 o (pair "#undef")) dts; *)
1.130 @@ -662,17 +662,17 @@
1.131
1.132 val fi = filter (eq "#Find") dsc_dats;
1.133 val fi = (case fi of
1.134 - [] => [](*28.8.01: ["tool"] ...// raise error
1.135 + [] => [](*28.8.01: ["tool"] ...// error
1.136 ("prep_pbt: no '#Find' in "^(strs2str pblID))*)
1.137 (* val ((_,fi')::[]) = fi;
1.138 *)
1.139 | ((_,fi')::[]) =>
1.140 ((map (split_did o term_of o the o (parse thy)) fi')
1.141 - handle _ => raise error
1.142 + handle _ => error
1.143 ("prep_pbt: syntax error in '#Find' of "^
1.144 (strs2str pblID)))
1.145 | _ =>
1.146 - (raise error ("prep_pbt: more than one '#Find' in "^
1.147 + (error ("prep_pbt: more than one '#Find' in "^
1.148 (strs2str pblID))));
1.149 val fi = map (pair "#Find") fi;
1.150
1.151 @@ -681,11 +681,11 @@
1.152 [] => []
1.153 | ((_,re')::[]) =>
1.154 ((map (split_did o term_of o the o (parse thy)) re')
1.155 - handle _ => raise error
1.156 + handle _ => error
1.157 ("prep_pbt: syntax error in '#Relate' of "^
1.158 (strs2str pblID)))
1.159 | _ =>
1.160 - (raise error ("prep_pbt: more than one '#Relate' in "^
1.161 + (error ("prep_pbt: more than one '#Relate' in "^
1.162 (strs2str pblID))));
1.163 val re = map (pair "#Relate") re;
1.164
1.165 @@ -694,11 +694,11 @@
1.166 [] => []
1.167 | ((_,wh')::[]) =>
1.168 ((map (parse_patt thy) wh')
1.169 - handle _ => raise error
1.170 + handle _ => error
1.171 ("prep_pbt: syntax error in '#Where' of "^
1.172 (strs2str pblID)))
1.173 | _ =>
1.174 - (raise error ("prep_pbt: more than one '#Where' in "^
1.175 + (error ("prep_pbt: more than one '#Where' in "^
1.176 (strs2str pblID))));
1.177 in ({guh=guh,mathauthors=maa,init=init,
1.178 thy=thy,cas= case ca of NONE => NONE
1.179 @@ -732,25 +732,25 @@
1.180 [] => []
1.181 | ((_,gi')::[]) =>
1.182 ((map (split_did o term_of o the o (parse thy)) gi')
1.183 - handle _ => raise error
1.184 + handle _ => error
1.185 ("prep_pbt: syntax error in '#Given' of "^
1.186 (strs2str metID)))
1.187 | _ =>
1.188 - (raise error ("prep_pbt: more than one '#Given' in "^
1.189 + (error ("prep_pbt: more than one '#Given' in "^
1.190 (strs2str metID))));
1.191 val gi = map (pair "#Given") gi;
1.192
1.193 val fi = filter (eq "#Find") ppc;
1.194 val fi = (case fi of
1.195 - [] => [](*28.8.01: ["tool"] ...// raise error
1.196 + [] => [](*28.8.01: ["tool"] ...// error
1.197 ("prep_pbt: no '#Find' in "^(strs2str metID))*)
1.198 | ((_,fi')::[]) =>
1.199 ((map (split_did o term_of o the o (parse thy)) fi')
1.200 - handle _ => raise error
1.201 + handle _ => error
1.202 ("prep_pbt: syntax error in '#Find' of "^
1.203 (strs2str metID)))
1.204 | _ =>
1.205 - (raise error ("prep_pbt: more than one '#Find' in "^
1.206 + (error ("prep_pbt: more than one '#Find' in "^
1.207 (strs2str metID))));
1.208 val fi = map (pair "#Find") fi;
1.209
1.210 @@ -759,11 +759,11 @@
1.211 [] => []
1.212 | ((_,re')::[]) =>
1.213 ((map (split_did o term_of o the o (parse thy)) re')
1.214 - handle _ => raise error
1.215 + handle _ => error
1.216 ("prep_pbt: syntax error in '#Relate' of "^
1.217 (strs2str metID)))
1.218 | _ =>
1.219 - (raise error ("prep_pbt: more than one '#Relate' in "^
1.220 + (error ("prep_pbt: more than one '#Relate' in "^
1.221 (strs2str metID))));
1.222 val re = map (pair "#Relate") re;
1.223
1.224 @@ -772,11 +772,11 @@
1.225 [] => []
1.226 | ((_,wh')::[]) =>
1.227 ((map (parse_patt thy) wh')
1.228 - handle _ => raise error
1.229 + handle _ => error
1.230 ("prep_pbt: syntax error in '#Where' of "^
1.231 (strs2str metID)))
1.232 | _ =>
1.233 - (raise error ("prep_pbt: more than one '#Where' in "^
1.234 + (error ("prep_pbt: more than one '#Where' in "^
1.235 (strs2str metID))));
1.236 val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
1.237 in ({guh=guh,mathauthors=maa,init=init,
1.238 @@ -907,7 +907,7 @@
1.239 (case find_first (eq1 d) pbt of
1.240 (* val SOME (_,(_,id)) = find_first (eq1 d) pbt;
1.241 *)
1.242 - SOME (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
1.243 + SOME (_,(_,id)) => error "chk_: ((i,vats,b,f,Cor ((d,vs),\
1.244 \(id, pbl_ids' d vs))):itm)"
1.245 | NONE => (i,vats,false,f,Sup (d,[vs])));
1.246
1.247 @@ -1200,7 +1200,7 @@
1.248
1.249 (*. apply a fun to a ptyps node; copied from get_py .*)
1.250 fun app_ptyp f (d:pblID) _ [] =
1.251 - raise error ("app_ptyp not found: "^(strs2str d))
1.252 + error ("app_ptyp not found: "^(strs2str d))
1.253 | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =
1.254 if k=k' then f p
1.255 else app_ptyp f d ([k]:pblRD) pys
1.256 @@ -1247,15 +1247,15 @@
1.257 EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
1.258 fun pblID2guh (pblID:pblID) =
1.259 (((#guh o get_pbt) pblID)
1.260 - handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
1.261 + handle _ => error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
1.262 fun metID2guh (metID:metID) =
1.263 (((#guh o get_met) metID)
1.264 - handle _ => raise error ("metID2guh: no 'Met_' for '"^
1.265 + handle _ => error ("metID2guh: no 'Met_' for '"^
1.266 strs2str' metID ^ "'"));
1.267 fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
1.268 | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
1.269 | kestoreID2guh ketype kestoreID =
1.270 - raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
1.271 + error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
1.272 strs2str' kestoreID ^ "'");
1.273
1.274 fun show_pblguhs () =