# HG changeset patch
# User boehmes
# Date 1251732749 -7200
# Node ID ba0cf920a39c3d4766508ab26289e2e9039cc8f0
# Parent  0a13ae5d09c8764d0516494ac530f3a4ee422748
Mirabelle: handle possible parser exceptions, emit suitable log message

diff -r 0a13ae5d09c8 -r ba0cf920a39c src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 15:30:11 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 17:32:29 2009 +0200
@@ -63,11 +63,12 @@
     fun get_thms ctxt = maps (thms_of_name ctxt)
     fun metis thms ctxt = MetisTools.metis_tac ctxt thms
     fun apply_metis thms = "\nApplying metis with these theorems: " ^
-     (if try (Mirabelle.can_apply (metis thms)) st = SOME true
+     (if Mirabelle.can_apply (metis thms) st
       then "success"
       else "failure")
     val msg = if not (AList.defined (op =) args metisK) then ""
-      else apply_metis (get_thms (Proof.context_of st) (these thm_names))
+      else (apply_metis (get_thms (Proof.context_of st) (these thm_names))
+        handle ERROR m => "\nException: " ^ m)
   in
     if success
     then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)