more uniform ML keyword markup;
authorwenzelm
Sat, 15 Feb 2014 18:28:18 +0100
changeset 55505 2a1ca7f6607b
parent 55504 4b6a5068a128
child 55506 46f3e31c5a87
more uniform ML keyword markup; tuned;
src/Pure/Isar/token.scala
src/Pure/ML/ml_lex.ML
src/Pure/ML/ml_lex.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
--- a/src/Pure/Isar/token.scala	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/Isar/token.scala	Sat Feb 15 18:28:18 2014 +0100
@@ -155,7 +155,7 @@
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
-  def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
+  def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_ident: Boolean = kind == Token.Kind.IDENT
   def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
   def is_string: Boolean = kind == Token.Kind.STRING
--- a/src/Pure/ML/ml_lex.ML	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sat Feb 15 18:28:18 2014 +0100
@@ -6,6 +6,7 @@
 
 signature ML_LEX =
 sig
+  val keywords: string list
   datatype token_kind =
     Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
     Space | Comment | Error of string | EOF
@@ -20,7 +21,6 @@
   val content_of: token -> string
   val check_content_of: token -> string
   val flatten: token list -> string
-  val keywords: string list
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
@@ -31,6 +31,28 @@
 structure ML_Lex: ML_LEX =
 struct
 
+(** keywords **)
+
+val keywords =
+ ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", "[",
+  "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", "case",
+  "datatype", "do", "else", "end", "eqtype", "exception", "fn", "fun",
+  "functor", "handle", "if", "in", "include", "infix", "infixr",
+  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise",
+  "rec", "sharing", "sig", "signature", "struct", "structure", "then",
+  "type", "val", "where", "while", "with", "withtype"];
+
+val keywords2 =
+ ["case", "do", "else", "end", "if", "in", "let", "local", "of",
+  "sig", "struct", "then", "while", "with"];
+
+val keywords3 =
+ ["handle", "open", "raise"];
+
+val lexicon = Scan.make_lexicon (map raw_explode keywords);
+
+
+
 (** tokens **)
 
 (* datatype token *)
@@ -69,6 +91,12 @@
 fun content_of (Token (_, (_, x))) = x;
 fun token_leq (tok, tok') = content_of tok <= content_of tok';
 
+fun is_keyword (Token (_, (Keyword, _))) = true
+  | is_keyword _ = false;
+
+fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x)
+  | is_delimiter _ = false;
+
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
   | is_regular _ = true;
@@ -104,7 +132,7 @@
 local
 
 val token_kind_markup =
- fn Keyword   => (Markup.ML_keyword, "")
+ fn Keyword   => (Markup.empty, "")
   | Ident     => (Markup.empty, "")
   | LongIdent => (Markup.empty, "")
   | TypeVar   => (Markup.ML_tvar, "")
@@ -118,15 +146,16 @@
   | Error msg => (Markup.bad, msg)
   | EOF       => (Markup.empty, "");
 
-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_of_token (Token ((pos, _), (kind, x))) =
-  let val (markup, txt) = token_markup kind x
+fun report_of_token (tok as Token ((pos, _), (kind, x))) =
+  let
+    val (markup, txt) =
+      if not (is_keyword tok) then token_kind_markup kind
+      else if is_delimiter tok then (Markup.ML_delimiter, "")
+      else if member (op =) keywords2 x then (Markup.ML_keyword2, "")
+      else if member (op =) keywords3 x then (Markup.ML_keyword3, "")
+      else (Markup.ML_keyword1, "");
   in ((pos, markup), txt) end;
 
 end;
@@ -142,20 +171,6 @@
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
-(* keywords *)
-
-val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
-  "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
-  "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",
-  "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",
-  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",
-  "sharing", "sig", "signature", "struct", "structure", "then", "type",
-  "val", "where", "while", "with", "withtype"];
-
-val lex = Scan.make_lexicon (map raw_explode keywords);
-fun scan_keyword x = Scan.literal lex x;
-
-
 (* identifiers *)
 
 local
@@ -258,7 +273,7 @@
   scan_blanks1 >> token Space ||
   Symbol_Pos.scan_comment err_prefix >> token Comment ||
   Scan.max token_leq
-   (scan_keyword >> token Keyword)
+   (Scan.literal lexicon >> token Keyword)
    (scan_word >> token Word ||
     scan_real >> token Real ||
     scan_int >> token Int ||
--- a/src/Pure/ML/ml_lex.scala	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sat Feb 15 18:28:18 2014 +0100
@@ -13,6 +13,29 @@
 
 object ML_Lex
 {
+  /** keywords **/
+
+  val keywords: Set[String] =
+    Set("#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>",
+      "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
+      "case", "datatype", "do", "else", "end", "eqtype", "exception",
+      "fn", "fun", "functor", "handle", "if", "in", "include",
+      "infix", "infixr", "let", "local", "nonfix", "of", "op", "open",
+      "orelse", "raise", "rec", "sharing", "sig", "signature",
+      "struct", "structure", "then", "type", "val", "where", "while",
+      "with", "withtype")
+
+  val keywords2: Set[String] =
+    Set("case", "do", "else", "end", "if", "in", "let", "local", "of",
+      "sig", "struct", "then", "while", "with")
+
+  val keywords3: Set[String] =
+    Set("handle", "open", "raise")
+
+  private val lexicon: Scan.Lexicon = Scan.Lexicon(keywords.toList: _*)
+
+
+
   /** tokens **/
 
   object Kind extends Enumeration
@@ -34,7 +57,7 @@
   sealed case class Token(val kind: Kind.Value, val source: String)
   {
     def is_keyword: Boolean = kind == Kind.KEYWORD
-    def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
+    def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   }
 
 
@@ -43,15 +66,6 @@
 
   case object ML_String extends Scan.Context
 
-  private val lexicon =
-    Scan.Lexicon("#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
-      "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
-      "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",
-      "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",
-      "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",
-      "sharing", "sig", "signature", "struct", "structure", "then", "type",
-      "val", "where", "while", "with", "withtype")
-
   private object Parsers extends Scan.Parsers
   {
     /* string material */
--- a/src/Pure/PIDE/markup.ML	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Feb 15 18:28:18 2014 +0100
@@ -68,7 +68,9 @@
   val propN: string val prop: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
-  val ML_keywordN: string val ML_keyword: T
+  val ML_keyword1N: string val ML_keyword1: T
+  val ML_keyword2N: string val ML_keyword2: T
+  val ML_keyword3N: string val ML_keyword3: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
@@ -325,7 +327,9 @@
 
 (* ML syntax *)
 
-val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
+val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
+val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3";
 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
--- a/src/Pure/PIDE/markup.scala	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Feb 15 18:28:18 2014 +0100
@@ -169,7 +169,9 @@
 
   /* ML syntax */
 
-  val ML_KEYWORD = "ML_keyword"
+  val ML_KEYWORD1 = "ML_keyword1"
+  val ML_KEYWORD2 = "ML_keyword2"
+  val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
--- a/src/Tools/jEdit/etc/options	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Feb 15 18:28:18 2014 +0100
@@ -83,6 +83,7 @@
 option active_result_color : string = "999966FF"
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
+option keyword3_color : string = "0099FFFF"
 
 option tfree_color : string = "A020F0FF"
 option tvar_color : string = "A020F0FF"
--- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 18:28:18 2014 +0100
@@ -108,23 +108,17 @@
 
   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
-    else if (token.is_operator) JEditToken.OPERATOR
+    else if (token.is_delimiter) JEditToken.OPERATOR
     else token_style(token.kind)
 
 
   /* Isabelle/ML token markup */
 
-  private val ml_keyword2: Set[String] =
-    Set("case", "do", "else", "end", "if", "in", "let", "local", "of",
-      "sig", "struct", "then", "while", "with")
-
-  private val ml_keyword3: Set[String] =
-    Set("handle", "open", "raise")
-
   private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
   {
     import JEditToken._
     Map[ML_Lex.Kind.Value, Byte](
+      ML_Lex.Kind.KEYWORD -> NULL,
       ML_Lex.Kind.IDENT -> NULL,
       ML_Lex.Kind.LONG_IDENT -> NULL,
       ML_Lex.Kind.TYPE_VAR -> NULL,
@@ -141,9 +135,9 @@
 
   def ml_token_markup(token: ML_Lex.Token): Byte =
     if (!token.is_keyword) ml_token_style(token.kind)
-    else if (token.is_operator) JEditToken.OPERATOR
-    else if (ml_keyword2(token.source)) JEditToken.KEYWORD2
-    else if (ml_keyword3(token.source)) JEditToken.KEYWORD3
+    else if (token.is_delimiter) JEditToken.OPERATOR
+    else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
+    else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
     else JEditToken.KEYWORD1
 }
 
@@ -183,6 +177,7 @@
   val active_result_color = color_value("active_result_color")
   val keyword1_color = color_value("keyword1_color")
   val keyword2_color = color_value("keyword2_color")
+  val keyword3_color = color_value("keyword3_color")
 
   val tfree_color = color_value("tfree_color")
   val tvar_color = color_value("tvar_color")
@@ -634,7 +629,9 @@
       Markup.INNER_CARTOUCHE -> inner_cartouche_color,
       Markup.INNER_COMMENT -> inner_comment_color,
       Markup.DYNAMIC_FACT -> dynamic_color,
-      Markup.ML_KEYWORD -> keyword1_color,
+      Markup.ML_KEYWORD1 -> keyword1_color,
+      Markup.ML_KEYWORD2 -> keyword2_color,
+      Markup.ML_KEYWORD3 -> keyword3_color,
       Markup.ML_DELIMITER -> Color.BLACK,
       Markup.ML_NUMERAL -> inner_numeral_color,
       Markup.ML_CHAR -> inner_quoted_color,