do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
authorwenzelm
Mon Jul 12 20:21:39 2010 +0200 (2010-07-12)
changeset 3777887b5dfe00387
parent 37777 22107b894e5a
child 37779 982b0668dcbd
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
use up-to-date ML_Compiler.exn_message;
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Jul 12 18:59:38 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Jul 12 20:21:39 2010 +0200
     1.3 @@ -175,10 +175,6 @@
     1.4  exception PK of string * string
     1.5  fun ERR f mesg = PK (f,mesg)
     1.6  
     1.7 -fun print_exn e =
     1.8 -    case e of
     1.9 -        PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
    1.10 -      | _ => OldGoals.print_exn e
    1.11  
    1.12  (* Compatibility. *)
    1.13  
    1.14 @@ -1311,8 +1307,10 @@
    1.15                      end
    1.16                    | NONE => (thy,NONE)
    1.17              end
    1.18 -    end
    1.19 -    handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE))
    1.20 +    end  (* FIXME avoid handle _ *)
    1.21 +    handle e =>
    1.22 +      (if_debug (fn () => writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
    1.23 +        (thy,NONE))
    1.24  
    1.25  fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
    1.26    let
    1.27 @@ -1974,7 +1972,6 @@
    1.28      in
    1.29          (thy22',hth)
    1.30      end
    1.31 -    handle e => (message "exception in new_definition"; print_exn e)
    1.32  
    1.33  local
    1.34      val helper = thm "termspec_help"
    1.35 @@ -2056,7 +2053,6 @@
    1.36          in
    1.37              intern_store_thm false thyname thmname hth thy''
    1.38          end
    1.39 -        handle e => (message "exception in new_specification"; print_exn e)
    1.40  
    1.41  end
    1.42  
    1.43 @@ -2137,7 +2133,6 @@
    1.44          in
    1.45              (thy6,hth')
    1.46          end
    1.47 -        handle e => (message "exception in new_type_definition"; print_exn e)
    1.48  
    1.49  fun add_dump_syntax thy name =
    1.50      let
    1.51 @@ -2230,7 +2225,6 @@
    1.52          in
    1.53              (thy,hth')
    1.54          end
    1.55 -        handle e => (message "exception in type_introduction"; print_exn e)
    1.56  end
    1.57  
    1.58  val prin = prin
     2.1 --- a/src/HOL/Import/replay.ML	Mon Jul 12 18:59:38 2010 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Mon Jul 12 20:21:39 2010 +0200
     2.3 @@ -272,12 +272,12 @@
     2.4              end
     2.5      in
     2.6          let
     2.7 -            val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
     2.8 +            val x = rp' prf thy
     2.9              val _ = ImportRecorder.stop_replay_proof thyname thmname
    2.10          in
    2.11              x
    2.12          end
    2.13 -    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
    2.14 +    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)
    2.15  
    2.16  fun setup_int_thms thyname thy =
    2.17      let
     3.1 --- a/src/HOL/Import/shuffler.ML	Mon Jul 12 18:59:38 2010 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Mon Jul 12 20:21:39 2010 +0200
     3.3 @@ -219,7 +219,7 @@
     3.4          val rew = Logic.mk_equals (lhs,rhs)
     3.5          val init = Thm.trivial (cterm_of thy rew)
     3.6      in
     3.7 -        (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
     3.8 +        all_comm RS init
     3.9      end
    3.10  
    3.11  fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    3.12 @@ -315,7 +315,7 @@
    3.13      in
    3.14          case t of
    3.15              Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
    3.16 -            ((if eta_redex P andalso eta_redex Q
    3.17 +            (if eta_redex P andalso eta_redex Q
    3.18                then
    3.19                    let
    3.20                        val cert = cterm_of thy
    3.21 @@ -340,7 +340,6 @@
    3.22                         SOME res
    3.23                    end
    3.24                else NONE)
    3.25 -             handle e => OldGoals.print_exn e)
    3.26            | _ => NONE
    3.27         end
    3.28  
    3.29 @@ -521,7 +520,7 @@
    3.30      in
    3.31          Drule.forall_intr_list (map (cterm_of thy) vars) th
    3.32      end
    3.33 -    handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
    3.34 +
    3.35  
    3.36  (* Normalizes a theorem's conclusion using norm_term. *)
    3.37  
    3.38 @@ -618,7 +617,6 @@
    3.39                                          else error "Internal error in set_prop"
    3.40               | NONE => NONE
    3.41      end
    3.42 -    handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
    3.43  
    3.44  fun find_potential thy t =
    3.45      let