--- 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,