# HG changeset patch # User wenzelm # Date 1417603071 -3600 # Node ID 2ceb05ee0331232f4a7f7171d391dfbf24152d7b # Parent 611914621edbd7452801e0bc27d2b45da9719f1c clarified token kind; diff -r 611914621edb -r 2ceb05ee0331 src/Pure/Isar/parse.ML --- 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 diff -r 611914621edb -r 2ceb05ee0331 src/Pure/Isar/token.ML --- 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 || diff -r 611914621edb -r 2ceb05ee0331 src/Pure/Isar/token.scala --- 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") } diff -r 611914621edb -r 2ceb05ee0331 src/Pure/PIDE/markup.ML --- 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"; diff -r 611914621edb -r 2ceb05ee0331 src/Pure/PIDE/markup.scala --- 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" diff -r 611914621edb -r 2ceb05ee0331 src/Pure/Thy/latex.ML --- 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 diff -r 611914621edb -r 2ceb05ee0331 src/Tools/jEdit/src/rendering.scala --- 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,