--- a/src/HOL/Import/hol4rews.ML Wed Jan 12 15:09:26 2011 +0100
+++ b/src/HOL/Import/hol4rews.ML Wed Jan 12 15:15:51 2011 +0100
@@ -319,6 +319,7 @@
val curmaps = HOL4TypeMaps.get thy
val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
+ (* FIXME avoid handle x *)
handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
val upd_thy = HOL4TypeMaps.put newmaps thy
--- a/src/HOL/Import/import_syntax.ML Wed Jan 12 15:09:26 2011 +0100
+++ b/src/HOL/Import/import_syntax.ML Wed Jan 12 15:15:51 2011 +0100
@@ -58,7 +58,7 @@
let
val _ = ImportRecorder.load_history thyname
val thy = Replay.import_thms thyname int_thms thmnames thy
- handle x => (ImportRecorder.save_history thyname; raise x)
+ handle x => (ImportRecorder.save_history thyname; raise x) (* FIXME avoid handle x ?? *)
val _ = ImportRecorder.save_history thyname
val _ = ImportRecorder.clear_history ()
in
--- a/src/HOL/Import/replay.ML Wed Jan 12 15:09:26 2011 +0100
+++ b/src/HOL/Import/replay.ML Wed Jan 12 15:15:51 2011 +0100
@@ -275,7 +275,7 @@
in
x
end
- end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)
+ end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x) (* FIXME avoid handle x ?? *)
fun setup_int_thms thyname thy =
let
--- a/src/Tools/WWW_Find/find_theorems.ML Wed Jan 12 15:09:26 2011 +0100
+++ b/src/Tools/WWW_Find/find_theorems.ML Wed Jan 12 15:15:51 2011 +0100
@@ -231,7 +231,7 @@
do_find ()
handle
ERROR msg => Xhtml.write send (html_error msg)
- | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
+ | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e)); (* FIXME avoid handle e *)
Xhtml.write_close send header
end;
in
--- a/src/Tools/WWW_Find/scgi_server.ML Wed Jan 12 15:09:26 2011 +0100
+++ b/src/Tools/WWW_Find/scgi_server.ML Wed Jan 12 15:15:51 2011 +0100
@@ -89,7 +89,7 @@
else f (req, get_content content_is, send)))
end;
- fun thread_req () =
+ fun thread_req () = (* FIXME avoid handle e *)
(do_req () handle e => (warning (exnMessage e));
BinIO.closeOut sout handle e => warning (exnMessage e);
BinIO.closeIn sin handle e => warning (exnMessage e);