tuned messages;
authorwenzelm
Wed Apr 15 14:54:25 2015 +0200 (2015-04-15)
changeset 60076e24f59cba23c
parent 60075 b079ee0e766c
child 60077 55cb9462e602
tuned messages;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 15 14:01:28 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 15 14:54:25 2015 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    val empty: transition
     1.5    val name_of: transition -> string
     1.6    val pos_of: transition -> Position.T
     1.7 -  val type_error: transition -> state -> string
     1.8 +  val type_error: transition -> string
     1.9    val name: string -> transition -> transition
    1.10    val position: Position.T -> transition -> transition
    1.11    val init_theory: (unit -> theory) -> transition -> transition
    1.12 @@ -309,11 +309,12 @@
    1.13  fun name_of (Transition {name, ...}) = name;
    1.14  fun pos_of (Transition {pos, ...}) = pos;
    1.15  
    1.16 -fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr);
    1.17 -fun at_command tr = command_msg "At " tr;
    1.18 +fun command_msg msg tr =
    1.19 +  msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^
    1.20 +    Position.here (pos_of tr);
    1.21  
    1.22 -fun type_error tr state =
    1.23 -  command_msg "Illegal application of " tr ^ " " ^ str_of_state state;
    1.24 +fun at_command tr = command_msg "At " tr;
    1.25 +fun type_error tr = command_msg "Bad context for " tr;
    1.26  
    1.27  
    1.28  (* modify transitions *)
    1.29 @@ -569,9 +570,7 @@
    1.30        val timing_props =
    1.31          Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
    1.32        val _ = Timing.protocol_message timing_props timing_result;
    1.33 -    in
    1.34 -      (result, Option.map (fn UNDEF => ERROR (type_error tr state) | exn => exn) opt_err)
    1.35 -    end);
    1.36 +    in (result, Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) opt_err) end);
    1.37  
    1.38  in
    1.39  
     2.1 --- a/src/Pure/PIDE/command.ML	Wed Apr 15 14:01:28 2015 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Apr 15 14:54:25 2015 +0200
     2.3 @@ -170,7 +170,7 @@
     2.4    in
     2.5      (case res of
     2.6        NONE => st0
     2.7 -    | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
     2.8 +    | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st))
     2.9    end) ();
    2.10  
    2.11  fun run keywords int tr st =