# HG changeset patch
# User wenzelm
# Date 1429102465 -7200
# Node ID e24f59cba23cffcd15629efbfad6e6425cfa5357
# Parent  b079ee0e766cb15797a0b55b67840b464b84095a
tuned messages;

diff -r b079ee0e766c -r e24f59cba23c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Apr 15 14:01:28 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 15 14:54:25 2015 +0200
@@ -31,7 +31,7 @@
   val empty: transition
   val name_of: transition -> string
   val pos_of: transition -> Position.T
-  val type_error: transition -> state -> string
+  val type_error: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
@@ -309,11 +309,12 @@
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
 
-fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr);
-fun at_command tr = command_msg "At " tr;
+fun command_msg msg tr =
+  msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^
+    Position.here (pos_of tr);
 
-fun type_error tr state =
-  command_msg "Illegal application of " tr ^ " " ^ str_of_state state;
+fun at_command tr = command_msg "At " tr;
+fun type_error tr = command_msg "Bad context for " tr;
 
 
 (* modify transitions *)
@@ -569,9 +570,7 @@
       val timing_props =
         Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
       val _ = Timing.protocol_message timing_props timing_result;
-    in
-      (result, Option.map (fn UNDEF => ERROR (type_error tr state) | exn => exn) opt_err)
-    end);
+    in (result, Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) opt_err) end);
 
 in
 
diff -r b079ee0e766c -r e24f59cba23c src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Apr 15 14:01:28 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Apr 15 14:54:25 2015 +0200
@@ -170,7 +170,7 @@
   in
     (case res of
       NONE => st0
-    | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
+    | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st))
   end) ();
 
 fun run keywords int tr st =