src/Pure/Isar/runtime.ML
changeset 38875 c7a66b584147
parent 38874 4a4d34d2f97b
child 39232 69c6d3e87660
     1.1 --- a/src/Pure/Isar/runtime.ML	Mon Aug 30 15:09:20 2010 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Mon Aug 30 15:19:39 2010 +0200
     1.3 @@ -58,10 +58,10 @@
     1.4        | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
     1.5        | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
     1.6            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
     1.7 -      | exn_msgs _ TERMINATE = ["Exit."]
     1.8 +      | exn_msgs _ TERMINATE = ["Exit"]
     1.9        | exn_msgs _ Exn.Interrupt = []
    1.10 -      | exn_msgs _ TimeLimit.TimeOut = ["Timeout."]
    1.11 -      | exn_msgs _ TOPLEVEL_ERROR = ["Error."]
    1.12 +      | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
    1.13 +      | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
    1.14        | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
    1.15        | exn_msgs _ (ERROR msg) = [msg]
    1.16        | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
    1.17 @@ -82,7 +82,7 @@
    1.18  
    1.19  fun exn_message exn_position exn =
    1.20    (case exn_messages exn_position exn of
    1.21 -    [] => "Interrupt."
    1.22 +    [] => "Interrupt"
    1.23    | msgs => cat_lines msgs);
    1.24  
    1.25