src/Pure/Isar/token.ML
author wenzelm
Tue, 12 Jul 2011 14:33:08 +0200
changeset 43773 e8ba493027a3
parent 43731 70072780e095
child 43947 9b00f09f7721
permissions -rw-r--r--
more precise Symbol_Pos.quote_string;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
     1
(*  Title:      Pure/Isar/token.ML
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     3
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
     4
Outer token syntax for Isabelle/Isar.
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     5
*)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     6
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
     7
signature TOKEN =
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     8
sig
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
     9
  datatype kind =
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    10
    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
    11
    Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
40958
755f8fe7ced9 eliminated obsolete Token.Malformed -- subsumed by Token.Error;
wenzelm
parents: 40627
diff changeset
    12
    Error of string | Sync | EOF
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    13
  datatype value =
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    14
    Text of string | Typ of typ | Term of term | Fact of thm list |
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    15
    Attribute of morphism -> attribute
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    16
  type T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    17
  val str_of_kind: kind -> string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    18
  val position_of: T -> Position.T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    19
  val end_position_of: T -> Position.T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    20
  val pos_of: T -> string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    21
  val eof: T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    22
  val is_eof: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    23
  val not_eof: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    24
  val not_sync: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    25
  val stopper: T Scan.stopper
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    26
  val kind_of: T -> kind
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    27
  val is_kind: kind -> T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    28
  val keyword_with: (string -> bool) -> T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    29
  val ident_with: (string -> bool) -> T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    30
  val is_proper: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    31
  val is_semicolon: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    32
  val is_comment: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    33
  val is_begin_ignore: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    34
  val is_end_ignore: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    35
  val is_blank: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    36
  val is_newline: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    37
  val source_of: T -> string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    38
  val source_position_of: T -> Symbol_Pos.text * Position.T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    39
  val content_of: T -> string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    40
  val unparse: T -> string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    41
  val text_of: T -> string * string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    42
  val get_value: T -> value option
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    43
  val map_value: (value -> value) -> T -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    44
  val mk_text: string -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    45
  val mk_typ: typ -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    46
  val mk_term: term -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    47
  val mk_fact: thm list -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    48
  val mk_attribute: (morphism -> attribute) -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    49
  val assignable: T -> T
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    50
  val assign: value option -> T -> unit
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    51
  val closure: T -> T
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    52
  val ident_or_symbolic: string -> bool
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    53
  val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    54
  val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
27835
ff8b8513965a Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27814
diff changeset
    55
  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    56
    (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
27835
ff8b8513965a Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27814
diff changeset
    57
  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    58
    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    59
      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    60
  val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    61
end;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    62
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    63
structure Token: TOKEN =
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    64
struct
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    65
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    66
(** tokens **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    67
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    68
(* token values *)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    69
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    70
(*The value slot assigns an (optional) internal value to a token,
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    71
  usually as a side-effect of special scanner setup (see also
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    72
  args.ML).  Note that an assignable ref designates an intermediate
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    73
  state of internalization -- it is NOT meant to persist.*)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    74
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    75
datatype value =
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    76
  Text of string |
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    77
  Typ of typ |
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    78
  Term of term |
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    79
  Fact of thm list |
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    80
  Attribute of morphism -> attribute;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    81
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    82
datatype slot =
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    83
  Slot |
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    84
  Value of value option |
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30586
diff changeset
    85
  Assignable of value option Unsynchronized.ref;
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    86
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    87
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    88
(* datatype token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    89
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    90
datatype kind =
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    91
  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
    92
  Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
40958
755f8fe7ced9 eliminated obsolete Token.Malformed -- subsumed by Token.Error;
wenzelm
parents: 40627
diff changeset
    93
  Error of string | Sync | EOF;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    94
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    95
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    96
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    97
val str_of_kind =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    98
 fn Command => "command"
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    99
  | Keyword => "keyword"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   100
  | Ident => "identifier"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   101
  | LongIdent => "long identifier"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   102
  | SymIdent => "symbolic identifier"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   103
  | Var => "schematic variable"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   104
  | TypeIdent => "type variable"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   105
  | TypeVar => "schematic type variable"
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
   106
  | Nat => "natural number"
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
   107
  | Float => "floating-point number"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   108
  | String => "string"
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   109
  | AltString => "back-quoted string"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   110
  | Verbatim => "verbatim text"
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   111
  | Space => "white space"
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   112
  | Comment => "comment text"
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   113
  | InternalValue => "internal value"
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   114
  | Error _ => "bad input"
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   115
  | Sync => "sync marker"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   116
  | EOF => "end-of-file";
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   117
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   118
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   119
(* position *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   120
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   121
fun position_of (Token ((_, (pos, _)), _, _)) = pos;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   122
fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
27663
098798321622 maintain token range;
wenzelm
parents: 27358
diff changeset
   123
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   124
val pos_of = Position.str_of o position_of;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   125
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   126
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   127
(* control tokens *)
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   128
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   129
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   130
val eof = mk_eof Position.none;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   131
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   132
fun is_eof (Token (_, (EOF, _), _)) = true
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   133
  | is_eof _ = false;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   134
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   135
val not_eof = not o is_eof;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   136
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   137
fun not_sync (Token (_, (Sync, _), _)) = false
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   138
  | not_sync _ = true;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   139
27752
ea7d573e565f removed obsolete range_of (already included in position);
wenzelm
parents: 27747
diff changeset
   140
val stopper =
ea7d573e565f removed obsolete range_of (already included in position);
wenzelm
parents: 27747
diff changeset
   141
  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   142
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   143
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   144
(* kind of token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   145
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   146
fun kind_of (Token (_, (k, _), _)) = k;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   147
fun is_kind k (Token (_, (k', _), _)) = k = k';
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   148
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   149
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   150
  | keyword_with _ _ = false;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   151
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   152
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
16029
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   153
  | ident_with _ _ = false;
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   154
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   155
fun is_proper (Token (_, (Space, _), _)) = false
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   156
  | is_proper (Token (_, (Comment, _), _)) = false
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   157
  | is_proper _ = true;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   158
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   159
fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   160
  | is_semicolon _ = false;
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   161
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   162
fun is_comment (Token (_, (Comment, _), _)) = true
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   163
  | is_comment _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   164
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   165
fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   166
  | is_begin_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   167
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   168
fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   169
  | is_end_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   170
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   171
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   172
(* blanks and newlines -- space tokens obey lines *)
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   173
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   174
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   175
  | is_blank _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   176
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   177
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   178
  | is_newline _ = false;
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   179
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   180
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   181
(* token content *)
9155
adfa40218e06 OuterLex.name_of: include val;
wenzelm
parents: 9130
diff changeset
   182
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43709
diff changeset
   183
fun source_of (Token ((source, (pos, _)), (_, x), _)) =
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43709
diff changeset
   184
  if YXML.detect x then x
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43709
diff changeset
   185
  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
25642
ebdff0dca2a5 text_of: made even more robust against recurrent errors;
wenzelm
parents: 25582
diff changeset
   186
27885
76b51cd0a37c renamed T.source_of' to T.source_position_of;
wenzelm
parents: 27873
diff changeset
   187
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
27873
34d61938e27a added source_of';
wenzelm
parents: 27856
diff changeset
   188
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   189
fun content_of (Token (_, (_, x), _)) = x;
27747
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   190
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   191
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   192
(* unparse *)
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   193
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   194
fun unparse (Token (_, (kind, x), _)) =
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   195
  (case kind of
43773
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   196
    String => Symbol_Pos.quote_string_qq x
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   197
  | AltString => Symbol_Pos.quote_string_bq x
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   198
  | Verbatim => enclose "{*" "*}" x
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   199
  | Comment => enclose "(*" "*)" x
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   200
  | Sync => ""
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   201
  | EOF => ""
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   202
  | _ => x);
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   203
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   204
fun text_of tok =
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   205
  if is_semicolon tok then ("terminator", "")
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   206
  else
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   207
    let
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   208
      val k = str_of_kind (kind_of tok);
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 40290
diff changeset
   209
      val s = unparse tok;
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   210
    in
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   211
      if s = "" then (k, "")
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   212
      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   213
      else (k, s)
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   214
    end;
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   215
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   216
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   217
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   218
(** associated values **)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   219
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   220
(* access values *)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   221
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   222
fun get_value (Token (_, _, Value v)) = v
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   223
  | get_value _ = NONE;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   224
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   225
fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   226
  | map_value _ tok = tok;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   227
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   228
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   229
(* make values *)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   230
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   231
fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   232
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   233
val mk_text = mk_value "<text>" o Text;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   234
val mk_typ = mk_value "<typ>" o Typ;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   235
val mk_term = mk_value "<term>" o Term;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   236
val mk_fact = mk_value "<fact>" o Fact;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   237
val mk_attribute = mk_value "<attribute>" o Attribute;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   238
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   239
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   240
(* static binding *)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   241
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   242
(*1st stage: make empty slots assignable*)
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30586
diff changeset
   243
fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   244
  | assignable tok = tok;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   245
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   246
(*2nd stage: assign values as side-effect of scanning*)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   247
fun assign v (Token (_, _, Assignable r)) = r := v
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   248
  | assign _ _ = ();
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   249
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   250
(*3rd stage: static closure of final values*)
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30586
diff changeset
   251
fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   252
  | closure tok = tok;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   253
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   254
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   255
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   256
(** scanners **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   257
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   258
open Basic_Symbol_Pos;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   259
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   260
fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   261
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   262
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   263
(* scan symbolic idents *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   264
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 40531
diff changeset
   265
val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   266
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   267
val scan_symid =
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   268
  Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   269
  Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   270
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   271
fun is_symid str =
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   272
  (case try Symbol.explode str of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15224
diff changeset
   273
    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15224
diff changeset
   274
  | SOME ss => forall is_sym_char ss
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   275
  | _ => false);
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   276
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   277
fun ident_or_symbolic "begin" = false
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   278
  | ident_or_symbolic ":" = true
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   279
  | ident_or_symbolic "::" = true
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   280
  | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   281
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   282
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   283
(* scan verbatim text *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   284
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   285
val scan_verb =
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   286
  $$$ "*" --| Scan.ahead (~$$$ "}") ||
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   287
  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   288
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   289
val scan_verbatim =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   290
  (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
30586
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   291
    (Symbol_Pos.change_prompt
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   292
      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   293
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   294
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   295
(* scan space *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   296
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 18547
diff changeset
   297
fun is_space s = Symbol.is_blank s andalso s <> "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   298
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   299
val scan_space =
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   300
  Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   301
  Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   302
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   303
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   304
(* scan comment *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   305
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   306
val scan_comment =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   307
  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   308
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   309
27663
098798321622 maintain token range;
wenzelm
parents: 27358
diff changeset
   310
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   311
(** token sources **)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   312
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   313
fun source_proper src = src |> Source.filter is_proper;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   314
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   315
local
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   316
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   317
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   318
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   319
fun token k ss =
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 42503
diff changeset
   320
  Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   321
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   322
fun token_range k (pos1, (ss, pos2)) =
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 42503
diff changeset
   323
  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   324
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   325
fun scan (lex1, lex2) = !!! "bad input"
42503
27514b6fbe93 more uniform variations of scan_string;
wenzelm
parents: 42290
diff changeset
   326
  (Symbol_Pos.scan_string_qq >> token_range String ||
27514b6fbe93 more uniform variations of scan_string;
wenzelm
parents: 42290
diff changeset
   327
    Symbol_Pos.scan_string_bq >> token_range AltString ||
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   328
    scan_verbatim >> token_range Verbatim ||
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   329
    scan_comment >> token_range Comment ||
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   330
    scan_space >> token Space ||
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   331
    Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   332
    (Scan.max token_leq
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   333
      (Scan.max token_leq
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   334
        (Scan.literal lex2 >> pair Command)
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   335
        (Scan.literal lex1 >> pair Keyword))
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   336
      (Lexicon.scan_longid >> pair LongIdent ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   337
        Lexicon.scan_id >> pair Ident ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   338
        Lexicon.scan_var >> pair Var ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   339
        Lexicon.scan_tid >> pair TypeIdent ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   340
        Lexicon.scan_tvar >> pair TypeVar ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   341
        Lexicon.scan_float >> pair Float ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   342
        Lexicon.scan_nat >> pair Nat ||
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   343
        scan_symid >> pair SymIdent) >> uncurry token));
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   344
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   345
fun recover msg =
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   346
  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o Symbol_Pos.symbol)
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   347
  >> (single o token (Error msg));
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   348
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   349
in
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   350
27835
ff8b8513965a Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27814
diff changeset
   351
fun source' {do_recover} get_lex =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   352
  Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   353
    (Option.map (rpair recover) do_recover);
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   354
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   355
fun source do_recover get_lex pos src =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   356
  Symbol_Pos.source pos src
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   357
  |> source' do_recover get_lex;
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   358
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   359
end;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   360
30586
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   361
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   362
(* read_antiq *)
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   363
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   364
fun read_antiq lex scan (syms, pos) =
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   365
  let
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   366
    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   367
      "@{" ^ Symbol_Pos.content syms ^ "}");
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   368
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   369
    val res =
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   370
      Source.of_list syms
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   371
      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   372
      |> source_proper
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   373
      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   374
      |> Source.exhaust;
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   375
  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   376
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   377
end;