# HG changeset patch
# User wenzelm
# Date 1394486093 -3600
# Node ID 0e2dec6661521f05d5a2941b618c52249172116f
# Parent  7b716baac02c5c32bb1c5b7b3a4a2685706e7ae7
tuned messages -- in accordance to Isabelle/Scala;

diff -r 7b716baac02c -r 0e2dec666152 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Mar 10 22:08:51 2014 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 10 22:14:53 2014 +0100
@@ -99,10 +99,10 @@
   quote (Markup.markup (entry_markup false kind (name, entry)) name);
 
 fun err_dup kind entry1 entry2 pos =
-  error ("Duplicate " ^ kind ^ " declaration " ^
+  error ("Duplicate " ^ plain_words kind ^ " declaration " ^
     print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
 
-fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
+fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
 
 
 (* datatype T *)
diff -r 7b716baac02c -r 0e2dec666152 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 10 22:08:51 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 22:14:53 2014 +0100
@@ -331,7 +331,7 @@
           val print_name =
             (case output_info of
               NONE => quote name
-            | SOME (kind, markup) => kind ^ " " ^ quote (Markup.markup markup name));
+            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
           val print_args =
             if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2);
         in
diff -r 7b716baac02c -r 0e2dec666152 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Mar 10 22:08:51 2014 +0100
+++ b/src/Pure/library.ML	Mon Mar 10 22:14:53 2014 +0100
@@ -146,6 +146,7 @@
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
+  val plain_words: string -> string
   val prefix_lines: string -> string -> string
   val prefix: string -> string -> string
   val suffix: string -> string -> string
@@ -745,6 +746,8 @@
 
 val split_lines = space_explode "\n";
 
+fun plain_words s = space_explode "_" s |> space_implode " ";
+
 fun prefix_lines "" txt = txt
   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;