src/Pure/Isar/token.ML
author wenzelm
Thu, 02 Apr 2015 20:07:32 +0200
changeset 59913 a7f6359665c6
parent 59908 fdf6957f8635
child 59924 801b979ec0c2
permissions -rw-r--r--
tuned signature;
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 =
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    10
    (*immediate source*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    11
    Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    12
    Float | Space |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    13
    (*delimited content*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    14
    String | Alt_String | Verbatim | Cartouche | Comment |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    15
    (*special content*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    16
    Error of string | Internal_Value | EOF
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    17
  val str_of_kind: kind -> string
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55750
diff changeset
    18
  type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    19
  type T
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    20
  type src
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    21
  datatype value =
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    22
    Source of src |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    23
    Literal of bool * Markup.T |
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    24
    Name of string * morphism |
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    25
    Typ of typ |
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    26
    Term of term |
57942
e5bec882fdd0 more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents: 56202
diff changeset
    27
    Fact of string option * thm list |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    28
    Attribute of morphism -> attribute |
58017
5bdb58845eab support for declaration within token source;
wenzelm
parents: 58012
diff changeset
    29
    Declaration of declaration |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    30
    Files of file Exn.result list
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    31
  val name0: string -> value
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
    32
  val pos_of: T -> Position.T
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
    33
  val range_of: T list -> Position.range
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    34
  val src: xstring * Position.T -> T list -> src
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
    35
  val src_checked: string * Position.T -> T list -> string * Markup.T -> src
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    36
  val name_of_src: src -> string * Position.T
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    37
  val args_of_src: src -> T list
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    38
  val range_of_src: src -> Position.T
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    39
  val check_src: Proof.context -> 'a Name_Space.table -> src -> src * '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
    40
  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
    41
  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
    42
  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
    43
  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
    44
  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
    45
  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
    46
  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
    47
  val ident_with: (string -> bool) -> T -> bool
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 45666
diff changeset
    48
  val is_command: T -> bool
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
    49
  val is_name: T -> bool
36959
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 is_proper: T -> bool
51266
3007d0bc9cb1 unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents: 50239
diff changeset
    51
  val is_improper: T -> bool
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    52
  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
    53
  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
    54
  val is_end_ignore: T -> bool
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48743
diff changeset
    55
  val is_error: T -> bool
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
    56
  val is_space: T -> bool
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    57
  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
    58
  val is_newline: T -> bool
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
    59
  val content_of: T -> string
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59795
diff changeset
    60
  val input_of: T -> Input.source
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
    61
  val inner_syntax_of: T -> string
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56064
diff changeset
    62
  val keyword_markup: bool * Markup.T -> string -> Markup.T
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
    63
  val completion_report: T -> Position.report_text list
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
    64
  val reports: Keyword.keywords -> T -> Position.report_text list
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
    65
  val markups: Keyword.keywords -> T -> Markup.T list
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    66
  val unparse: T -> string
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    67
  val unparse_src: src -> string list
55745
b865c3035d5c tuned message -- more markup;
wenzelm
parents: 55744
diff changeset
    68
  val print: T -> string
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    69
  val text_of: T -> string * string
54520
cee77d2e9582 release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents: 54519
diff changeset
    70
  val get_files: T -> file Exn.result list
cee77d2e9582 release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents: 54519
diff changeset
    71
  val put_files: file Exn.result list -> T -> T
58025
wenzelm
parents: 58017
diff changeset
    72
  val make_value: string -> value -> T
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    73
  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
    74
  val map_value: (value -> value) -> T -> T
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
    75
  val reports_of_value: T -> Position.report list
59908
fdf6957f8635 operation on embedded sources for Eisbach;
wenzelm
parents: 59906
diff changeset
    76
  val map_values: (value -> value) -> src -> src
59646
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
    77
  val declare_maxidx: T -> Proof.context -> Proof.context
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
    78
  val declare_maxidx_src: src -> Proof.context -> Proof.context
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    79
  val transform: morphism -> T -> T
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    80
  val transform_src: morphism -> src -> src
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
    81
  val init_assignable: T -> T
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    82
  val init_assignable_src: src -> src
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    83
  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
    84
  val closure: T -> T
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    85
  val closure_src: src -> src
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    86
  val pretty_value: Proof.context -> T -> Pretty.T
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    87
  val pretty_src: Proof.context -> src -> Pretty.T
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    88
  val ident_or_symbolic: string -> bool
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    89
  val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
    90
  val source: Keyword.keywords ->
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
    91
    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
    92
      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
    93
  val source_strict: Keyword.keywords ->
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    94
    Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    95
      (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
    96
  val explode: Keyword.keywords -> Position.T -> string -> T list
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
    97
  val make: (int * int) * string -> Position.T -> T * Position.T
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    98
  type 'a parser = T list -> 'a * T list
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    99
  type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   100
  val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   101
  val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   102
  val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   103
  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   104
end;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   105
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
   106
structure Token: TOKEN =
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   107
struct
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   108
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   109
(** tokens **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   110
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   111
(* token kind *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   112
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
   113
datatype kind =
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   114
  (*immediate source*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   115
  Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   116
  Float | Space |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   117
  (*delimited content*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   118
  String | Alt_String | Verbatim | Cartouche | Comment |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   119
  (*special content*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   120
  Error of string | Internal_Value | EOF;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   121
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   122
val str_of_kind =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   123
 fn Command => "command"
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   124
  | Keyword => "keyword"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   125
  | Ident => "identifier"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   126
  | Long_Ident => "long identifier"
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   127
  | Sym_Ident => "symbolic identifier"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   128
  | Var => "schematic variable"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   129
  | Type_Ident => "type variable"
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   130
  | Type_Var => "schematic type variable"
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
   131
  | Nat => "natural number"
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
   132
  | Float => "floating-point number"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   133
  | Space => "white space"
55103
57d87ec3da4c tuned errors;
wenzelm
parents: 55033
diff changeset
   134
  | String => "quoted string"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   135
  | Alt_String => "back-quoted string"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   136
  | Verbatim => "verbatim text"
55103
57d87ec3da4c tuned errors;
wenzelm
parents: 55033
diff changeset
   137
  | Cartouche => "text cartouche"
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   138
  | Comment => "comment text"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   139
  | Internal_Value => "internal value"
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   140
  | Error _ => "bad input"
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48905
diff changeset
   141
  | EOF => "end-of-input";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   142
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   143
val immediate_kinds =
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   144
  Vector.fromList
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   145
    [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   146
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   147
val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55788
diff changeset
   148
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   149
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   150
(* datatype token *)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   151
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   152
(*The value slot assigns an (optional) internal value to a token,
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   153
  usually as a side-effect of special scanner setup (see also
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   154
  args.ML).  Note that an assignable ref designates an intermediate
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   155
  state of internalization -- it is NOT meant to persist.*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   156
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   157
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   158
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   159
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   160
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   161
and src =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   162
  Src of
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   163
   {name: string * Position.T,
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   164
    args: T list,
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   165
    checked: (string * Markup.T) option}
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   166
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   167
and slot =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   168
  Slot |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   169
  Value of value option |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   170
  Assignable of value option Unsynchronized.ref
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   171
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   172
and value =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   173
  Source of src |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   174
  Literal of bool * Markup.T |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   175
  Name of string * morphism |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   176
  Typ of typ |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   177
  Term of term |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   178
  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   179
  Attribute of morphism -> attribute |
58017
5bdb58845eab support for declaration within token source;
wenzelm
parents: 58012
diff changeset
   180
  Declaration of declaration |
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   181
  Files of file Exn.result list;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   182
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   183
fun name0 a = Name (a, Morphism.identity);
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   184
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   185
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   186
(* position *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   187
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   188
fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   189
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
27663
098798321622 maintain token range;
wenzelm
parents: 27358
diff changeset
   190
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   191
fun range_of (toks as tok :: _) =
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   192
      let val pos' = end_pos_of (List.last toks)
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   193
      in Position.range (pos_of tok) pos' end
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   194
  | range_of [] = Position.no_range;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   195
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   196
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   197
(* src *)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   198
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   199
fun src name args = Src {name = name, args = args, checked = NONE};
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   200
fun src_checked name args checked = Src {name = name, args = args, checked = SOME checked};
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   201
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   202
fun map_args f (Src {name, args, checked}) =
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   203
  Src {name = name, args = map f args, checked = checked};
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   204
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   205
fun name_of_src (Src {name, ...}) = name;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   206
fun args_of_src (Src {args, ...}) = args;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   207
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   208
fun range_of_src (Src {name = (_, pos), args, ...}) =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   209
  if null args then pos
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   210
  else Position.set_range (pos, #2 (range_of args));
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   211
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   212
fun check_src _ table (src as Src {name = (name, _), checked = SOME _, ...}) =
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59646
diff changeset
   213
      (src, Name_Space.get table name)
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   214
  | check_src ctxt table (Src {name = (xname, pos), args, checked = NONE}) =
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59646
diff changeset
   215
      let
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59646
diff changeset
   216
        val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59646
diff changeset
   217
        val space = Name_Space.space_of_table table;
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59646
diff changeset
   218
        val kind = Name_Space.kind_of space;
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59646
diff changeset
   219
        val markup = Name_Space.markup space name;
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   220
      in (src_checked (name, pos) args (kind, markup), x) end;
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   221
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   222
58855
2885e2eaa0fb removed pointless markup;
wenzelm
parents: 58854
diff changeset
   223
(* stopper *)
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   224
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   225
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
   226
val eof = mk_eof Position.none;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   227
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   228
fun is_eof (Token (_, (EOF, _), _)) = true
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   229
  | is_eof _ = false;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   230
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   231
val not_eof = not o is_eof;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   232
27752
ea7d573e565f removed obsolete range_of (already included in position);
wenzelm
parents: 27747
diff changeset
   233
val stopper =
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   234
  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   235
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   236
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   237
(* kind of token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   238
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   239
fun kind_of (Token (_, (k, _), _)) = k;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   240
fun is_kind k (Token (_, (k', _), _)) = k = k';
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   241
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 45666
diff changeset
   242
val is_command = is_kind Command;
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   243
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   244
val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 45666
diff changeset
   245
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   246
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   247
  | keyword_with _ _ = false;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   248
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   249
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
16029
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   250
  | ident_with _ _ = false;
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   251
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   252
fun is_proper (Token (_, (Space, _), _)) = false
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   253
  | is_proper (Token (_, (Comment, _), _)) = false
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   254
  | is_proper _ = true;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   255
51266
3007d0bc9cb1 unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents: 50239
diff changeset
   256
val is_improper = not o is_proper;
3007d0bc9cb1 unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents: 50239
diff changeset
   257
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   258
fun is_comment (Token (_, (Comment, _), _)) = true
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   259
  | is_comment _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   260
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   261
fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   262
  | is_begin_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   263
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   264
fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   265
  | is_end_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   266
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48743
diff changeset
   267
fun is_error (Token (_, (Error _, _), _)) = true
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48743
diff changeset
   268
  | is_error _ = false;
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48743
diff changeset
   269
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   270
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   271
(* blanks and newlines -- space tokens obey lines *)
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   272
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
   273
fun is_space (Token (_, (Space, _), _)) = true
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
   274
  | is_space _ = false;
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
   275
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   276
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   277
  | is_blank _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   278
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   279
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   280
  | is_newline _ = false;
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   281
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   282
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   283
(* token content *)
9155
adfa40218e06 OuterLex.name_of: include val;
wenzelm
parents: 9130
diff changeset
   284
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
   285
fun content_of (Token (_, (_, x), _)) = x;
25642
ebdff0dca2a5 text_of: made even more robust against recurrent errors;
wenzelm
parents: 25582
diff changeset
   286
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59795
diff changeset
   287
fun input_of (Token ((source, range), (kind, _), _)) =
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 58978
diff changeset
   288
  Input.source (delimited_kind kind) source range;
27873
34d61938e27a added source_of';
wenzelm
parents: 27856
diff changeset
   289
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
   290
fun inner_syntax_of tok =
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
   291
  let val x = content_of tok
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59795
diff changeset
   292
  in if YXML.detect x then x else Syntax.implode_input (input_of tok) end;
27747
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   293
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   294
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   295
(* markup reports *)
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   296
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   297
local
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   298
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   299
val token_kind_markup =
59124
wenzelm
parents: 59123
diff changeset
   300
 fn Var => (Markup.var, "")
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   301
  | Type_Ident => (Markup.tfree, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   302
  | Type_Var => (Markup.tvar, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   303
  | String => (Markup.string, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   304
  | Alt_String => (Markup.alt_string, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   305
  | Verbatim => (Markup.verbatim, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   306
  | Cartouche => (Markup.cartouche, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   307
  | Comment => (Markup.comment, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   308
  | Error msg => (Markup.bad, msg)
59124
wenzelm
parents: 59123
diff changeset
   309
  | _ => (Markup.empty, "");
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   310
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   311
fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   312
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   313
fun command_markups keywords x =
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   314
  if Keyword.is_theory_end keywords x then [Markup.keyword2]
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   315
  else if Keyword.is_proof_asm keywords x then [Markup.keyword3]
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   316
  else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   317
  else [Markup.keyword1];
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   318
56063
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   319
in
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   320
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56064
diff changeset
   321
fun keyword_markup (important, keyword) x =
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56064
diff changeset
   322
  if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
55919
2eb8c13339a5 more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents: 55916
diff changeset
   323
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   324
fun completion_report tok =
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   325
  if is_kind Keyword tok
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   326
  then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   327
  else [];
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   328
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   329
fun reports keywords tok =
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   330
  if is_command tok then
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   331
    keyword_reports tok (command_markups keywords (content_of tok))
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   332
  else if is_kind Keyword tok then
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   333
    keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)]
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   334
  else
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   335
    let val (m, text) = token_kind_markup (kind_of tok)
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   336
    in [((pos_of tok, m), text)] end;
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   337
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   338
fun markups keywords = map (#2 o #1) o reports keywords;
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   339
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   340
end;
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   341
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   342
27747
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   343
(* unparse *)
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   344
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   345
fun unparse (Token (_, (kind, x), _)) =
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   346
  (case kind of
43773
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   347
    String => Symbol_Pos.quote_string_qq x
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   348
  | Alt_String => Symbol_Pos.quote_string_bq x
43773
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   349
  | Verbatim => enclose "{*" "*}" x
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   350
  | Cartouche => cartouche x
43773
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   351
  | Comment => enclose "(*" "*)" x
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   352
  | EOF => ""
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   353
  | _ => x);
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   354
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   355
fun unparse_src (Src {args, ...}) = map unparse args;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   356
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   357
fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
55745
b865c3035d5c tuned message -- more markup;
wenzelm
parents: 55744
diff changeset
   358
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   359
fun text_of tok =
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   360
  let
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   361
    val k = str_of_kind (kind_of tok);
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   362
    val ms = markups Keyword.empty_keywords tok;
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   363
    val s = unparse tok;
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   364
  in
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   365
    if s = "" then (k, "")
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   366
    else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   367
    then (k ^ " " ^ Markup.markups ms s, "")
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   368
    else (k, Markup.markups ms s)
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   369
  end;
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   370
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   371
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   372
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   373
(** associated values **)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   374
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   375
(* inlined file content *)
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   376
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   377
fun get_files (Token (_, _, Value (SOME (Files files)))) = files
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   378
  | get_files _ = [];
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   379
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   380
fun put_files [] tok = tok
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   381
  | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   382
  | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   383
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   384
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   385
(* access values *)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   386
58025
wenzelm
parents: 58017
diff changeset
   387
fun make_value name v =
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   388
  Token ((name, Position.no_range), (Internal_Value, name), Value (SOME v));
58025
wenzelm
parents: 58017
diff changeset
   389
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   390
fun get_value (Token (_, _, Value v)) = v
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   391
  | get_value _ = NONE;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   392
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   393
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
   394
  | map_value _ tok = tok;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   395
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   396
fun reports_of_value tok =
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   397
  (case get_value tok of
56063
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   398
    SOME (Literal markup) =>
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   399
      let
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   400
        val pos = pos_of tok;
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   401
        val x = content_of tok;
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   402
      in
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   403
        if Position.is_reported pos then
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   404
          map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x)
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   405
        else []
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   406
      end
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   407
  | _ => []);
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   408
59908
fdf6957f8635 operation on embedded sources for Eisbach;
wenzelm
parents: 59906
diff changeset
   409
fun map_values f =
fdf6957f8635 operation on embedded sources for Eisbach;
wenzelm
parents: 59906
diff changeset
   410
  (map_args o map_value) (fn Source src => Source (map_values f src) | x => f x);
fdf6957f8635 operation on embedded sources for Eisbach;
wenzelm
parents: 59906
diff changeset
   411
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   412
59646
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   413
(* maxidx *)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   414
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   415
fun declare_maxidx tok =
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   416
  (case get_value tok of
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   417
    SOME (Source src) => declare_maxidx_src src
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   418
  | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   419
  | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   420
  | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   421
  | SOME (Attribute _) => I  (* FIXME !? *)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   422
  | SOME (Declaration decl) =>
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   423
      (fn ctxt =>
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   424
        let val ctxt' = Context.proof_map (Morphism.form decl) ctxt
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   425
        in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   426
  | _ => I)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   427
and declare_maxidx_src src = fold declare_maxidx (args_of_src src);
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   428
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   429
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   430
(* transform *)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   431
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   432
fun transform phi =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   433
  map_value (fn v =>
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   434
    (case v of
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   435
      Source src => Source (transform_src phi src)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   436
    | Literal _ => v
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   437
    | Name (a, psi) => Name (a, psi $> phi)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   438
    | Typ T => Typ (Morphism.typ phi T)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   439
    | Term t => Term (Morphism.term phi t)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   440
    | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   441
    | Attribute att => Attribute (Morphism.transform phi att)
58017
5bdb58845eab support for declaration within token source;
wenzelm
parents: 58012
diff changeset
   442
    | Declaration decl => Declaration (Morphism.transform phi decl)
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   443
    | Files _ => v))
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   444
and transform_src phi = map_args (transform phi);
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   445
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   446
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   447
(* static binding *)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   448
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   449
(*1st stage: initialize assignable slots*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   450
fun init_assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   451
  | init_assignable (tok as Token (_, _, Assignable r)) = (r := NONE; tok)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   452
  | init_assignable tok = tok;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   453
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   454
val init_assignable_src = map_args init_assignable;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   455
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   456
(*2nd stage: assign values as side-effect of scanning*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   457
fun assign v (Token (_, _, Assignable r)) = r := v
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   458
  | assign _ _ = ();
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   459
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   460
(*3rd stage: static closure of final values*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   461
fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   462
  | closure tok = tok;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   463
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   464
val closure_src = map_args closure;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   465
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   466
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   467
(* pretty *)
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   468
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   469
fun pretty_value ctxt tok =
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   470
  (case get_value tok of
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   471
    SOME (Literal markup) =>
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   472
      let val x = content_of tok
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   473
      in Pretty.mark_str (keyword_markup markup x, x) end
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   474
  | SOME (Name (a, _)) => Pretty.str (quote a)
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   475
  | SOME (Typ T) => Syntax.pretty_typ ctxt T
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   476
  | SOME (Term t) => Syntax.pretty_term ctxt t
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   477
  | SOME (Fact (_, ths)) =>
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   478
      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   479
  | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   480
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   481
fun pretty_src ctxt src =
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   482
  let
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   483
    val Src {name = (name, _), args, checked} = src;
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   484
    val prt_name =
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   485
      (case checked of
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   486
        NONE => Pretty.str name
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   487
      | SOME (_, markup) => Pretty.mark_str (markup, name));
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   488
    val prt_arg = pretty_value ctxt;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   489
  in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   490
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   491
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   492
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   493
(** scanners **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   494
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   495
open Basic_Symbol_Pos;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   496
48764
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   497
val err_prefix = "Outer lexical error: ";
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   498
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   499
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   500
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   501
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   502
(* scan symbolic idents *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   503
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   504
val scan_symid =
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   505
  Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) ||
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   506
  Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   507
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   508
fun is_symid str =
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   509
  (case try Symbol.explode str of
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   510
    SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   511
  | SOME ss => forall Symbol.is_symbolic_char ss
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   512
  | _ => false);
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   513
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   514
fun ident_or_symbolic "begin" = false
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   515
  | ident_or_symbolic ":" = true
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   516
  | ident_or_symbolic "::" = true
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50201
diff changeset
   517
  | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   518
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   519
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   520
(* scan verbatim text *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   521
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   522
val scan_verb =
55107
1a29ea173bf9 tuned signature;
wenzelm
parents: 55106
diff changeset
   523
  $$$ "*" --| Scan.ahead (~$$ "}") ||
58854
b979c781c2db discontinued obsolete \<^sync> marker;
wenzelm
parents: 58850
diff changeset
   524
  Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   525
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   526
val scan_verbatim =
55107
1a29ea173bf9 tuned signature;
wenzelm
parents: 55106
diff changeset
   527
  Scan.ahead ($$ "{" -- $$ "*") |--
55106
080c0006e917 tuned error messages, more accurate position;
wenzelm
parents: 55105
diff changeset
   528
    !!! "unclosed verbatim text"
55107
1a29ea173bf9 tuned signature;
wenzelm
parents: 55106
diff changeset
   529
      ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
58850
1bb0ad7827b4 discontinued obsolete tty and prompt;
wenzelm
parents: 58045
diff changeset
   530
        ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   531
48743
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   532
val recover_verbatim =
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   533
  $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   534
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   535
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   536
(* scan cartouche *)
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   537
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   538
val scan_cartouche =
55104
8284c0d5bf52 clarified scan_cartouche_depth, according to Scala version;
wenzelm
parents: 55103
diff changeset
   539
  Symbol_Pos.scan_pos --
55105
75815b3b38a1 tuned -- more direct err_prefix;
wenzelm
parents: 55104
diff changeset
   540
    ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   541
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   542
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   543
(* scan space *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   544
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
   545
fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   546
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   547
val scan_space =
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
   548
  Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] ||
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48764
diff changeset
   549
  Scan.many space_symbol @@@ $$$ "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   550
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   551
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   552
(* scan comment *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   553
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   554
val scan_comment =
55105
75815b3b38a1 tuned -- more direct err_prefix;
wenzelm
parents: 55104
diff changeset
   555
  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos);
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   556
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   557
27663
098798321622 maintain token range;
wenzelm
parents: 27358
diff changeset
   558
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   559
(** token sources **)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   560
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   561
fun source_proper src = src |> Source.filter is_proper;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   562
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   563
local
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   564
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   565
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   566
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   567
fun token k ss =
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 42503
diff changeset
   568
  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
   569
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   570
fun token_range k (pos1, (ss, pos2)) =
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 59085
diff changeset
   571
  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
   572
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   573
fun scan_token keywords = !!! "bad input"
48764
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   574
  (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   575
    Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   576
    scan_verbatim >> token_range Verbatim ||
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   577
    scan_cartouche >> token_range Cartouche ||
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   578
    scan_comment >> token_range Comment ||
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   579
    scan_space >> token Space ||
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   580
    (Scan.max token_leq
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   581
      (Scan.max token_leq
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   582
        (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   583
        (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   584
      (Lexicon.scan_longid >> pair Long_Ident ||
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   585
        Lexicon.scan_id >> pair Ident ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   586
        Lexicon.scan_var >> pair Var ||
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   587
        Lexicon.scan_tid >> pair Type_Ident ||
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   588
        Lexicon.scan_tvar >> pair Type_Var ||
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   589
        Lexicon.scan_float >> pair Float ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   590
        Lexicon.scan_nat >> pair Nat ||
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   591
        scan_symid >> pair Sym_Ident) >> uncurry token));
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   592
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   593
fun recover msg =
48743
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   594
  (Symbol_Pos.recover_string_qq ||
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   595
    Symbol_Pos.recover_string_bq ||
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   596
    recover_verbatim ||
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   597
    Symbol_Pos.recover_cartouche ||
48743
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   598
    Symbol_Pos.recover_comment ||
58854
b979c781c2db discontinued obsolete \<^sync> marker;
wenzelm
parents: 58850
diff changeset
   599
    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   600
  >> (single o token (Error msg));
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   601
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   602
in
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   603
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
   604
fun source' strict keywords =
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   605
  let
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   606
    val scan_strict = Scan.bulk (scan_token keywords);
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   607
    val scan = if strict then scan_strict else Scan.recover scan_strict recover;
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   608
  in Source.source Symbol_Pos.stopper scan end;
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   609
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
   610
fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords;
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
   611
fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords;
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   612
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   613
end;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   614
30586
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   615
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   616
(* explode *)
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   617
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   618
fun explode keywords pos =
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   619
  Source.of_string #>
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   620
  Symbol.source #>
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   621
  source keywords pos #>
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   622
  Source.exhaust;
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   623
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   624
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   625
(* make *)
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   626
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   627
fun make ((k, n), s) pos =
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   628
  let
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   629
    val pos' = Position.advance_offset n pos;
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   630
    val range = Position.range pos pos';
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   631
    val tok =
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   632
      if k < Vector.length immediate_kinds then
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   633
        Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   634
      else
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   635
        (case explode Keyword.empty_keywords pos s of
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   636
          [tok] => tok
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   637
        | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot))
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   638
  in (tok, pos') end;
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   639
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   640
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   641
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   642
(** parsers **)
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   643
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   644
type 'a parser = T list -> 'a * T list;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   645
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   646
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   647
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   648
(* read source *)
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   649
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   650
fun read_no_commands keywords scan syms =
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   651
  Source.of_list syms
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
   652
  |> source' true (Keyword.no_command_keywords keywords)
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   653
  |> source_proper
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   654
  |> Source.source stopper (Scan.error (Scan.bulk scan))
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   655
  |> Source.exhaust;
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   656
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   657
fun read_antiq keywords scan (syms, pos) =
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   658
  let
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   659
    fun err msg =
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   660
      cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   661
        "@{" ^ Symbol_Pos.content syms ^ "}");
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   662
    val res = read_no_commands keywords scan syms handle ERROR msg => err msg;
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   663
  in (case res of [x] => x | _ => err "") end;
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   664
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   665
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   666
(* wrapped syntax *)
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   667
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   668
fun syntax_generic scan (Src {name = (name, pos), args = args0, checked}) context =
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   669
  let
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   670
    val args1 = map init_assignable args0;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   671
    fun reported_text () =
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   672
      if Context_Position.is_visible_generic context then
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   673
        ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   674
        |> map (fn (p, m) => Position.reported_text p m "")
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   675
      else [];
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   676
  in
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   677
    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   678
      (SOME x, (context', [])) =>
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   679
        let val _ = Output.report (reported_text ())
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   680
        in (x, context') end
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   681
    | (_, (_, args2)) =>
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   682
        let
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   683
          val print_name =
59913
a7f6359665c6 tuned signature;
wenzelm
parents: 59908
diff changeset
   684
            (case checked of
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   685
              NONE => quote name
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   686
            | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   687
          val print_args =
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   688
            if null args2 then "" else ":\n  " ^ space_implode " " (map print args2);
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   689
        in
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   690
          error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   691
            Markup.markup_report (implode (reported_text ())))
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   692
        end)
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   693
  end;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   694
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   695
fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   696
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   697
end;
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   698
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   699
type 'a parser = 'a Token.parser;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   700
type 'a context_parser = 'a Token.context_parser;