clarified token kind;
authorwenzelm
Wed Dec 03 11:37:51 2014 +0100 (2014-12-03)
changeset 590812ceb05ee0331
parent 59080 611914621edb
child 59082 25501ba956ac
clarified token kind;
src/Pure/Isar/parse.ML
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/latex.ML
src/Tools/jEdit/src/rendering.scala
     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,