tuned messages -- in accordance to Isabelle/Scala;
authorwenzelm
Mon Mar 10 22:14:53 2014 +0100 (2014-03-10)
changeset 560380e2dec666152
parent 56037 7b716baac02c
child 56039 5ff5208de089
tuned messages -- in accordance to Isabelle/Scala;
src/Pure/General/name_space.ML
src/Pure/Isar/args.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Mar 10 22:08:51 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Mar 10 22:14:53 2014 +0100
     1.3 @@ -99,10 +99,10 @@
     1.4    quote (Markup.markup (entry_markup false kind (name, entry)) name);
     1.5  
     1.6  fun err_dup kind entry1 entry2 pos =
     1.7 -  error ("Duplicate " ^ kind ^ " declaration " ^
     1.8 +  error ("Duplicate " ^ plain_words kind ^ " declaration " ^
     1.9      print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
    1.10  
    1.11 -fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
    1.12 +fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
    1.13  
    1.14  
    1.15  (* datatype T *)
     2.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 22:08:51 2014 +0100
     2.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 22:14:53 2014 +0100
     2.3 @@ -331,7 +331,7 @@
     2.4            val print_name =
     2.5              (case output_info of
     2.6                NONE => quote name
     2.7 -            | SOME (kind, markup) => kind ^ " " ^ quote (Markup.markup markup name));
     2.8 +            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
     2.9            val print_args =
    2.10              if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2);
    2.11          in
     3.1 --- a/src/Pure/library.ML	Mon Mar 10 22:08:51 2014 +0100
     3.2 +++ b/src/Pure/library.ML	Mon Mar 10 22:14:53 2014 +0100
     3.3 @@ -146,6 +146,7 @@
     3.4    val cat_lines: string list -> string
     3.5    val space_explode: string -> string -> string list
     3.6    val split_lines: string -> string list
     3.7 +  val plain_words: string -> string
     3.8    val prefix_lines: string -> string -> string
     3.9    val prefix: string -> string -> string
    3.10    val suffix: string -> string -> string
    3.11 @@ -745,6 +746,8 @@
    3.12  
    3.13  val split_lines = space_explode "\n";
    3.14  
    3.15 +fun plain_words s = space_explode "_" s |> space_implode " ";
    3.16 +
    3.17  fun prefix_lines "" txt = txt
    3.18    | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
    3.19