1.1 --- a/src/Pure/Isar/parse.ML Tue Dec 02 17:30:53 2014 +0100
1.2 +++ b/src/Pure/Isar/parse.ML Wed Dec 03 11:37:51 2014 +0100
1.3 @@ -185,15 +185,15 @@
1.4 val command_ = kind Token.Command;
1.5 val keyword = kind Token.Keyword;
1.6 val short_ident = kind Token.Ident;
1.7 -val long_ident = kind Token.LongIdent;
1.8 -val sym_ident = kind Token.SymIdent;
1.9 +val long_ident = kind Token.Long_Ident;
1.10 +val sym_ident = kind Token.Sym_Ident;
1.11 val term_var = kind Token.Var;
1.12 -val type_ident = kind Token.TypeIdent;
1.13 -val type_var = kind Token.TypeVar;
1.14 +val type_ident = kind Token.Type_Ident;
1.15 +val type_var = kind Token.Type_Var;
1.16 val number = kind Token.Nat;
1.17 val float_number = kind Token.Float;
1.18 val string = kind Token.String;
1.19 -val alt_string = kind Token.AltString;
1.20 +val alt_string = kind Token.Alt_String;
1.21 val verbatim = kind Token.Verbatim;
1.22 val cartouche = kind Token.Cartouche;
1.23 val eof = kind Token.EOF;
1.24 @@ -405,8 +405,8 @@
1.25 local
1.26
1.27 val argument_kinds =
1.28 - [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar,
1.29 - Token.Nat, Token.Float, Token.String, Token.AltString, Token.Cartouche, Token.Verbatim];
1.30 + [Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var,
1.31 + Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim];
1.32
1.33 fun arguments is_symid =
1.34 let
2.1 --- a/src/Pure/Isar/token.ML Tue Dec 02 17:30:53 2014 +0100
2.2 +++ b/src/Pure/Isar/token.ML Wed Dec 03 11:37:51 2014 +0100
2.3 @@ -7,9 +7,13 @@
2.4 signature TOKEN =
2.5 sig
2.6 datatype kind =
2.7 - Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
2.8 - Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
2.9 - Error of string | EOF
2.10 + (*immediate source*)
2.11 + Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
2.12 + Float | Space |
2.13 + (*delimited content*)
2.14 + String | Alt_String | Verbatim | Cartouche | Comment |
2.15 + (*special content*)
2.16 + Error of string | Internal_Value | EOF
2.17 val str_of_kind: kind -> string
2.18 type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
2.19 type T
2.20 @@ -101,32 +105,36 @@
2.21 (* token kind *)
2.22
2.23 datatype kind =
2.24 - Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
2.25 - Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
2.26 - Error of string | EOF;
2.27 + (*immediate source*)
2.28 + Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
2.29 + Float | Space |
2.30 + (*delimited content*)
2.31 + String | Alt_String | Verbatim | Cartouche | Comment |
2.32 + (*special content*)
2.33 + Error of string | Internal_Value | EOF;
2.34
2.35 val str_of_kind =
2.36 fn Command => "command"
2.37 | Keyword => "keyword"
2.38 | Ident => "identifier"
2.39 - | LongIdent => "long identifier"
2.40 - | SymIdent => "symbolic identifier"
2.41 + | Long_Ident => "long identifier"
2.42 + | Sym_Ident => "symbolic identifier"
2.43 | Var => "schematic variable"
2.44 - | TypeIdent => "type variable"
2.45 - | TypeVar => "schematic type variable"
2.46 + | Type_Ident => "type variable"
2.47 + | Type_Var => "schematic type variable"
2.48 | Nat => "natural number"
2.49 | Float => "floating-point number"
2.50 + | Space => "white space"
2.51 | String => "quoted string"
2.52 - | AltString => "back-quoted string"
2.53 + | Alt_String => "back-quoted string"
2.54 | Verbatim => "verbatim text"
2.55 | Cartouche => "text cartouche"
2.56 - | Space => "white space"
2.57 | Comment => "comment text"
2.58 - | InternalValue => "internal value"
2.59 + | Internal_Value => "internal value"
2.60 | Error _ => "bad input"
2.61 | EOF => "end-of-input";
2.62
2.63 -val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
2.64 +val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
2.65
2.66
2.67 (* datatype token *)
2.68 @@ -219,7 +227,7 @@
2.69 fun is_kind k (Token (_, (k', _), _)) = k = k';
2.70
2.71 val is_command = is_kind Command;
2.72 -val is_name = is_kind Ident orf is_kind SymIdent orf is_kind String orf is_kind Nat;
2.73 +val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
2.74
2.75 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
2.76 | keyword_with _ _ = false;
2.77 @@ -279,25 +287,25 @@
2.78 local
2.79
2.80 val token_kind_markup =
2.81 - fn Command => (Markup.command, "")
2.82 - | Keyword => (Markup.keyword2, "")
2.83 - | Ident => (Markup.empty, "")
2.84 - | LongIdent => (Markup.empty, "")
2.85 - | SymIdent => (Markup.empty, "")
2.86 - | Var => (Markup.var, "")
2.87 - | TypeIdent => (Markup.tfree, "")
2.88 - | TypeVar => (Markup.tvar, "")
2.89 - | Nat => (Markup.empty, "")
2.90 - | Float => (Markup.empty, "")
2.91 - | String => (Markup.string, "")
2.92 - | AltString => (Markup.altstring, "")
2.93 - | Verbatim => (Markup.verbatim, "")
2.94 - | Cartouche => (Markup.cartouche, "")
2.95 - | Space => (Markup.empty, "")
2.96 - | Comment => (Markup.comment, "")
2.97 - | InternalValue => (Markup.empty, "")
2.98 - | Error msg => (Markup.bad, msg)
2.99 - | EOF => (Markup.empty, "");
2.100 + fn Command => (Markup.command, "")
2.101 + | Keyword => (Markup.keyword2, "")
2.102 + | Ident => (Markup.empty, "")
2.103 + | Long_Ident => (Markup.empty, "")
2.104 + | Sym_Ident => (Markup.empty, "")
2.105 + | Var => (Markup.var, "")
2.106 + | Type_Ident => (Markup.tfree, "")
2.107 + | Type_Var => (Markup.tvar, "")
2.108 + | Nat => (Markup.empty, "")
2.109 + | Float => (Markup.empty, "")
2.110 + | Space => (Markup.empty, "")
2.111 + | String => (Markup.string, "")
2.112 + | Alt_String => (Markup.alt_string, "")
2.113 + | Verbatim => (Markup.verbatim, "")
2.114 + | Cartouche => (Markup.cartouche, "")
2.115 + | Comment => (Markup.comment, "")
2.116 + | Error msg => (Markup.bad, msg)
2.117 + | Internal_Value => (Markup.empty, "")
2.118 + | EOF => (Markup.empty, "");
2.119
2.120 in
2.121
2.122 @@ -326,7 +334,7 @@
2.123 fun unparse (Token (_, (kind, x), _)) =
2.124 (case kind of
2.125 String => Symbol_Pos.quote_string_qq x
2.126 - | AltString => Symbol_Pos.quote_string_bq x
2.127 + | Alt_String => Symbol_Pos.quote_string_bq x
2.128 | Verbatim => enclose "{*" "*}" x
2.129 | Cartouche => cartouche x
2.130 | Comment => enclose "(*" "*)" x
2.131 @@ -366,7 +374,7 @@
2.132 (* access values *)
2.133
2.134 fun make_value name v =
2.135 - Token ((name, Position.no_range), (InternalValue, name), Value (SOME v));
2.136 + Token ((name, Position.no_range), (Internal_Value, name), Value (SOME v));
2.137
2.138 fun get_value (Token (_, _, Value v)) = v
2.139 | get_value _ = NONE;
2.140 @@ -532,7 +540,7 @@
2.141
2.142 fun scan keywords = !!! "bad input"
2.143 (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
2.144 - Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
2.145 + Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
2.146 scan_verbatim >> token_range Verbatim ||
2.147 scan_cartouche >> token_range Cartouche ||
2.148 scan_comment >> token_range Comment ||
2.149 @@ -541,14 +549,14 @@
2.150 (Scan.max token_leq
2.151 (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
2.152 (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
2.153 - (Lexicon.scan_longid >> pair LongIdent ||
2.154 + (Lexicon.scan_longid >> pair Long_Ident ||
2.155 Lexicon.scan_id >> pair Ident ||
2.156 Lexicon.scan_var >> pair Var ||
2.157 - Lexicon.scan_tid >> pair TypeIdent ||
2.158 - Lexicon.scan_tvar >> pair TypeVar ||
2.159 + Lexicon.scan_tid >> pair Type_Ident ||
2.160 + Lexicon.scan_tvar >> pair Type_Var ||
2.161 Lexicon.scan_float >> pair Float ||
2.162 Lexicon.scan_nat >> pair Nat ||
2.163 - scan_symid >> pair SymIdent) >> uncurry token));
2.164 + scan_symid >> pair Sym_Ident) >> uncurry token));
2.165
2.166 fun recover msg =
2.167 (Symbol_Pos.recover_string_qq ||
3.1 --- a/src/Pure/Isar/token.scala Tue Dec 02 17:30:53 2014 +0100
3.2 +++ b/src/Pure/Isar/token.scala Wed Dec 03 11:37:51 2014 +0100
3.3 @@ -13,6 +13,7 @@
3.4
3.5 object Kind extends Enumeration
3.6 {
3.7 + /*immediate source*/
3.8 val COMMAND = Value("command")
3.9 val KEYWORD = Value("keyword")
3.10 val IDENT = Value("identifier")
3.11 @@ -23,12 +24,14 @@
3.12 val TYPE_VAR = Value("schematic type variable")
3.13 val NAT = Value("natural number")
3.14 val FLOAT = Value("floating-point number")
3.15 + val SPACE = Value("white space")
3.16 + /*delimited content*/
3.17 val STRING = Value("string")
3.18 val ALT_STRING = Value("back-quoted string")
3.19 val VERBATIM = Value("verbatim text")
3.20 val CARTOUCHE = Value("text cartouche")
3.21 - val SPACE = Value("white space")
3.22 val COMMENT = Value("comment text")
3.23 + /*special content*/
3.24 val ERROR = Value("bad input")
3.25 val UNPARSED = Value("unparsed input")
3.26 }
4.1 --- a/src/Pure/PIDE/markup.ML Tue Dec 02 17:30:53 2014 +0100
4.2 +++ b/src/Pure/PIDE/markup.ML Wed Dec 03 11:37:51 2014 +0100
4.3 @@ -115,7 +115,7 @@
4.4 val text_foldN: string val text_fold: T
4.5 val commandN: string val command: T
4.6 val stringN: string val string: T
4.7 - val altstringN: string val altstring: T
4.8 + val alt_stringN: string val alt_string: T
4.9 val verbatimN: string val verbatim: T
4.10 val cartoucheN: string val cartouche: T
4.11 val commentN: string val comment: T
4.12 @@ -463,7 +463,7 @@
4.13 val (improperN, improper) = markup_elem "improper";
4.14 val (operatorN, operator) = markup_elem "operator";
4.15 val (stringN, string) = markup_elem "string";
4.16 -val (altstringN, altstring) = markup_elem "altstring";
4.17 +val (alt_stringN, alt_string) = markup_elem "alt_string";
4.18 val (verbatimN, verbatim) = markup_elem "verbatim";
4.19 val (cartoucheN, cartouche) = markup_elem "cartouche";
4.20 val (commentN, comment) = markup_elem "comment";
5.1 --- a/src/Pure/PIDE/markup.scala Tue Dec 02 17:30:53 2014 +0100
5.2 +++ b/src/Pure/PIDE/markup.scala Wed Dec 03 11:37:51 2014 +0100
5.3 @@ -261,7 +261,7 @@
5.4 val IMPROPER = "improper"
5.5 val OPERATOR = "operator"
5.6 val STRING = "string"
5.7 - val ALTSTRING = "altstring"
5.8 + val ALT_STRING = "alt_string"
5.9 val VERBATIM = "verbatim"
5.10 val CARTOUCHE = "cartouche"
5.11 val COMMENT = "comment"
6.1 --- a/src/Pure/Thy/latex.ML Tue Dec 02 17:30:53 2014 +0100
6.2 +++ b/src/Pure/Thy/latex.ML Wed Dec 03 11:37:51 2014 +0100
6.3 @@ -128,7 +128,7 @@
6.4 "\\isakeyword{" ^ output_syms s ^ "}"
6.5 else if Token.is_kind Token.String tok then
6.6 enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
6.7 - else if Token.is_kind Token.AltString tok then
6.8 + else if Token.is_kind Token.Alt_String tok then
6.9 enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
6.10 else if Token.is_kind Token.Verbatim tok then
6.11 let
7.1 --- a/src/Tools/jEdit/src/rendering.scala Tue Dec 02 17:30:53 2014 +0100
7.2 +++ b/src/Tools/jEdit/src/rendering.scala Wed Dec 03 11:37:51 2014 +0100
7.3 @@ -74,11 +74,11 @@
7.4 Token.Kind.TYPE_VAR -> NULL,
7.5 Token.Kind.NAT -> NULL,
7.6 Token.Kind.FLOAT -> NULL,
7.7 + Token.Kind.SPACE -> NULL,
7.8 Token.Kind.STRING -> LITERAL1,
7.9 Token.Kind.ALT_STRING -> LITERAL2,
7.10 Token.Kind.VERBATIM -> COMMENT3,
7.11 Token.Kind.CARTOUCHE -> COMMENT4,
7.12 - Token.Kind.SPACE -> NULL,
7.13 Token.Kind.COMMENT -> COMMENT1,
7.14 Token.Kind.ERROR -> INVALID
7.15 ).withDefaultValue(NULL)
7.16 @@ -132,7 +132,7 @@
7.17 Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
7.18
7.19 private val language_context_elements =
7.20 - Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
7.21 + Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
7.22 Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
7.23 Markup.ML_STRING, Markup.ML_COMMENT)
7.24
7.25 @@ -194,7 +194,7 @@
7.26 active_elements
7.27
7.28 private val foreground_elements =
7.29 - Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
7.30 + Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
7.31 Markup.CARTOUCHE, Markup.ANTIQUOTED)
7.32
7.33 private val bullet_elements =
7.34 @@ -704,7 +704,7 @@
7.35 Markup.IMPROPER -> improper_color,
7.36 Markup.OPERATOR -> operator_color,
7.37 Markup.STRING -> Color.BLACK,
7.38 - Markup.ALTSTRING -> Color.BLACK,
7.39 + Markup.ALT_STRING -> Color.BLACK,
7.40 Markup.VERBATIM -> Color.BLACK,
7.41 Markup.CARTOUCHE -> Color.BLACK,
7.42 Markup.LITERAL -> keyword1_color,