# HG changeset patch
# User wenzelm
# Date 1393345400 -3600
# Node ID b865c3035d5cebc56857a3b2b726f31c51373f4b
# Parent  4a4e5686e091f254b20f7edc1a9315bb96df572c
tuned message -- more markup;

diff -r 4a4e5686e091 -r b865c3035d5c src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Feb 25 17:03:55 2014 +0100
+++ b/src/Pure/Isar/args.ML	Tue Feb 25 17:23:20 2014 +0100
@@ -89,7 +89,7 @@
       | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
       | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
-      | _ => Pretty.str (Token.unparse arg));
+      | _ => Pretty.mark_str (#1 (Token.markup arg), Token.unparse arg));
     val (s, args) = #1 (dest_src src);
   in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
 
@@ -291,8 +291,8 @@
   (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
     (SOME x, (st', [])) => (x, st')
   | (_, (_, args')) =>
-      error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments" ^
-        (if null args' then "" else "\n  " ^ space_implode " " (map Token.unparse args'))));
+      error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
+        (if null args' then "" else ":\n  " ^ space_implode " " (map Token.print args'))));
 
 fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
 
diff -r 4a4e5686e091 -r b865c3035d5c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Feb 25 17:03:55 2014 +0100
+++ b/src/Pure/Isar/token.ML	Tue Feb 25 17:23:20 2014 +0100
@@ -44,6 +44,7 @@
   val content_of: T -> string
   val markup: T -> Markup.T * string
   val unparse: T -> string
+  val print: T -> string
   val text_of: T -> string * string
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
@@ -263,6 +264,8 @@
   | EOF => ""
   | _ => x);
 
+fun print tok = Markup.markup (#1 (markup tok)) (unparse tok);
+
 fun text_of tok =
   if is_semicolon tok then ("terminator", "")
   else