more explicit markup for Token.Literal;
Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well;
Markup.operator for name of Args.syntax, to override outer keywords like "where";
tuned signature;

--- a/src/Pure/Isar/args.ML	Wed Mar 12 14:37:14 2014 +0100
+++ b/src/Pure/Isar/args.ML	Wed Mar 12 16:11:47 2014 +0100
@@ -102,7 +102,9 @@
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
     fun prt_arg arg =
       (case Token.get_value arg of
-        SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup v, s)
+        SOME (Token.Literal markup) =>
+          let val x = Token.content_of arg
+          in Pretty.mark_str (Token.keyword_markup markup x, x) end
       | SOME (Token.Text s) => Pretty.str (quote s)
       | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
@@ -113,7 +115,7 @@
 
 (* check *)
 
-fun check_src ctxt table (Src {name = (xname, pos), args, output_info}) =
+fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
   let
     val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
     val space = Name_Space.space_of_table table;
@@ -157,12 +159,15 @@
 
 val string = token (Parse.string || Parse.verbatim);
 val alt_string = token Parse.alt_string;
-val symbolic = token Parse.keyword_ident_or_symbolic;
+val symbolic = token (Parse.keyword_with Token.ident_or_symbolic);
 
 fun $$$ x =
   (ident || token Parse.keyword) :|-- (fn tok =>
-    let val y = Token.content_of tok
-    in if x = y then (Token.assign (SOME (Token.Literal x)) tok; Scan.succeed x) else Scan.fail end);
+    let val y = Token.content_of tok in
+      if x = y
+      then (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; Scan.succeed x)
+      else Scan.fail
+    end);
 
 
 val named = ident || string;
@@ -317,7 +322,7 @@
     val args1 = map Token.init_assignable args0;
     fun reported_text () =
       if Context_Position.is_visible_generic context then
-        maps (Token.reports_of_value o Token.closure) args1
+        ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1)
         |> map (fn (p, m) => Position.reported_text p m "")
         |> implode
       else "";

--- a/src/Pure/Isar/parse.ML	Wed Mar 12 14:37:14 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Wed Mar 12 16:11:47 2014 +0100
@@ -37,7 +37,6 @@
   val eof: string parser
   val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
-  val keyword_ident_or_symbolic: string parser
   val $$$ : string -> string parser
   val reserved: string -> string parser
   val semicolon: string parser
@@ -195,7 +194,6 @@
 val eof = kind Token.EOF;
 
 fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
-val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
 
 fun command_name x =
   group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
@@ -204,7 +202,8 @@
 
 fun $$$ x =
   group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
-    (keyword_with (fn y => x = y));
+    (Scan.ahead not_eof -- keyword_with (fn y => x = y))
+  >> (fn (tok, x) => (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; x));
 
 fun reserved x =
   group (fn () => "reserved identifier " ^ quote x)
@@ -270,7 +269,7 @@
 
 val path = group (fn () => "file name/path specification") name;
 
-val liberal_name = keyword_ident_or_symbolic || xname;
+val liberal_name = keyword_with Token.ident_or_symbolic || xname;
 
 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
 val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;

--- a/src/Pure/Isar/token.ML	Wed Mar 12 14:37:14 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Mar 12 16:11:47 2014 +0100
@@ -12,7 +12,7 @@
     Error of string | Sync | EOF
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   datatype value =
-    Literal of string | Text of string | Typ of typ | Term of term | Fact of thm list |
+    Literal of Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
     Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
@@ -42,7 +42,7 @@
   val inner_syntax_of: T -> string
   val source_position_of: T -> Symbol_Pos.source
   val content_of: T -> string
-  val value_markup: value -> Markup.T list
+  val keyword_markup: Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
   val report: T -> Position.report_text
   val markup: T -> Markup.T
@@ -87,7 +87,7 @@
 type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
 
 datatype value =
-  Literal of string |
+  Literal of Markup.T |
   Text of string |
   Typ of typ |
   Term of term |
@@ -253,15 +253,11 @@
   | Sync          => (Markup.control, "")
   | EOF           => (Markup.control, "");
 
+in
+
 fun keyword_markup keyword x =
   if Symbol.is_ascii_identifier x then keyword else Markup.operator;
 
-in
-
-fun value_markup (Literal x) =
-      keyword_markup Markup.quasi_keyword x :: Completion.suppress_abbrevs x
-  | value_markup _ = [];
-
 fun completion_report tok =
   if is_kind Keyword tok
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
@@ -332,10 +328,16 @@
 
 fun reports_of_value tok =
   (case get_value tok of
-    NONE => []
-  | SOME v =>
-      let val pos = pos_of tok
-      in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end);
+    SOME (Literal markup) =>
+      let
+        val pos = pos_of tok;
+        val x = content_of tok;
+      in
+        if Position.is_reported pos then
+          map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x)
+        else []
+      end
+  | _ => []);
 
 
 (* make values *)

--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 12 14:37:14 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 12 16:11:47 2014 +0100
@@ -653,6 +653,7 @@
       Markup.KEYWORD2 -> keyword2_color,
       Markup.KEYWORD3 -> keyword3_color,
       Markup.QUASI_KEYWORD -> quasi_keyword_color,
+      Markup.OPERATOR -> Color.BLACK,
       Markup.STRING -> Color.BLACK,
       Markup.ALTSTRING -> Color.BLACK,
       Markup.VERBATIM -> Color.BLACK,