src/Pure/Isar/toplevel.ML
changeset 60076 e24f59cba23c
parent 59990 a81dc82ecba3
child 60096 96a4765ba7d1
     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