src/HOL/Tools/Nitpick/nitpick.ML
changeset 47670 24babc4b1925
parent 47564 8074b18d8d76
child 47715 04400144c6fc
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 22 14:16:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 22 14:16:46 2012 +0200
     1.3 @@ -1048,7 +1048,10 @@
     1.4  
     1.5  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
     1.6                        step subst assm_ts orig_t =
     1.7 -  let val print_nt = if is_mode_nt mode then Output.urgent_message else K () in
     1.8 +  let
     1.9 +    val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
    1.10 +    val print_t = if mode = TPTP then Output.urgent_message else K ()
    1.11 +  in
    1.12      if getenv "KODKODI" = "" then
    1.13        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    1.14           that the "Nitpick_Examples" can be processed on any machine. *)
    1.15 @@ -1064,14 +1067,18 @@
    1.16                (pick_them_nits_in_term deadline state params mode i n step subst
    1.17                                        assm_ts) orig_t
    1.18            handle TOO_LARGE (_, details) =>
    1.19 -                 (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.20 +                 (print_t "% SZS status Unknown";
    1.21 +                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.22                 | TOO_SMALL (_, details) =>
    1.23 -                 (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.24 +                 (print_t "% SZS status Unknown";
    1.25 +                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.26                 | Kodkod.SYNTAX (_, details) =>
    1.27 -                 (print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
    1.28 +                 (print_t "% SZS status Unknown";
    1.29 +                  print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
    1.30                    unknown_outcome)
    1.31                 | TimeLimit.TimeOut =>
    1.32 -                 (print_nt "Nitpick ran out of time."; unknown_outcome)
    1.33 +                 (print_t "% SZS status TimedOut";
    1.34 +                  print_nt "Nitpick ran out of time."; unknown_outcome)
    1.35        in
    1.36          if expect = "" orelse outcome_code = expect then outcome
    1.37          else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")