# HG changeset patch
# User wenzelm
# Date 1294841751 -3600
# Node ID 42d13d00ccfb248fc771c2ea9f03041888897e91
# Parent  c704c437ec741fd923920fc0a82dc905a73751a9
more FIXMEs concerning bad catch-all exception handlers;

diff -r c704c437ec74 -r 42d13d00ccfb src/HOL/Import/hol4rews.ML
--- 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
diff -r c704c437ec74 -r 42d13d00ccfb src/HOL/Import/import_syntax.ML
--- 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
diff -r c704c437ec74 -r 42d13d00ccfb src/HOL/Import/replay.ML
--- 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
diff -r c704c437ec74 -r 42d13d00ccfb src/Tools/WWW_Find/find_theorems.ML
--- 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
diff -r c704c437ec74 -r 42d13d00ccfb src/Tools/WWW_Find/scgi_server.ML
--- 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);