# HG changeset patch
# User wenzelm
# Date 1308393462 -7200
# Node ID 224006e5ac466ca457ff592ce7973c172a0b37bc
# Parent  f3d5cecfecdc0202c0cfd33ee56267a866b2aefa
inner literal/delimiter corresponds to outer keyword/operator;

diff -r f3d5cecfecdc -r 224006e5ac46 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Sat Jun 18 12:13:42 2011 +0200
+++ b/lib/html/isabelle.css	Sat Jun 18 12:37:42 2011 +0200
@@ -28,6 +28,7 @@
 .var, var                     { color: #00009B; }
 .numeral, numeral             { }
 .literal, literal             { font-weight: bold; }
+.delimiter, delimiter         { }
 .inner_string, inner_string   { color: #D2691E; }
 .inner_comment, inner_comment { color: #8B0000; }
 
diff -r f3d5cecfecdc -r 224006e5ac46 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jun 18 12:13:42 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Jun 18 12:37:42 2011 +0200
@@ -47,6 +47,7 @@
   val varN: string val var: T
   val numeralN: string val numeral: T
   val literalN: string val literal: T
+  val delimiterN: string val delimiter: T
   val inner_stringN: string val inner_string: T
   val inner_commentN: string val inner_comment: T
   val token_rangeN: string val token_range: T
@@ -223,6 +224,7 @@
 val (varN, var) = markup_elem "var";
 val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
+val (delimiterN, delimiter) = markup_elem "delimiter";
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
diff -r f3d5cecfecdc -r 224006e5ac46 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Jun 18 12:13:42 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Jun 18 12:37:42 2011 +0200
@@ -167,6 +167,7 @@
   val XNUM = "xnum"
   val XSTR = "xstr"
   val LITERAL = "literal"
+  val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"
   val INNER_COMMENT = "inner_comment"
 
diff -r f3d5cecfecdc -r 224006e5ac46 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Jun 18 12:13:42 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jun 18 12:37:42 2011 +0200
@@ -203,8 +203,11 @@
   | Comment     => Markup.inner_comment
   | EOF         => Markup.empty;
 
-fun report_token ctxt (Token (kind, _, (pos, _))) =
-  Context_Position.report ctxt pos (token_kind_markup kind);
+fun report_token ctxt (Token (kind, s, (pos, _))) =
+  let val markup =
+    if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
+    else token_kind_markup kind
+  in Context_Position.report ctxt pos markup end;
 
 fun reported_token_range ctxt tok =
   if is_proper tok
diff -r f3d5cecfecdc -r 224006e5ac46 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:13:42 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:37:42 2011 +0200
@@ -122,6 +122,7 @@
       Markup.INNER_COMMENT -> get_color("#8B0000"),
       Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
       Markup.LITERAL -> keyword1_color,
+      Markup.DELIMITER -> get_color("black"),
       Markup.ML_KEYWORD -> keyword1_color,
       Markup.ML_DELIMITER -> get_color("black"),
       Markup.ML_NUMERAL -> get_color("red"),