# HG changeset patch
# User wenzelm
# Date 1394032404 -3600
# Node ID 2eb8c13339a55885ddbadbacf063d9ddb0efe405
# Parent  41e06ec17604b8f52fd7bdd8b0fd6f180e5ae00c
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;

diff -r 41e06ec17604 -r 2eb8c13339a5 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Mar 05 16:06:11 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Mar 05 16:13:24 2014 +0100
@@ -42,7 +42,6 @@
   val inner_syntax_of: T -> string
   val source_position_of: T -> Symbol_Pos.source
   val content_of: T -> string
-  val keyword_markup: string -> Markup.T
   val value_markup: value -> Markup.T list
   val completion_report: T -> Position.report_text list
   val report: T -> Position.report_text
@@ -254,14 +253,13 @@
   | Sync          => (Markup.control, "")
   | EOF           => (Markup.control, "");
 
+fun keyword_markup keyword x =
+  if Symbol.is_ascii_identifier x then keyword else Markup.operator;
+
 in
 
-fun keyword_markup x =
-  if Symbol.is_ascii_identifier x
-  then Markup.keyword2
-  else Markup.operator;
-
-fun value_markup (Literal x) = keyword_markup x :: Completion.suppress_abbrevs x
+fun value_markup (Literal x) =
+      keyword_markup Markup.quasi_keyword x :: Completion.suppress_abbrevs x
   | value_markup _ = [];
 
 fun completion_report tok =
@@ -271,7 +269,7 @@
 
 fun report tok =
   if is_kind Keyword tok then
-    ((pos_of tok, keyword_markup (content_of tok)), "")
+    ((pos_of tok, keyword_markup Markup.keyword2 (content_of tok)), "")
   else
     let val (m, text) = token_kind_markup (kind_of tok)
     in ((pos_of tok, m), text) end;
diff -r 41e06ec17604 -r 2eb8c13339a5 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Mar 05 16:06:11 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Mar 05 16:13:24 2014 +0100
@@ -114,6 +114,7 @@
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
+  val quasi_keywordN: string val quasi_keyword: T
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -419,6 +420,7 @@
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
+val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
 val (operatorN, operator) = markup_elem "operator";
 val (stringN, string) = markup_elem "string";
 val (altstringN, altstring) = markup_elem "altstring";
diff -r 41e06ec17604 -r 2eb8c13339a5 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Mar 05 16:06:11 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Mar 05 16:13:24 2014 +0100
@@ -215,6 +215,7 @@
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
+  val QUASI_KEYWORD = "quasi_keyword"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALTSTRING = "altstring"
diff -r 41e06ec17604 -r 2eb8c13339a5 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Mar 05 16:06:11 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Mar 05 16:13:24 2014 +0100
@@ -84,6 +84,7 @@
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
 option keyword3_color : string = "0099FFFF"
+option quasi_keyword_color : string = "66CCFFFF"
 option caret_invisible_color : string = "50000080"
 option completion_color : string = "0000FFFF"
 
diff -r 41e06ec17604 -r 2eb8c13339a5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 05 16:06:11 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 05 16:13:24 2014 +0100
@@ -239,6 +239,7 @@
   val keyword1_color = color_value("keyword1_color")
   val keyword2_color = color_value("keyword2_color")
   val keyword3_color = color_value("keyword3_color")
+  val quasi_keyword_color = color_value("quasi_keyword_color")
   val caret_invisible_color = color_value("caret_invisible_color")
   val completion_color = color_value("completion_color")
 
@@ -651,6 +652,7 @@
       Markup.KEYWORD1 -> keyword1_color,
       Markup.KEYWORD2 -> keyword2_color,
       Markup.KEYWORD3 -> keyword3_color,
+      Markup.QUASI_KEYWORD -> quasi_keyword_color,
       Markup.STRING -> Color.BLACK,
       Markup.ALTSTRING -> Color.BLACK,
       Markup.VERBATIM -> Color.BLACK,