more FIXMEs concerning bad catch-all exception handlers;
authorwenzelm
Wed Jan 12 15:15:51 2011 +0100 (2011-01-12)
changeset 4152242d13d00ccfb
parent 41521 c704c437ec74
child 41523 6c7f5d5b7e9a
more FIXMEs concerning bad catch-all exception handlers;
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/replay.ML
src/Tools/WWW_Find/find_theorems.ML
src/Tools/WWW_Find/scgi_server.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Wed Jan 12 15:09:26 2011 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Wed Jan 12 15:15:51 2011 +0100
     1.3 @@ -319,6 +319,7 @@
     1.4          val curmaps = HOL4TypeMaps.get thy
     1.5          val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
     1.6          val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
     1.7 +               (* FIXME avoid handle x *)
     1.8                 handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
     1.9                        warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
    1.10          val upd_thy = HOL4TypeMaps.put newmaps thy
     2.1 --- a/src/HOL/Import/import_syntax.ML	Wed Jan 12 15:09:26 2011 +0100
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Wed Jan 12 15:15:51 2011 +0100
     2.3 @@ -58,7 +58,7 @@
     2.4                      let
     2.5                          val _ = ImportRecorder.load_history thyname
     2.6                          val thy = Replay.import_thms thyname int_thms thmnames thy
     2.7 -                            handle x => (ImportRecorder.save_history thyname; raise x)
     2.8 +                            handle x => (ImportRecorder.save_history thyname; raise x)  (* FIXME avoid handle x ?? *)
     2.9                          val _ = ImportRecorder.save_history thyname
    2.10                          val _ = ImportRecorder.clear_history ()
    2.11                      in
     3.1 --- a/src/HOL/Import/replay.ML	Wed Jan 12 15:09:26 2011 +0100
     3.2 +++ b/src/HOL/Import/replay.ML	Wed Jan 12 15:15:51 2011 +0100
     3.3 @@ -275,7 +275,7 @@
     3.4          in
     3.5              x
     3.6          end
     3.7 -    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)
     3.8 +    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)  (* FIXME avoid handle x ?? *)
     3.9  
    3.10  fun setup_int_thms thyname thy =
    3.11      let
     4.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Wed Jan 12 15:09:26 2011 +0100
     4.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Wed Jan 12 15:15:51 2011 +0100
     4.3 @@ -231,7 +231,7 @@
     4.4        do_find ()
     4.5          handle
     4.6            ERROR msg => Xhtml.write send (html_error msg)
     4.7 -        | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
     4.8 +        | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e)); (* FIXME avoid handle e *)
     4.9      Xhtml.write_close send header
    4.10    end;
    4.11  in
     5.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Wed Jan 12 15:09:26 2011 +0100
     5.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Wed Jan 12 15:15:51 2011 +0100
     5.3 @@ -89,7 +89,7 @@
     5.4                   else f (req, get_content content_is, send)))
     5.5            end;
     5.6  
     5.7 -        fun thread_req () =
     5.8 +        fun thread_req () =  (* FIXME avoid handle e *)
     5.9            (do_req () handle e => (warning (exnMessage e));
    5.10             BinIO.closeOut sout handle e => warning (exnMessage e);
    5.11             BinIO.closeIn sin handle e => warning (exnMessage e);