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]