Mirabelle: handle possible parser exceptions, emit suitable log message
authorboehmes
Mon Aug 31 17:32:29 2009 +0200 (2009-08-31)
changeset 32460ba0cf920a39c
parent 32459 0a13ae5d09c8
child 32461 eee4fa79398f
child 32468 3e6f5365971e
Mirabelle: handle possible parser exceptions, emit suitable log message
src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
     1.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 15:30:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 17:32:29 2009 +0200
     1.3 @@ -63,11 +63,12 @@
     1.4      fun get_thms ctxt = maps (thms_of_name ctxt)
     1.5      fun metis thms ctxt = MetisTools.metis_tac ctxt thms
     1.6      fun apply_metis thms = "\nApplying metis with these theorems: " ^
     1.7 -     (if try (Mirabelle.can_apply (metis thms)) st = SOME true
     1.8 +     (if Mirabelle.can_apply (metis thms) st
     1.9        then "success"
    1.10        else "failure")
    1.11      val msg = if not (AList.defined (op =) args metisK) then ""
    1.12 -      else apply_metis (get_thms (Proof.context_of st) (these thm_names))
    1.13 +      else (apply_metis (get_thms (Proof.context_of st) (these thm_names))
    1.14 +        handle ERROR m => "\nException: " ^ m)
    1.15    in
    1.16      if success
    1.17      then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)