# HG changeset patch
# User wenzelm
# Date 1275228013 -7200
# Node ID e87d305a44905499d9064a9c13ce618a56f0eec5
# Parent  825456e5db3029a46122cbc5d0a5aaeded89b3d4
separate markup for ML delimiters;

diff -r 825456e5db30 -r e87d305a4490 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun May 30 15:27:49 2010 +0200
+++ b/src/Pure/General/markup.ML	Sun May 30 16:00:13 2010 +0200
@@ -63,6 +63,7 @@
   val attributeN: string val attribute: string -> T
   val methodN: string val method: string -> T
   val ML_keywordN: string val ML_keyword: T
+  val ML_delimiterN: string val ML_delimiter: T
   val ML_identN: string val ML_ident: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
@@ -239,6 +240,7 @@
 (* ML syntax *)
 
 val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_identN, ML_ident) = markup_elem "ML_ident";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
diff -r 825456e5db30 -r e87d305a4490 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun May 30 15:27:49 2010 +0200
+++ b/src/Pure/General/markup.scala	Sun May 30 16:00:13 2010 +0200
@@ -123,6 +123,7 @@
   /* ML syntax */
 
   val ML_KEYWORD = "ML_keyword"
+  val ML_DELIMITER = "ML_delimiter"
   val ML_IDENT = "ML_ident"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
diff -r 825456e5db30 -r e87d305a4490 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun May 30 15:27:49 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sun May 30 16:00:13 2010 +0200
@@ -88,6 +88,8 @@
 
 (* markup *)
 
+local
+
 val token_kind_markup =
  fn Keyword   => Markup.ML_keyword
   | Ident     => Markup.ML_ident
@@ -103,8 +105,16 @@
   | Error _   => Markup.ML_malformed
   | EOF       => Markup.none;
 
-fun report_token (Token ((pos, _), (kind, _))) =
-  Position.report (token_kind_markup kind) pos;
+fun token_markup kind x =
+  if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
+  then Markup.ML_delimiter
+  else token_kind_markup kind;
+
+in
+
+fun report_token (Token ((pos, _), (kind, x))) = Position.report (token_markup kind x) pos;
+
+end;
 
 
 
diff -r 825456e5db30 -r e87d305a4490 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 15:27:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 16:00:13 2010 +0200
@@ -67,6 +67,7 @@
       Markup.METHOD -> NULL,
       // ML syntax
       Markup.ML_KEYWORD -> KEYWORD1,
+      Markup.ML_DELIMITER -> OPERATOR,
       Markup.ML_IDENT -> NULL,
       Markup.ML_TVAR -> NULL,
       Markup.ML_NUMERAL -> DIGIT,