tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
--- a/src/Pure/General/scan.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/General/scan.ML Mon Aug 30 15:19:39 2010 +0200
@@ -105,7 +105,7 @@
fun catch scan xs = scan xs
handle ABORT msg => raise Fail msg
- | FAIL msg => raise Fail (the_default "Syntax error." msg);
+ | FAIL msg => raise Fail (the_default "Syntax error" msg);
(* scanner combinators *)
--- a/src/Pure/Isar/class_declaration.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Mon Aug 30 15:19:39 2010 +0200
@@ -126,8 +126,8 @@
else error ("Type inference imposes additional sort constraint "
^ Syntax.string_of_sort_global thy inferred_sort
^ " of type parameter " ^ Name.aT ^ " of sort "
- ^ Syntax.string_of_sort_global thy a_sort ^ ".")
- | _ => error "Multiple type variables in class specification.";
+ ^ Syntax.string_of_sort_global thy a_sort)
+ | _ => error "Multiple type variables in class specification";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
val after_infer_fixate = (map o map_atyps)
(fn T as TFree _ => T | T as TVar (vi, sort) =>
--- a/src/Pure/Isar/obtain.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Aug 30 15:19:39 2010 +0200
@@ -181,7 +181,7 @@
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
- | [] => error "Goal solved -- nothing guessed."
+ | [] => error "Goal solved -- nothing guessed"
| _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
fun result tac facts ctxt =
--- a/src/Pure/Isar/runtime.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Mon Aug 30 15:19:39 2010 +0200
@@ -58,10 +58,10 @@
| exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
| exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
- | exn_msgs _ TERMINATE = ["Exit."]
+ | exn_msgs _ TERMINATE = ["Exit"]
| exn_msgs _ Exn.Interrupt = []
- | exn_msgs _ TimeLimit.TimeOut = ["Timeout."]
- | exn_msgs _ TOPLEVEL_ERROR = ["Error."]
+ | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
+ | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
| exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
| exn_msgs _ (ERROR msg) = [msg]
| exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
@@ -82,7 +82,7 @@
fun exn_message exn_position exn =
(case exn_messages exn_position exn of
- [] => "Interrupt."
+ [] => "Interrupt"
| msgs => cat_lines msgs);
--- a/src/Pure/Isar/toplevel.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Aug 30 15:19:39 2010 +0200
@@ -356,7 +356,7 @@
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
fun command_msg msg tr = msg ^ "command " ^ str_of tr;
-fun at_command tr = command_msg "At " tr ^ ".";
+fun at_command tr = command_msg "At " tr;
fun type_error tr state =
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
--- a/src/Pure/Syntax/parser.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/Syntax/parser.ML Mon Aug 30 15:19:39 2010 +0200
@@ -773,7 +773,7 @@
if not (! warned) andalso
length (new_states @ States) > ! branching_level then
(Context_Position.if_visible ctxt warning
- "Currently parsed expression could be extremely ambiguous.";
+ "Currently parsed expression could be extremely ambiguous";
warned := true)
else ();
in
--- a/src/Pure/goal.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/goal.ML Mon Aug 30 15:19:39 2010 +0200
@@ -159,7 +159,7 @@
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
SOME th => Drule.implies_intr_list casms
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
- | NONE => error "Tactic failed.");
+ | NONE => error "Tactic failed");
(* prove_common etc. *)
@@ -191,7 +191,7 @@
fun result () =
(case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
- NONE => err "Tactic failed."
+ NONE => err "Tactic failed"
| SOME st =>
let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]