tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
authorwenzelm
Mon Aug 30 15:19:39 2010 +0200 (2010-08-30)
changeset 38875c7a66b584147
parent 38874 4a4d34d2f97b
child 38876 ec7045139e70
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
src/Pure/General/scan.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/Syntax/parser.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/General/scan.ML	Mon Aug 30 15:09:20 2010 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Mon Aug 30 15:19:39 2010 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5  fun catch scan xs = scan xs
     1.6    handle ABORT msg => raise Fail msg
     1.7 -    | FAIL msg => raise Fail (the_default "Syntax error." msg);
     1.8 +    | FAIL msg => raise Fail (the_default "Syntax error" msg);
     1.9  
    1.10  
    1.11  (* scanner combinators *)
     2.1 --- a/src/Pure/Isar/class_declaration.ML	Mon Aug 30 15:09:20 2010 +0200
     2.2 +++ b/src/Pure/Isar/class_declaration.ML	Mon Aug 30 15:19:39 2010 +0200
     2.3 @@ -126,8 +126,8 @@
     2.4                  else error ("Type inference imposes additional sort constraint "
     2.5                    ^ Syntax.string_of_sort_global thy inferred_sort
     2.6                    ^ " of type parameter " ^ Name.aT ^ " of sort "
     2.7 -                  ^ Syntax.string_of_sort_global thy a_sort ^ ".")
     2.8 -            | _ => error "Multiple type variables in class specification.";
     2.9 +                  ^ Syntax.string_of_sort_global thy a_sort)
    2.10 +            | _ => error "Multiple type variables in class specification";
    2.11        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
    2.12      val after_infer_fixate = (map o map_atyps)
    2.13        (fn T as TFree _ => T | T as TVar (vi, sort) =>
     3.1 --- a/src/Pure/Isar/obtain.ML	Mon Aug 30 15:09:20 2010 +0200
     3.2 +++ b/src/Pure/Isar/obtain.ML	Mon Aug 30 15:19:39 2010 +0200
     3.3 @@ -181,7 +181,7 @@
     3.4        if Thm.concl_of th aconv thesis andalso
     3.5          Logic.strip_assums_concl prem aconv thesis then th
     3.6        else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
     3.7 -  | [] => error "Goal solved -- nothing guessed."
     3.8 +  | [] => error "Goal solved -- nothing guessed"
     3.9    | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
    3.10  
    3.11  fun result tac facts ctxt =
     4.1 --- a/src/Pure/Isar/runtime.ML	Mon Aug 30 15:09:20 2010 +0200
     4.2 +++ b/src/Pure/Isar/runtime.ML	Mon Aug 30 15:19:39 2010 +0200
     4.3 @@ -58,10 +58,10 @@
     4.4        | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
     4.5        | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
     4.6            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
     4.7 -      | exn_msgs _ TERMINATE = ["Exit."]
     4.8 +      | exn_msgs _ TERMINATE = ["Exit"]
     4.9        | exn_msgs _ Exn.Interrupt = []
    4.10 -      | exn_msgs _ TimeLimit.TimeOut = ["Timeout."]
    4.11 -      | exn_msgs _ TOPLEVEL_ERROR = ["Error."]
    4.12 +      | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
    4.13 +      | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
    4.14        | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
    4.15        | exn_msgs _ (ERROR msg) = [msg]
    4.16        | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
    4.17 @@ -82,7 +82,7 @@
    4.18  
    4.19  fun exn_message exn_position exn =
    4.20    (case exn_messages exn_position exn of
    4.21 -    [] => "Interrupt."
    4.22 +    [] => "Interrupt"
    4.23    | msgs => cat_lines msgs);
    4.24  
    4.25  
     5.1 --- a/src/Pure/Isar/toplevel.ML	Mon Aug 30 15:09:20 2010 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Aug 30 15:19:39 2010 +0200
     5.3 @@ -356,7 +356,7 @@
     5.4  fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
     5.5  
     5.6  fun command_msg msg tr = msg ^ "command " ^ str_of tr;
     5.7 -fun at_command tr = command_msg "At " tr ^ ".";
     5.8 +fun at_command tr = command_msg "At " tr;
     5.9  
    5.10  fun type_error tr state =
    5.11    ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
     6.1 --- a/src/Pure/Syntax/parser.ML	Mon Aug 30 15:09:20 2010 +0200
     6.2 +++ b/src/Pure/Syntax/parser.ML	Mon Aug 30 15:19:39 2010 +0200
     6.3 @@ -773,7 +773,7 @@
     6.4                    if not (! warned) andalso
     6.5                       length (new_states @ States) > ! branching_level then
     6.6                      (Context_Position.if_visible ctxt warning
     6.7 -                      "Currently parsed expression could be extremely ambiguous.";
     6.8 +                      "Currently parsed expression could be extremely ambiguous";
     6.9                       warned := true)
    6.10                    else ();
    6.11                in
     7.1 --- a/src/Pure/goal.ML	Mon Aug 30 15:09:20 2010 +0200
     7.2 +++ b/src/Pure/goal.ML	Mon Aug 30 15:19:39 2010 +0200
     7.3 @@ -159,7 +159,7 @@
     7.4    (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
     7.5      SOME th => Drule.implies_intr_list casms
     7.6        (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
     7.7 -  | NONE => error "Tactic failed.");
     7.8 +  | NONE => error "Tactic failed");
     7.9  
    7.10  
    7.11  (* prove_common etc. *)
    7.12 @@ -191,7 +191,7 @@
    7.13  
    7.14      fun result () =
    7.15        (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
    7.16 -        NONE => err "Tactic failed."
    7.17 +        NONE => err "Tactic failed"
    7.18        | SOME st =>
    7.19            let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
    7.20              if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]