src/Pure/Isar/token.ML
author wenzelm
Tue, 31 Jul 2018 21:21:20 +0200
changeset 68730 0bc491938780
parent 68729 3a02b424d5fb
child 69851 29a4f633609e
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*)
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
    14
    String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
    15
    (*special content*)
61819
wenzelm
parents: 61814
diff changeset
    16
    Error of string | 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
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    20
  type src = T list
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    21
  type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    22
  datatype value =
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    23
    Source of src |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    24
    Literal of bool * Markup.T |
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    25
    Name of name_value * morphism |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    26
    Typ of typ |
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    27
    Term of term |
57942
e5bec882fdd0 more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents: 56202
diff changeset
    28
    Fact of string option * thm list |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    29
    Attribute of morphism -> attribute |
58017
5bdb58845eab support for declaration within token source;
wenzelm
parents: 58012
diff changeset
    30
    Declaration of declaration |
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
    31
    Files of file Exn.result list
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
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 67652
diff changeset
    34
  val adjust_offsets: (int -> int option) -> T -> 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
    35
  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
    36
  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
    37
  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
    38
  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
    39
  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
    40
  val is_kind: kind -> 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
    41
  val is_command: T -> bool
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59913
diff changeset
    42
  val keyword_with: (string -> bool) -> T -> bool
59939
7d46aa03696e support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents: 59924
diff changeset
    43
  val is_command_modifier: T -> bool
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59913
diff changeset
    44
  val ident_with: (string -> bool) -> 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
    45
  val is_proper: T -> bool
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
    46
  val is_comment: T -> bool
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
    47
  val is_informal_comment: T -> bool
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
    48
  val is_formal_comment: T -> bool
68729
3a02b424d5fb clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents: 68298
diff changeset
    49
  val is_ignored: 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_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
    51
  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
    52
  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
    53
  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
    54
  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
    55
  val is_newline: T -> bool
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
    56
  val content_of: T -> string
68298
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
    57
  val source_of: T -> string
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59795
diff changeset
    58
  val input_of: T -> Input.source
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
    59
  val inner_syntax_of: T -> string
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56064
diff changeset
    60
  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
    61
  val completion_report: T -> Position.report_text list
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
    62
  val reports: Keyword.keywords -> T -> Position.report_text list
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
    63
  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
    64
  val unparse: T -> string
55745
b865c3035d5c tuned message -- more markup;
wenzelm
parents: 55744
diff changeset
    65
  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
    66
  val text_of: T -> string * string
54520
cee77d2e9582 release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents: 54519
diff changeset
    67
  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
    68
  val put_files: file Exn.result list -> T -> 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
    69
  val get_value: T -> value option
61822
wenzelm
parents: 61820
diff changeset
    70
  val reports_of_value: T -> Position.report list
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    71
  val name_value: name_value -> value
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    72
  val get_name: T -> name_value option
59646
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
    73
  val declare_maxidx: T -> Proof.context -> Proof.context
61820
e65344e3eeb5 tuned signature;
wenzelm
parents: 61819
diff changeset
    74
  val map_facts: (string option -> thm list -> thm list) -> T -> T
67652
11716a084cae clarified signature;
wenzelm
parents: 67504
diff changeset
    75
  val trim_context_src: src -> src
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    76
  val transform: morphism -> T -> T
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
    77
  val init_assignable: T -> T
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    78
  val assign: value option -> T -> T
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    79
  val evaluate: ('a -> value) -> (T -> 'a) -> T -> '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
    80
  val closure: T -> T
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
    81
  val pretty_value: Proof.context -> T -> Pretty.T
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    82
  val name_of_src: src -> string * Position.T
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    83
  val args_of_src: src -> T list
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    84
  val checked_src: src -> bool
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    85
  val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    86
  val pretty_src: Proof.context -> src -> Pretty.T
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
    87
  val ident_or_symbolic: string -> bool
61471
9d4c08af61b8 support control symbol antiquotations;
wenzelm
parents: 61268
diff changeset
    88
  val read_cartouche: Symbol_Pos.T list -> T
67497
3a0b08e7dfe9 clarified signature;
wenzelm
parents: 67495
diff changeset
    89
  val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
    90
  val explode: Keyword.keywords -> Position.T -> string -> T list
67495
90d760fa8f34 clarified operations;
wenzelm
parents: 67446
diff changeset
    91
  val explode0: Keyword.keywords -> string -> T list
63640
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
    92
  val print_name: Keyword.keywords -> string -> string
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
    93
  val make: (int * int) * string -> Position.T -> T * Position.T
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    94
  val make_string: string * Position.T -> T
63019
80ef19b51493 prefer internal attribute source;
wenzelm
parents: 62969
diff changeset
    95
  val make_int: int -> T list
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
    96
  val make_src: string * Position.T -> T list -> src
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    97
  type 'a parser = T list -> 'a * T list
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
    98
  type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
67504
310114bec0d7 clarified signature;
wenzelm
parents: 67503
diff changeset
    99
  val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   100
  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
   101
  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
   102
  val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   103
end;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   104
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
   105
structure Token: TOKEN =
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   106
struct
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   107
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   108
(** tokens **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   109
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   110
(* token kind *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   111
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 32738
diff changeset
   112
datatype kind =
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   113
  (*immediate source*)
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   114
  Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   115
  Float | Space |
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   116
  (*delimited content*)
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   117
  String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   118
  (*special content*)
61819
wenzelm
parents: 61814
diff changeset
   119
  Error of string | EOF;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   120
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   121
val str_of_kind =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   122
 fn Command => "command"
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   123
  | Keyword => "keyword"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   124
  | Ident => "identifier"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   125
  | Long_Ident => "long identifier"
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   126
  | Sym_Ident => "symbolic identifier"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   127
  | Var => "schematic variable"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   128
  | Type_Ident => "type variable"
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   129
  | 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
   130
  | Nat => "natural number"
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 38229
diff changeset
   131
  | Float => "floating-point number"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   132
  | Space => "white space"
55103
57d87ec3da4c tuned errors;
wenzelm
parents: 55033
diff changeset
   133
  | String => "quoted string"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   134
  | Alt_String => "back-quoted string"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   135
  | Verbatim => "verbatim text"
55103
57d87ec3da4c tuned errors;
wenzelm
parents: 55033
diff changeset
   136
  | Cartouche => "text cartouche"
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   137
  | Comment NONE => "informal comment"
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   138
  | Comment (SOME _) => "formal comment"
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   139
  | Error _ => "bad input"
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48905
diff changeset
   140
  | EOF => "end-of-input";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   141
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   142
val immediate_kinds =
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   143
  Vector.fromList
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   144
    [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
   145
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   146
val delimited_kind =
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   147
  (fn String => true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   148
    | Alt_String => true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   149
    | Verbatim => true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   150
    | Cartouche => true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   151
    | Comment _ => true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   152
    | _ => false);
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55788
diff changeset
   153
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   154
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   155
(* datatype token *)
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
(*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
   158
  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
   159
  args.ML).  Note that an assignable ref designates an intermediate
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   160
  state of internalization -- it is NOT meant to persist.*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   161
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   162
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
   163
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   164
type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring};
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   165
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   166
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   167
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   168
and slot =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   169
  Slot |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   170
  Value of value option |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   171
  Assignable of value option Unsynchronized.ref
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   172
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   173
and value =
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   174
  Source of T list |
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   175
  Literal of bool * Markup.T |
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   176
  Name of name_value * morphism |
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   177
  Typ of typ |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   178
  Term of term |
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   179
  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
   180
  Attribute of morphism -> attribute |
58017
5bdb58845eab support for declaration within token source;
wenzelm
parents: 58012
diff changeset
   181
  Declaration of declaration |
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   182
  Files of file Exn.result list;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   183
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   184
type src = T list;
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   185
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   186
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   187
(* position *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   188
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   189
fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   190
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
27663
098798321622 maintain token range;
wenzelm
parents: 27358
diff changeset
   191
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   192
fun range_of (toks as tok :: _) =
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   193
      let val pos' = end_pos_of (List.last toks)
62797
e08c44eed27f tuned signature;
wenzelm
parents: 62782
diff changeset
   194
      in Position.range (pos_of tok, pos') end
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   195
  | range_of [] = Position.no_range;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   196
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 67652
diff changeset
   197
fun adjust_offsets adjust (Token ((x, range), y, z)) =
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 67652
diff changeset
   198
  Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 67652
diff changeset
   199
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   200
58855
2885e2eaa0fb removed pointless markup;
wenzelm
parents: 58854
diff changeset
   201
(* stopper *)
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   202
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   203
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
   204
val eof = mk_eof Position.none;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   205
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   206
fun is_eof (Token (_, (EOF, _), _)) = true
27733
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   207
  | is_eof _ = false;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   208
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   209
val not_eof = not o is_eof;
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   210
27752
ea7d573e565f removed obsolete range_of (already included in position);
wenzelm
parents: 27747
diff changeset
   211
val stopper =
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   212
  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
   213
d3d7038fb7b5 abstract type Scan.stopper, position taken from last input token;
wenzelm
parents: 27663
diff changeset
   214
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   215
(* kind of token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   216
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   217
fun kind_of (Token (_, (k, _), _)) = k;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   218
fun is_kind k (Token (_, (k', _), _)) = k = k';
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   219
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
   220
val is_command = is_kind Command;
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   221
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   222
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   223
  | keyword_with _ _ = false;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   224
59990
a81dc82ecba3 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents: 59939
diff changeset
   225
val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified");
59924
801b979ec0c2 more general notion of command span: command keyword not necessarily at start;
wenzelm
parents: 59913
diff changeset
   226
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   227
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
16029
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   228
  | ident_with _ _ = false;
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   229
68729
3a02b424d5fb clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents: 68298
diff changeset
   230
fun is_ignored (Token (_, (Space, _), _)) = true
3a02b424d5fb clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents: 68298
diff changeset
   231
  | is_ignored (Token (_, (Comment NONE, _), _)) = true
3a02b424d5fb clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents: 68298
diff changeset
   232
  | is_ignored _ = false;
3a02b424d5fb clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents: 68298
diff changeset
   233
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   234
fun is_proper (Token (_, (Space, _), _)) = false
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   235
  | is_proper (Token (_, (Comment _, _), _)) = false
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   236
  | is_proper _ = true;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   237
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   238
fun is_comment (Token (_, (Comment _, _), _)) = true
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   239
  | is_comment _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   240
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   241
fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   242
  | is_informal_comment _ = false;
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   243
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   244
fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   245
  | is_formal_comment _ = false;
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   246
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   247
fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   248
  | is_begin_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   249
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   250
fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   251
  | is_end_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   252
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48743
diff changeset
   253
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
   254
  | 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
   255
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   256
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   257
(* blanks and newlines -- space tokens obey lines *)
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   258
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
   259
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
   260
  | 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
   261
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   262
fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   263
  | is_blank _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   264
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   265
fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   266
  | is_newline _ = false;
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   267
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   268
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   269
(* token content *)
9155
adfa40218e06 OuterLex.name_of: include val;
wenzelm
parents: 9130
diff changeset
   270
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
   271
fun content_of (Token (_, (_, x), _)) = x;
68298
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
   272
fun source_of (Token ((source, _), _, _)) = source;
25642
ebdff0dca2a5 text_of: made even more robust against recurrent errors;
wenzelm
parents: 25582
diff changeset
   273
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59795
diff changeset
   274
fun input_of (Token ((source, range), (kind, _), _)) =
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 58978
diff changeset
   275
  Input.source (delimited_kind kind) source range;
27873
34d61938e27a added source_of';
wenzelm
parents: 27856
diff changeset
   276
59795
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
   277
fun inner_syntax_of tok =
d453c69596cc clarified input source;
wenzelm
parents: 59666
diff changeset
   278
  let val x = content_of tok
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59795
diff changeset
   279
  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
   280
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   281
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   282
(* markup reports *)
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   283
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   284
local
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   285
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   286
val token_kind_markup =
59124
wenzelm
parents: 59123
diff changeset
   287
 fn Var => (Markup.var, "")
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   288
  | Type_Ident => (Markup.tfree, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   289
  | Type_Var => (Markup.tvar, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   290
  | String => (Markup.string, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   291
  | Alt_String => (Markup.alt_string, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   292
  | Verbatim => (Markup.verbatim, "")
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   293
  | Cartouche => (Markup.cartouche, "")
67440
e5ba0ca1e465 clarified markup;
wenzelm
parents: 67439
diff changeset
   294
  | Comment _ => (Markup.comment, "")
64677
8dc24130e8fe more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents: 64421
diff changeset
   295
  | Error msg => (Markup.bad (), msg)
59124
wenzelm
parents: 59123
diff changeset
   296
  | _ => (Markup.empty, "");
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   297
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   298
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
   299
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   300
fun command_markups keywords x =
66067
cdbcb417db67 more markup for HTML rendering;
wenzelm
parents: 66066
diff changeset
   301
  if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties]
65174
c0388fbd8096 avoid extra decorations for regular command keywords;
wenzelm
parents: 64677
diff changeset
   302
  else
c0388fbd8096 avoid extra decorations for regular command keywords;
wenzelm
parents: 64677
diff changeset
   303
    (if Keyword.is_proof_asm keywords x then [Markup.keyword3]
c0388fbd8096 avoid extra decorations for regular command keywords;
wenzelm
parents: 64677
diff changeset
   304
     else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
c0388fbd8096 avoid extra decorations for regular command keywords;
wenzelm
parents: 64677
diff changeset
   305
     else [Markup.keyword1])
66066
7ac97dea27d2 tuned signature;
wenzelm
parents: 66044
diff changeset
   306
    |> map Markup.command_properties;
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   307
56063
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   308
in
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   309
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56064
diff changeset
   310
fun keyword_markup (important, keyword) x =
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56064
diff changeset
   311
  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
   312
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   313
fun completion_report tok =
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   314
  if is_kind Keyword tok
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   315
  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
   316
  else [];
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   317
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   318
fun reports keywords tok =
59123
e68e44836d04 imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents: 59112
diff changeset
   319
  if is_command tok then
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   320
    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
   321
  else if is_kind Keyword tok then
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 65174
diff changeset
   322
    keyword_reports tok
66067
cdbcb417db67 more markup for HTML rendering;
wenzelm
parents: 66066
diff changeset
   323
      [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)]
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   324
  else
68298
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
   325
    let
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
   326
      val pos = pos_of tok;
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
   327
      val (m, text) = token_kind_markup (kind_of tok);
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
   328
      val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos));
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68183
diff changeset
   329
    in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end;
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55914
diff changeset
   330
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   331
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
   332
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   333
end;
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   334
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55709
diff changeset
   335
27747
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   336
(* unparse *)
d41abb7bc08a token: maintain of source, which retains original position information;
wenzelm
parents: 27733
diff changeset
   337
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   338
fun unparse (Token (_, (kind, x), _)) =
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   339
  (case kind of
43773
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   340
    String => Symbol_Pos.quote_string_qq x
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   341
  | Alt_String => Symbol_Pos.quote_string_bq x
43773
e8ba493027a3 more precise Symbol_Pos.quote_string;
wenzelm
parents: 43731
diff changeset
   342
  | Verbatim => enclose "{*" "*}" x
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   343
  | Cartouche => cartouche x
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   344
  | Comment NONE => enclose "(*" "*)" x
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   345
  | EOF => ""
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   346
  | _ => x);
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   347
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   348
fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
55745
b865c3035d5c tuned message -- more markup;
wenzelm
parents: 55744
diff changeset
   349
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   350
fun text_of tok =
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   351
  let
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   352
    val k = str_of_kind (kind_of tok);
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   353
    val ms = markups Keyword.empty_keywords tok;
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   354
    val s = unparse tok;
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   355
  in
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   356
    if s = "" then (k, "")
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   357
    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
   358
    then (k ^ " " ^ Markup.markups ms s, "")
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   359
    else (k, Markup.markups ms s)
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents: 58855
diff changeset
   360
  end;
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   361
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   362
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   363
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   364
(** associated values **)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   365
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   366
(* inlined file content *)
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   367
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   368
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
   369
  | get_files _ = [];
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   370
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   371
fun put_files [] tok = tok
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 51266
diff changeset
   372
  | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   373
  | 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
   374
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48771
diff changeset
   375
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   376
(* access values *)
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   377
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   378
fun get_value (Token (_, _, Value v)) = v
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   379
  | get_value _ = NONE;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   380
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   381
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
   382
  | map_value _ tok = tok;
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   383
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   384
61822
wenzelm
parents: 61820
diff changeset
   385
(* reports of value *)
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   386
61822
wenzelm
parents: 61820
diff changeset
   387
fun get_assignable_value (Token (_, _, Assignable r)) = ! r
wenzelm
parents: 61820
diff changeset
   388
  | get_assignable_value (Token (_, _, Value v)) = v
wenzelm
parents: 61820
diff changeset
   389
  | get_assignable_value _ = NONE;
60211
c0f686b39ebb modifier markup for all parsed tokens;
wenzelm
parents: 59990
diff changeset
   390
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   391
fun reports_of_value tok =
60211
c0f686b39ebb modifier markup for all parsed tokens;
wenzelm
parents: 59990
diff changeset
   392
  (case get_assignable_value tok of
56063
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   393
    SOME (Literal markup) =>
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   394
      let
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   395
        val pos = pos_of tok;
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   396
        val x = content_of tok;
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   397
      in
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   398
        if Position.is_reported pos then
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   399
          map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x)
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   400
        else []
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   401
      end
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55919
diff changeset
   402
  | _ => []);
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55828
diff changeset
   403
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   404
61822
wenzelm
parents: 61820
diff changeset
   405
(* name value *)
wenzelm
parents: 61820
diff changeset
   406
wenzelm
parents: 61820
diff changeset
   407
fun name_value a = Name (a, Morphism.identity);
wenzelm
parents: 61820
diff changeset
   408
wenzelm
parents: 61820
diff changeset
   409
fun get_name tok =
wenzelm
parents: 61820
diff changeset
   410
  (case get_assignable_value tok of
wenzelm
parents: 61820
diff changeset
   411
    SOME (Name (a, _)) => SOME a
wenzelm
parents: 61820
diff changeset
   412
  | _ => NONE);
wenzelm
parents: 61820
diff changeset
   413
wenzelm
parents: 61820
diff changeset
   414
59646
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   415
(* maxidx *)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   416
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   417
fun declare_maxidx tok =
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   418
  (case get_value tok of
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   419
    SOME (Source src) => fold declare_maxidx src
59646
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   420
  | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   421
  | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   422
  | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   423
  | SOME (Attribute _) => I  (* FIXME !? *)
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   424
  | SOME (Declaration decl) =>
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   425
      (fn ctxt =>
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   426
        let val ctxt' = Context.proof_map (Morphism.form decl) ctxt
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   427
        in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end)
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   428
  | _ => I);
59646
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   429
48d400469bcb added declare_maxidx operations for Eisbach;
wenzelm
parents: 59125
diff changeset
   430
61080
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   431
(* fact values *)
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   432
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   433
fun map_facts f =
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   434
  map_value (fn v =>
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   435
    (case v of
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   436
      Source src => Source (map (map_facts f) src)
61820
e65344e3eeb5 tuned signature;
wenzelm
parents: 61819
diff changeset
   437
    | Fact (a, ths) => Fact (a, f a ths)
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   438
    | _ => v));
61080
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   439
67652
11716a084cae clarified signature;
wenzelm
parents: 67504
diff changeset
   440
val trim_context_src = (map o map_facts) (K (map Thm.trim_context));
11716a084cae clarified signature;
wenzelm
parents: 67504
diff changeset
   441
61080
3bccde9cbb9d trim context more thoroughly;
wenzelm
parents: 60211
diff changeset
   442
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   443
(* transform *)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   444
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   445
fun transform phi =
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   446
  map_value (fn v =>
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   447
    (case v of
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   448
      Source src => Source (map (transform phi) src)
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   449
    | Literal _ => v
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   450
    | Name (a, psi) => Name (a, psi $> phi)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   451
    | Typ T => Typ (Morphism.typ phi T)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   452
    | Term t => Term (Morphism.term phi t)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   453
    | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   454
    | Attribute att => Attribute (Morphism.transform phi att)
58017
5bdb58845eab support for declaration within token source;
wenzelm
parents: 58012
diff changeset
   455
    | Declaration decl => Declaration (Morphism.transform phi decl)
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   456
    | Files _ => v));
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   457
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   458
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   459
(* static binding *)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   460
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   461
(*1st stage: initialize assignable slots*)
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   462
fun init_assignable tok =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   463
  (case tok of
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   464
    Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE))
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   465
  | Token (_, _, Value _) => tok
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   466
  | Token (_, _, Assignable r) => (r := NONE; tok));
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   467
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   468
(*2nd stage: assign values as side-effect of scanning*)
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   469
fun assign v tok =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   470
  (case tok of
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   471
    Token (x, y, Slot) => Token (x, y, Value v)
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   472
  | Token (_, _, Value _) => tok
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   473
  | Token (_, _, Assignable r) => (r := v; tok));
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   474
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   475
fun evaluate mk eval arg =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   476
  let val x = eval arg in (assign (SOME (mk x)) arg; x) end;
58012
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   477
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   478
(*3rd stage: static closure of final values*)
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   479
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
   480
  | closure tok = tok;
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   481
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   482
0b0519c41229 support for nested Token.src within Token.T;
wenzelm
parents: 58011
diff changeset
   483
(* pretty *)
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   484
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   485
fun pretty_value ctxt tok =
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   486
  (case get_value tok of
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   487
    SOME (Literal markup) =>
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   488
      let val x = content_of tok
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   489
      in Pretty.mark_str (keyword_markup markup x, x) end
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   490
  | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt))
57944
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   491
  | SOME (Typ T) => Syntax.pretty_typ ctxt T
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   492
  | SOME (Term t) => Syntax.pretty_term ctxt t
fff8d328da56 more informative Token.Name with history of morphisms;
wenzelm
parents: 57942
diff changeset
   493
  | SOME (Fact (_, ths)) =>
62094
7d47cf67516d prefer non-ASCII output;
wenzelm
parents: 61825
diff changeset
   494
      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   495
  | _ => 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
   496
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   497
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   498
(* src *)
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   499
61825
69b035408b18 make SML/NJ happy;
wenzelm
parents: 61822
diff changeset
   500
fun dest_src ([]: src) = raise Fail "Empty token source"
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   501
  | dest_src (head :: args) = (head, args);
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   502
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   503
fun name_of_src src =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   504
  let
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   505
    val head = #1 (dest_src src);
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   506
    val name =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   507
      (case get_name head of
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   508
        SOME {name, ...} => name
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   509
      | NONE => content_of head);
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   510
  in (name, pos_of head) end;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   511
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   512
val args_of_src = #2 o dest_src;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   513
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   514
fun pretty_src ctxt src =
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   515
  let
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   516
    val (head, args) = dest_src src;
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   517
    val prt_name =
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   518
      (case get_name head of
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   519
        SOME {print, ...} => Pretty.mark_str (print ctxt)
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   520
      | NONE => Pretty.str (content_of head));
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   521
  in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   522
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   523
fun checked_src (head :: _) = is_some (get_name head)
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   524
  | checked_src [] = true;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   525
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   526
fun check_src ctxt get_table src =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   527
  let
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   528
    val (head, args) = dest_src src;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   529
    val table = get_table ctxt;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   530
  in
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   531
    (case get_name head of
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   532
      SOME {name, ...} => (src, Name_Space.get table name)
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   533
    | NONE =>
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   534
        let
64421
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   535
          val pos = pos_of head;
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   536
          val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos);
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   537
          val _ = Context_Position.report ctxt pos Markup.operator;
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   538
          val kind = Name_Space.kind_of (Name_Space.space_of_table table);
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   539
          fun print ctxt' =
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   540
            Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   541
          val value = name_value {name = name, kind = kind, print = print};
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   542
          val head' = closure (assign (SOME value) head);
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   543
        in (head' :: args, x) end)
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   544
  end;
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   545
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   546
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59124
diff changeset
   547
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   548
(** scanners **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   549
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   550
open Basic_Symbol_Pos;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   551
48764
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   552
val err_prefix = "Outer lexical error: ";
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   553
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   554
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   555
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   556
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   557
(* scan symbolic idents *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   558
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   559
val scan_symid =
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   560
  Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) ||
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40523
diff changeset
   561
  Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   562
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   563
fun is_symid str =
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   564
  (case try Symbol.explode str of
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   565
    SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   566
  | SOME ss => forall Symbol.is_symbolic_char ss
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   567
  | _ => false);
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   568
27814
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   569
fun ident_or_symbolic "begin" = false
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   570
  | ident_or_symbolic ":" = true
05a50886dacb unified Args.T with OuterLex.token;
wenzelm
parents: 27799
diff changeset
   571
  | ident_or_symbolic "::" = true
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50201
diff changeset
   572
  | 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
   573
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   574
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   575
(* scan verbatim text *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   576
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   577
val scan_verb =
55107
1a29ea173bf9 tuned signature;
wenzelm
parents: 55106
diff changeset
   578
  $$$ "*" --| Scan.ahead (~$$ "}") ||
58854
b979c781c2db discontinued obsolete \<^sync> marker;
wenzelm
parents: 58850
diff changeset
   579
  Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   580
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   581
val scan_verbatim =
55107
1a29ea173bf9 tuned signature;
wenzelm
parents: 55106
diff changeset
   582
  Scan.ahead ($$ "{" -- $$ "*") |--
55106
080c0006e917 tuned error messages, more accurate position;
wenzelm
parents: 55105
diff changeset
   583
    !!! "unclosed verbatim text"
55107
1a29ea173bf9 tuned signature;
wenzelm
parents: 55106
diff changeset
   584
      ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
61476
1884c40f1539 tuned signature;
wenzelm
parents: 61471
diff changeset
   585
        (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   586
48743
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   587
val recover_verbatim =
61476
1884c40f1539 tuned signature;
wenzelm
parents: 61471
diff changeset
   588
  $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb;
48743
a72f8ffecf31 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents: 48741
diff changeset
   589
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   590
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   591
(* scan cartouche *)
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   592
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   593
val scan_cartouche =
55104
8284c0d5bf52 clarified scan_cartouche_depth, according to Scala version;
wenzelm
parents: 55103
diff changeset
   594
  Symbol_Pos.scan_pos --
55105
75815b3b38a1 tuned -- more direct err_prefix;
wenzelm
parents: 55104
diff changeset
   595
    ((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
   596
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   597
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   598
(* scan space *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   599
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
   600
fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   601
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   602
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
   603
  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
   604
  Scan.many space_symbol @@@ $$$ "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   605
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   606
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   607
(* scan comment *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   608
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   609
val scan_comment =
55105
75815b3b38a1 tuned -- more direct err_prefix;
wenzelm
parents: 55104
diff changeset
   610
  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
   611
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   612
27663
098798321622 maintain token range;
wenzelm
parents: 27358
diff changeset
   613
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   614
(** token sources **)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   615
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   616
local
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   617
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   618
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   619
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   620
fun token k ss =
43709
717e96cf9527 discontinued special treatment of hard tabulators;
wenzelm
parents: 42503
diff changeset
   621
  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
   622
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   623
fun token_range k (pos1, (ss, pos2)) =
59112
e670969f34df expand ML cartouches to Input.source;
wenzelm
parents: 59085
diff changeset
   624
  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
   625
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   626
fun scan_token keywords = !!! "bad input"
48764
4fe0920d5049 proper error prefixes;
wenzelm
parents: 48749
diff changeset
   627
  (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   628
    Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27780
diff changeset
   629
    scan_verbatim >> token_range Verbatim ||
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   630
    scan_cartouche >> token_range Cartouche ||
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 66067
diff changeset
   631
    scan_comment >> token_range (Comment NONE) ||
67446
1f4d167b6ac9 discontinued old form of marginal comments;
wenzelm
parents: 67440
diff changeset
   632
    Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   633
    scan_space >> token Space ||
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   634
    (Scan.max token_leq
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   635
      (Scan.max token_leq
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   636
        (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   637
        (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   638
      (Lexicon.scan_longid >> pair Long_Ident ||
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   639
        Lexicon.scan_id >> pair Ident ||
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 40958
diff changeset
   640
        Lexicon.scan_var >> pair Var ||
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   641
        Lexicon.scan_tid >> pair Type_Ident ||
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   642
        Lexicon.scan_tvar >> pair Type_Var ||
62782
057e8dbe4326 clarified modules;
wenzelm
parents: 62094
diff changeset
   643
        Symbol_Pos.scan_float >> pair Float ||
057e8dbe4326 clarified modules;
wenzelm
parents: 62094
diff changeset
   644
        Symbol_Pos.scan_nat >> pair Nat ||
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   645
        scan_symid >> pair Sym_Ident) >> uncurry token));
27769
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   646
ad50c38ef842 improved position handling due to SymbolPos.T;
wenzelm
parents: 27752
diff changeset
   647
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
   648
  (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
   649
    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
   650
    recover_verbatim ||
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54520
diff changeset
   651
    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
   652
    Symbol_Pos.recover_comment ||
58854
b979c781c2db discontinued obsolete \<^sync> marker;
wenzelm
parents: 58850
diff changeset
   653
    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
   654
  >> (single o token (Error msg));
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   655
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   656
in
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   657
67497
3a0b08e7dfe9 clarified signature;
wenzelm
parents: 67495
diff changeset
   658
fun make_source keywords {strict} =
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   659
  let
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   660
    val scan_strict = Scan.bulk (scan_token keywords);
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   661
    val scan = if strict then scan_strict else Scan.recover scan_strict recover;
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   662
  in Source.source Symbol_Pos.stopper scan end;
27780
7d0910f662f7 more precise positions due to SymbolsPos.implode_delim;
wenzelm
parents: 27769
diff changeset
   663
61471
9d4c08af61b8 support control symbol antiquotations;
wenzelm
parents: 61268
diff changeset
   664
fun read_cartouche syms =
9d4c08af61b8 support control symbol antiquotations;
wenzelm
parents: 61268
diff changeset
   665
  (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of
9d4c08af61b8 support control symbol antiquotations;
wenzelm
parents: 61268
diff changeset
   666
    SOME tok => tok
9d4c08af61b8 support control symbol antiquotations;
wenzelm
parents: 61268
diff changeset
   667
  | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms))));
9d4c08af61b8 support control symbol antiquotations;
wenzelm
parents: 61268
diff changeset
   668
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   669
end;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   670
30586
9674f64a0702 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm
parents: 30573
diff changeset
   671
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   672
(* explode *)
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   673
67497
3a0b08e7dfe9 clarified signature;
wenzelm
parents: 67495
diff changeset
   674
fun tokenize keywords strict syms =
3a0b08e7dfe9 clarified signature;
wenzelm
parents: 67495
diff changeset
   675
  Source.of_list syms |> make_source keywords strict |> Source.exhaust;
67495
90d760fa8f34 clarified operations;
wenzelm
parents: 67446
diff changeset
   676
90d760fa8f34 clarified operations;
wenzelm
parents: 67446
diff changeset
   677
fun explode keywords pos text =
67497
3a0b08e7dfe9 clarified signature;
wenzelm
parents: 67495
diff changeset
   678
  Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false};
67495
90d760fa8f34 clarified operations;
wenzelm
parents: 67446
diff changeset
   679
90d760fa8f34 clarified operations;
wenzelm
parents: 67446
diff changeset
   680
fun explode0 keywords = explode keywords Position.none;
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   681
88b0b1f28adc tuned signature;
wenzelm
parents: 59081
diff changeset
   682
63640
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   683
(* print name in parsable form *)
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   684
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   685
fun print_name keywords name =
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   686
  ((case explode keywords Position.none name of
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   687
    [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok))
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   688
  | _ => true) ? Symbol_Pos.quote_string_qq) name;
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   689
c273583f0203 print name in parsable form;
wenzelm
parents: 63019
diff changeset
   690
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   691
(* make *)
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   692
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   693
fun make ((k, n), s) pos =
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   694
  let
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 67652
diff changeset
   695
    val pos' = Position.advance_offsets n pos;
62797
e08c44eed27f tuned signature;
wenzelm
parents: 62782
diff changeset
   696
    val range = Position.range (pos, pos');
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   697
    val tok =
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   698
      if 0 <= k andalso k < Vector.length immediate_kinds then
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   699
        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
   700
      else
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   701
        (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
   702
          [tok] => tok
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   703
        | _ => 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
   704
  in (tok, pos') end;
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   705
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   706
fun make_string (s, pos) =
62799
wenzelm
parents: 62797
diff changeset
   707
  let
wenzelm
parents: 62797
diff changeset
   708
    val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none);
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62799
diff changeset
   709
    val pos' = Position.no_range_position pos;
62799
wenzelm
parents: 62797
diff changeset
   710
  in Token ((x, (pos', pos')), y, z) end;
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   711
63019
80ef19b51493 prefer internal attribute source;
wenzelm
parents: 62969
diff changeset
   712
val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int;
80ef19b51493 prefer internal attribute source;
wenzelm
parents: 62969
diff changeset
   713
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   714
fun make_src a args = make_string a :: args;
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   715
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 59083
diff changeset
   716
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   717
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   718
(** parsers **)
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   719
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   720
type 'a parser = T list -> 'a * T list;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   721
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
   722
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   723
67502
1be337a7584f clarified operations;
wenzelm
parents: 67501
diff changeset
   724
(* read body -- e.g. antiquotation source *)
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   725
67502
1be337a7584f clarified operations;
wenzelm
parents: 67501
diff changeset
   726
fun read_body keywords scan =
1be337a7584f clarified operations;
wenzelm
parents: 67501
diff changeset
   727
  tokenize (Keyword.no_command_keywords keywords) {strict = true}
1be337a7584f clarified operations;
wenzelm
parents: 67501
diff changeset
   728
  #> filter is_proper
67504
310114bec0d7 clarified signature;
wenzelm
parents: 67503
diff changeset
   729
  #> Scan.read stopper scan;
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   730
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58865
diff changeset
   731
fun read_antiq keywords scan (syms, pos) =
67502
1be337a7584f clarified operations;
wenzelm
parents: 67501
diff changeset
   732
  (case read_body keywords scan syms of
67504
310114bec0d7 clarified signature;
wenzelm
parents: 67503
diff changeset
   733
    SOME x => x
310114bec0d7 clarified signature;
wenzelm
parents: 67503
diff changeset
   734
  | NONE => error ("Malformed antiquotation" ^ Position.here pos));
58045
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   735
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   736
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   737
(* wrapped syntax *)
ab2483fad861 tuned signature;
wenzelm
parents: 58025
diff changeset
   738
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   739
fun syntax_generic scan src context =
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   740
  let
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   741
    val (name, pos) = name_of_src src;
64421
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   742
    val old_reports = maps reports_of_value src;
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   743
    val args1 = map init_assignable (args_of_src src);
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   744
    fun reported_text () =
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   745
      if Context_Position.is_visible_generic context then
64421
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   746
        let val new_reports = maps (reports_of_value o closure) args1 in
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   747
          if old_reports <> new_reports then
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   748
            map (fn (p, m) => Position.reported_text p m "") new_reports
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   749
          else []
681fae6b00b5 more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
wenzelm
parents: 63936
diff changeset
   750
        end
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   751
      else [];
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   752
  in
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   753
    (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
   754
      (SOME x, (context', [])) =>
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   755
        let val _ = Output.report (reported_text ())
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   756
        in (x, context') end
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   757
    | (_, (context', args2)) =>
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   758
        let
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   759
          val print_name =
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   760
            (case get_name (hd src) of
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   761
              NONE => quote name
61814
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   762
            | SOME {kind, print, ...} =>
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   763
                let
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   764
                  val ctxt' = Context.proof_of context';
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   765
                  val (markup, xname) = print ctxt';
1ca1142e1711 clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents: 61614
diff changeset
   766
                in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end);
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   767
          val print_args =
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   768
            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
   769
        in
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   770
          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
   771
            Markup.markup_report (implode (reported_text ())))
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   772
        end)
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   773
  end;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   774
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   775
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
   776
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   777
end;
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   778
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   779
type 'a parser = 'a Token.parser;
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57944
diff changeset
   780
type 'a context_parser = 'a Token.context_parser;