Mirabelle: logging of exceptions (works only for PolyML)

--- a/src/HOL/Mirabelle/ROOT.ML	Wed Sep 02 22:12:40 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 14:05:13 2009 +0200
@@ -1,1 +1,2 @@
-use_thy "MirabelleTest";
+if can (unprefix "polyml") (getenv "ML_SYSTEM") then use_thy "MirabelleTest"
+else ();

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 22:12:40 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 14:05:13 2009 +0200
@@ -70,13 +70,13 @@
 
 fun log_sep thy = log thy "------------------"
 
-fun try_with f NONE = SOME ()
-  | try_with f (SOME e) = (f e; try (fn () => reraise e) ())
+fun log_exn thy name (exn : exn) = log thy ("Unhandled exception in action " ^
+  quote name ^ ":\n" ^ PolyML.makestring exn)
 
-fun capture_exns thy name f x =
-  (case try_with I (Exn.get_exn (Exn.capture f x)) of
-    NONE => (log thy ("Unhandled exception in " ^ quote name); log_sep thy)
-  | SOME _ => log_sep thy)
+fun try_with f g x = SOME (g x)
+  handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; NONE)
+
+fun capture_exns thy name f x = (try_with (log_exn thy name) f x; log_sep thy)
 
 fun apply_actions thy info (pre, post, time) actions =
   let

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 02 22:12:40 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 14:05:13 2009 +0200
@@ -83,12 +83,14 @@
     fun timed_metis thms =
       uncurry with_time (Mirabelle.cpu_time apply_metis thms)
       handle TimeLimit.TimeOut => "time out"
-    fun log_metis s = log ("-----\nmetis (sledgehammer): " ^ s)
+           | ERROR msg => "error: " ^ msg
+    fun log_metis s = log ("metis (sledgehammer): " ^ s)
   in
     if not (AList.defined (op =) args metisK) then ()
     else if is_none thm_names then ()
     else
-      these thm_names
+      log "-----"
+      |> K (these thm_names)
       |> get_thms (Proof.context_of st)
       |> timed_metis
       |> log_metis