--- a/src/Pure/Isar/parse.ML Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/Isar/parse.ML Wed Dec 03 11:37:51 2014 +0100
@@ -185,15 +185,15 @@
val command_ = kind Token.Command;
val keyword = kind Token.Keyword;
val short_ident = kind Token.Ident;
-val long_ident = kind Token.LongIdent;
-val sym_ident = kind Token.SymIdent;
+val long_ident = kind Token.Long_Ident;
+val sym_ident = kind Token.Sym_Ident;
val term_var = kind Token.Var;
-val type_ident = kind Token.TypeIdent;
-val type_var = kind Token.TypeVar;
+val type_ident = kind Token.Type_Ident;
+val type_var = kind Token.Type_Var;
val number = kind Token.Nat;
val float_number = kind Token.Float;
val string = kind Token.String;
-val alt_string = kind Token.AltString;
+val alt_string = kind Token.Alt_String;
val verbatim = kind Token.Verbatim;
val cartouche = kind Token.Cartouche;
val eof = kind Token.EOF;
@@ -405,8 +405,8 @@
local
val argument_kinds =
- [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
- Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
+ [Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var,
+ Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim];
fun arguments is_symid =
let
--- a/src/Pure/Isar/token.ML Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/Isar/token.ML Wed Dec 03 11:37:51 2014 +0100
@@ -7,9 +7,13 @@
signature TOKEN =
sig
datatype kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
- Error of string | EOF
+ (*immediate source*)
+ Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
+ Float | Space |
+ (*delimited content*)
+ String | Alt_String | Verbatim | Cartouche | Comment |
+ (*special content*)
+ Error of string | Internal_Value | EOF
val str_of_kind: kind -> string
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
type T
@@ -101,32 +105,36 @@
(* token kind *)
datatype kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
- Error of string | EOF;
+ (*immediate source*)
+ Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
+ Float | Space |
+ (*delimited content*)
+ String | Alt_String | Verbatim | Cartouche | Comment |
+ (*special content*)
+ Error of string | Internal_Value | EOF;
val str_of_kind =
fn Command => "command"
| Keyword => "keyword"
| Ident => "identifier"
- | LongIdent => "long identifier"
- | SymIdent => "symbolic identifier"
+ | Long_Ident => "long identifier"
+ | Sym_Ident => "symbolic identifier"
| Var => "schematic variable"
- | TypeIdent => "type variable"
- | TypeVar => "schematic type variable"
+ | Type_Ident => "type variable"
+ | Type_Var => "schematic type variable"
| Nat => "natural number"
| Float => "floating-point number"
+ | Space => "white space"
| String => "quoted string"
- | AltString => "back-quoted string"
+ | Alt_String => "back-quoted string"
| Verbatim => "verbatim text"
| Cartouche => "text cartouche"
- | Space => "white space"
| Comment => "comment text"
- | InternalValue => "internal value"
+ | Internal_Value => "internal value"
| Error _ => "bad input"
| EOF => "end-of-input";
-val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
+val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
(* datatype token *)
@@ -219,7 +227,7 @@
fun is_kind k (Token (_, (k', _), _)) = k = k';
val is_command = is_kind Command;
-val is_name = is_kind Ident orf is_kind SymIdent orf is_kind String orf is_kind Nat;
+val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
| keyword_with _ _ = false;
@@ -279,25 +287,25 @@
local
val token_kind_markup =
- fn Command => (Markup.command, "")
- | Keyword => (Markup.keyword2, "")
- | Ident => (Markup.empty, "")
- | LongIdent => (Markup.empty, "")
- | SymIdent => (Markup.empty, "")
- | Var => (Markup.var, "")
- | TypeIdent => (Markup.tfree, "")
- | TypeVar => (Markup.tvar, "")
- | Nat => (Markup.empty, "")
- | Float => (Markup.empty, "")
- | String => (Markup.string, "")
- | AltString => (Markup.altstring, "")
- | Verbatim => (Markup.verbatim, "")
- | Cartouche => (Markup.cartouche, "")
- | Space => (Markup.empty, "")
- | Comment => (Markup.comment, "")
- | InternalValue => (Markup.empty, "")
- | Error msg => (Markup.bad, msg)
- | EOF => (Markup.empty, "");
+ fn Command => (Markup.command, "")
+ | Keyword => (Markup.keyword2, "")
+ | Ident => (Markup.empty, "")
+ | Long_Ident => (Markup.empty, "")
+ | Sym_Ident => (Markup.empty, "")
+ | Var => (Markup.var, "")
+ | Type_Ident => (Markup.tfree, "")
+ | Type_Var => (Markup.tvar, "")
+ | Nat => (Markup.empty, "")
+ | Float => (Markup.empty, "")
+ | Space => (Markup.empty, "")
+ | String => (Markup.string, "")
+ | Alt_String => (Markup.alt_string, "")
+ | Verbatim => (Markup.verbatim, "")
+ | Cartouche => (Markup.cartouche, "")
+ | Comment => (Markup.comment, "")
+ | Error msg => (Markup.bad, msg)
+ | Internal_Value => (Markup.empty, "")
+ | EOF => (Markup.empty, "");
in
@@ -326,7 +334,7 @@
fun unparse (Token (_, (kind, x), _)) =
(case kind of
String => Symbol_Pos.quote_string_qq x
- | AltString => Symbol_Pos.quote_string_bq x
+ | Alt_String => Symbol_Pos.quote_string_bq x
| Verbatim => enclose "{*" "*}" x
| Cartouche => cartouche x
| Comment => enclose "(*" "*)" x
@@ -366,7 +374,7 @@
(* access values *)
fun make_value name v =
- Token ((name, Position.no_range), (InternalValue, name), Value (SOME v));
+ Token ((name, Position.no_range), (Internal_Value, name), Value (SOME v));
fun get_value (Token (_, _, Value v)) = v
| get_value _ = NONE;
@@ -532,7 +540,7 @@
fun scan keywords = !!! "bad input"
(Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
- Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
+ Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
scan_verbatim >> token_range Verbatim ||
scan_cartouche >> token_range Cartouche ||
scan_comment >> token_range Comment ||
@@ -541,14 +549,14 @@
(Scan.max token_leq
(Scan.literal (Keyword.major_keywords keywords) >> pair Command)
(Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
- (Lexicon.scan_longid >> pair LongIdent ||
+ (Lexicon.scan_longid >> pair Long_Ident ||
Lexicon.scan_id >> pair Ident ||
Lexicon.scan_var >> pair Var ||
- Lexicon.scan_tid >> pair TypeIdent ||
- Lexicon.scan_tvar >> pair TypeVar ||
+ Lexicon.scan_tid >> pair Type_Ident ||
+ Lexicon.scan_tvar >> pair Type_Var ||
Lexicon.scan_float >> pair Float ||
Lexicon.scan_nat >> pair Nat ||
- scan_symid >> pair SymIdent) >> uncurry token));
+ scan_symid >> pair Sym_Ident) >> uncurry token));
fun recover msg =
(Symbol_Pos.recover_string_qq ||
--- a/src/Pure/Isar/token.scala Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/Isar/token.scala Wed Dec 03 11:37:51 2014 +0100
@@ -13,6 +13,7 @@
object Kind extends Enumeration
{
+ /*immediate source*/
val COMMAND = Value("command")
val KEYWORD = Value("keyword")
val IDENT = Value("identifier")
@@ -23,12 +24,14 @@
val TYPE_VAR = Value("schematic type variable")
val NAT = Value("natural number")
val FLOAT = Value("floating-point number")
+ val SPACE = Value("white space")
+ /*delimited content*/
val STRING = Value("string")
val ALT_STRING = Value("back-quoted string")
val VERBATIM = Value("verbatim text")
val CARTOUCHE = Value("text cartouche")
- val SPACE = Value("white space")
val COMMENT = Value("comment text")
+ /*special content*/
val ERROR = Value("bad input")
val UNPARSED = Value("unparsed input")
}
--- a/src/Pure/PIDE/markup.ML Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Dec 03 11:37:51 2014 +0100
@@ -115,7 +115,7 @@
val text_foldN: string val text_fold: T
val commandN: string val command: T
val stringN: string val string: T
- val altstringN: string val altstring: T
+ val alt_stringN: string val alt_string: T
val verbatimN: string val verbatim: T
val cartoucheN: string val cartouche: T
val commentN: string val comment: T
@@ -463,7 +463,7 @@
val (improperN, improper) = markup_elem "improper";
val (operatorN, operator) = markup_elem "operator";
val (stringN, string) = markup_elem "string";
-val (altstringN, altstring) = markup_elem "altstring";
+val (alt_stringN, alt_string) = markup_elem "alt_string";
val (verbatimN, verbatim) = markup_elem "verbatim";
val (cartoucheN, cartouche) = markup_elem "cartouche";
val (commentN, comment) = markup_elem "comment";
--- a/src/Pure/PIDE/markup.scala Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Dec 03 11:37:51 2014 +0100
@@ -261,7 +261,7 @@
val IMPROPER = "improper"
val OPERATOR = "operator"
val STRING = "string"
- val ALTSTRING = "altstring"
+ val ALT_STRING = "alt_string"
val VERBATIM = "verbatim"
val CARTOUCHE = "cartouche"
val COMMENT = "comment"
--- a/src/Pure/Thy/latex.ML Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Pure/Thy/latex.ML Wed Dec 03 11:37:51 2014 +0100
@@ -128,7 +128,7 @@
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
- else if Token.is_kind Token.AltString tok then
+ else if Token.is_kind Token.Alt_String tok then
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
--- a/src/Tools/jEdit/src/rendering.scala Tue Dec 02 17:30:53 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Wed Dec 03 11:37:51 2014 +0100
@@ -74,11 +74,11 @@
Token.Kind.TYPE_VAR -> NULL,
Token.Kind.NAT -> NULL,
Token.Kind.FLOAT -> NULL,
+ Token.Kind.SPACE -> NULL,
Token.Kind.STRING -> LITERAL1,
Token.Kind.ALT_STRING -> LITERAL2,
Token.Kind.VERBATIM -> COMMENT3,
Token.Kind.CARTOUCHE -> COMMENT4,
- Token.Kind.SPACE -> NULL,
Token.Kind.COMMENT -> COMMENT1,
Token.Kind.ERROR -> INVALID
).withDefaultValue(NULL)
@@ -132,7 +132,7 @@
Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
private val language_context_elements =
- Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
@@ -194,7 +194,7 @@
active_elements
private val foreground_elements =
- Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.ANTIQUOTED)
private val bullet_elements =
@@ -704,7 +704,7 @@
Markup.IMPROPER -> improper_color,
Markup.OPERATOR -> operator_color,
Markup.STRING -> Color.BLACK,
- Markup.ALTSTRING -> Color.BLACK,
+ Markup.ALT_STRING -> Color.BLACK,
Markup.VERBATIM -> Color.BLACK,
Markup.CARTOUCHE -> Color.BLACK,
Markup.LITERAL -> keyword1_color,