src/Pure/Isar/outer_syntax.ML
author wenzelm
Fri, 24 Aug 2012 12:35:39 +0200
changeset 48918 6e5fd4585512
parent 48864 3ee314ae1e0a
child 48992 0518bf89c777
permissions -rw-r--r--
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/outer_syntax.ML
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     3
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     4
The global Isabelle/Isar outer syntax.
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     5
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     6
Note: the syntax for files is statically determined at the very
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     7
beginning; for interactive processing it may change dynamically.
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     8
*)
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     9
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    10
signature OUTER_SYNTAX =
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    11
sig
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    12
  type outer_syntax
43712
3c2c912af2ef moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents: 43711
diff changeset
    13
  val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    14
  val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
46970
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
    15
  val check_syntax: unit -> unit
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 48638
diff changeset
    16
  type command_spec = (string * Keyword.T) * Position.T
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    17
  val command: command_spec -> string ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    18
    (Toplevel.transition -> Toplevel.transition) parser -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    19
  val markup_command: Thy_Output.markup -> command_spec -> string ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    20
    (Toplevel.transition -> Toplevel.transition) parser -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    21
  val improper_command: command_spec -> string ->
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    22
    (Toplevel.transition -> Toplevel.transition) parser -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    23
  val local_theory': command_spec -> string ->
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29315
diff changeset
    24
    (bool -> local_theory -> local_theory) parser -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    25
  val local_theory: command_spec -> string ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    26
    (local_theory -> local_theory) parser -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    27
  val local_theory_to_proof': command_spec -> string ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    28
    (bool -> local_theory -> Proof.state) parser -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    29
  val local_theory_to_proof: command_spec -> string ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    30
    (local_theory -> Proof.state) parser -> unit
5883
975c984526b0 tuned names;
wenzelm
parents: 5829
diff changeset
    31
  val print_outer_syntax: unit -> unit
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    32
  val scan: Position.T -> string -> Token.T list
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
    33
  val parse: Position.T -> string -> Toplevel.transition list
26600
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
    34
  type isar
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38236
diff changeset
    35
  val isar: TextIO.instream -> bool -> isar
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
    36
  val span_cmts: Token.T list -> Token.T list
46876
8f3bb485f628 refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents: 44736
diff changeset
    37
  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
44478
4fdb1009a370 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents: 44357
diff changeset
    38
  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
43712
3c2c912af2ef moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents: 43711
diff changeset
    39
    (Toplevel.transition * Toplevel.transition list) list
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    40
end;
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    41
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
    42
structure Outer_Syntax: OUTER_SYNTAX =
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    43
struct
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    44
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    45
(** outer syntax **)
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    46
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    47
(* command parsers *)
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    48
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    49
datatype command = Command of
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
    50
 {comment: string,
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
    51
  markup: Thy_Output.markup option,
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
    52
  int_only: bool,
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    53
  parse: (Toplevel.transition -> Toplevel.transition) parser,
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    54
  pos: Position.T,
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    55
  id: serial};
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    56
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    57
fun new_command comment markup int_only parse pos =
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    58
  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    59
    pos = pos, id = serial ()};
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    60
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    61
fun command_markup def (name, Command {pos, id, ...}) =
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    62
  Markup.properties (Position.entity_properties_of def id pos)
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
    63
    (Isabelle_Markup.entity Isabelle_Markup.commandN name);
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    64
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    65
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    66
(* parse command *)
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    67
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    68
local
6199
9b1be867e21a removed load;
wenzelm
parents: 6107
diff changeset
    69
14925
0f86a8a694f8 added read (provides transition names and sources);
wenzelm
parents: 14687
diff changeset
    70
fun terminate false = Scan.succeed ()
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 44187
diff changeset
    71
  | terminate true =
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 44187
diff changeset
    72
      Parse.group (fn () => "end of input")
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 44187
diff changeset
    73
        (Scan.option Parse.sync -- Parse.semicolon >> K ());
14925
0f86a8a694f8 added read (provides transition names and sources);
wenzelm
parents: 14687
diff changeset
    74
26620
722cf4fdd4dd eliminated unused trace, read;
wenzelm
parents: 26611
diff changeset
    75
fun body cmd (name, _) =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
    76
  (case cmd name of
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    77
    SOME (Command {int_only, parse, ...}) =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    78
      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
48191
c1def7433a72 internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
wenzelm
parents: 47416
diff changeset
    79
  | NONE =>
c1def7433a72 internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
wenzelm
parents: 47416
diff changeset
    80
      Scan.succeed (false, Toplevel.imperative (fn () =>
c1def7433a72 internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
wenzelm
parents: 47416
diff changeset
    81
        error ("Bad parser for outer syntax command " ^ quote name))));
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    82
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    83
in
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    84
26620
722cf4fdd4dd eliminated unused trace, read;
wenzelm
parents: 26611
diff changeset
    85
fun parse_command do_terminate cmd =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    86
  Parse.semicolon >> K NONE ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    87
  Parse.sync >> K NONE ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    88
  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    89
    >> (fn ((name, pos), (int_only, f)) =>
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15224
diff changeset
    90
      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    91
        Toplevel.interactive int_only |> f));
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    92
6199
9b1be867e21a removed load;
wenzelm
parents: 6107
diff changeset
    93
end;
9b1be867e21a removed load;
wenzelm
parents: 6107
diff changeset
    94
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    95
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    96
(* type outer_syntax *)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    97
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    98
datatype outer_syntax = Outer_Syntax of
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    99
 {commands: command Symtab.table,
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   100
  markups: (string * Thy_Output.markup) list};
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   101
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   102
fun make_outer_syntax commands markups =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   103
  Outer_Syntax {commands = commands, markups = markups};
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   104
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   105
val empty_outer_syntax = make_outer_syntax Symtab.empty [];
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   106
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   107
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   108
fun map_commands f (Outer_Syntax {commands, ...}) =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   109
  let
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   110
    val commands' = f commands;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   111
    val markups' =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   112
      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   113
        commands' [];
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   114
  in make_outer_syntax commands' markups' end;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   115
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   116
fun dest_commands (Outer_Syntax {commands, ...}) =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   117
  commands |> Symtab.dest |> sort_wrt #1
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   118
  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   119
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   120
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   121
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   122
fun is_markup (Outer_Syntax {markups, ...}) kind name =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   123
  AList.lookup (op =) markups name = SOME kind;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   124
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   125
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   126
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   127
(** global outer syntax **)
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   128
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 48638
diff changeset
   129
type command_spec = (string * Keyword.T) * Position.T;
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   130
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   131
local
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   132
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   133
(*synchronized wrt. Keywords*)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   134
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
5952
7d4ec8992b23 added commands;
wenzelm
parents: 5923
diff changeset
   135
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   136
fun add_command (name, kind) cmd = CRITICAL (fn () =>
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   137
  let
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   138
    val thy = ML_Context.the_global_context ();
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   139
    val Command {pos, ...} = cmd;
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   140
    val _ =
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   141
      (case try (Thy_Header.the_keyword thy) name of
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   142
        SOME spec =>
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48771
diff changeset
   143
          if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 48638
diff changeset
   144
          else error ("Inconsistent outer syntax keyword declaration " ^
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 48638
diff changeset
   145
            quote name ^ Position.str_of pos)
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   146
      | NONE =>
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   147
          if Context.theory_name thy = Context.PureN
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   148
          then Keyword.define (name, SOME kind)
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 48638
diff changeset
   149
          else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   150
    val _ = Position.report pos (command_markup true (name, cmd));
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   151
  in
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   152
    Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   153
     (if not (Symtab.defined commands name) then ()
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   154
      else warning ("Redefining outer syntax command " ^ quote name);
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   155
      Symtab.update (name, cmd) commands)))
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46876
diff changeset
   156
  end);
6722
5e82c7196789 added keyword classification;
wenzelm
parents: 6685
diff changeset
   157
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   158
in
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   159
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   160
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
7789
57d20133224e verbatim markup tokens;
wenzelm
parents: 7774
diff changeset
   161
46970
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   162
fun check_syntax () =
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   163
  let
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   164
    val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   165
  in
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   166
    (case subtract (op =) (map #1 (dest_commands syntax)) major of
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   167
      [] => ()
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   168
    | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   169
  end;
9667e0dcb5e2 check declared vs. defined commands at end of session;
wenzelm
parents: 46961
diff changeset
   170
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   171
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   172
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   173
fun command (spec, pos) comment parse =
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   174
  add_command spec (new_command comment NONE false parse pos);
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   175
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   176
fun markup_command markup (spec, pos) comment parse =
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   177
  add_command spec (new_command comment (SOME markup) false parse pos);
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   178
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   179
fun improper_command (spec, pos) comment parse =
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   180
  add_command spec (new_command comment NONE true parse pos);
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   181
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   182
end;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   183
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   184
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   185
(* local_theory commands *)
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   186
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   187
fun local_theory_command do_print trans command_spec comment parse =
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   188
  command command_spec comment (Parse.opt_target -- parse
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   189
    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   190
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29315
diff changeset
   191
val local_theory' = local_theory_command false Toplevel.local_theory';
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   192
val local_theory = local_theory_command false Toplevel.local_theory;
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   193
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   194
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   195
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   196
24872
7fd1aa6671a4 report on keyword/command declarations;
wenzelm
parents: 24868
diff changeset
   197
(* inspect syntax *)
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   198
9223
eb752c2fac22 removed help;
wenzelm
parents: 9213
diff changeset
   199
fun print_outer_syntax () =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   200
  let
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   201
    val ((keywords, _), outer_syntax) =
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   202
      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
   203
    fun pretty_cmd (name, comment, _) =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   204
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   205
    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   206
  in
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   207
    [Pretty.strs ("syntax keywords:" :: map quote keywords),
18326
2f57579e618f tuned msg;
wenzelm
parents: 18064
diff changeset
   208
      Pretty.big_list "commands:" (map pretty_cmd cmds),
2f57579e618f tuned msg;
wenzelm
parents: 18064
diff changeset
   209
      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
9223
eb752c2fac22 removed help;
wenzelm
parents: 9213
diff changeset
   210
    |> Pretty.chunks |> Pretty.writeln
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   211
  end;
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   212
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   213
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   214
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   215
(** toplevel parsing **)
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   216
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   217
(* basic sources *)
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
   218
26620
722cf4fdd4dd eliminated unused trace, read;
wenzelm
parents: 26611
diff changeset
   219
fun toplevel_source term do_recover cmd src =
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   220
  let
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   221
    val no_terminator =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   222
      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   223
    fun recover int =
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   224
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   225
  in
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   226
    src
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   227
    |> Token.source_proper
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   228
    |> Source.source Token.stopper
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
   229
      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   230
        (Option.map recover do_recover)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19060
diff changeset
   231
    |> Source.map_filter I
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   232
    |> Source.source Token.stopper
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
   233
        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   234
        (Option.map recover do_recover)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19060
diff changeset
   235
    |> Source.map_filter I
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   236
  end;
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   237
7746
b52c1a632e6a simplified;
wenzelm
parents: 7735
diff changeset
   238
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   239
(* off-line scanning/parsing *)
14925
0f86a8a694f8 added read (provides transition names and sources);
wenzelm
parents: 14687
diff changeset
   240
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   241
fun scan pos str =
16195
wenzelm
parents: 15989
diff changeset
   242
  Source.of_string str
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38422
diff changeset
   243
  |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   244
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
16195
wenzelm
parents: 15989
diff changeset
   245
  |> Source.exhaust;
wenzelm
parents: 15989
diff changeset
   246
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   247
fun parse pos str =
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   248
  Source.of_string str
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38422
diff changeset
   249
  |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   250
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   251
  |> toplevel_source false NONE lookup_commands_dynamic
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   252
  |> Source.exhaust;
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   253
14091
ad6ba9c55190 A patch by david aspinall
nipkow
parents: 12943
diff changeset
   254
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   255
(* interactive source of toplevel transformers *)
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   256
26600
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
   257
type isar =
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
   258
  (Toplevel.transition, (Toplevel.transition option,
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   259
    (Token.T, (Token.T option, (Token.T, (Token.T,
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30513
diff changeset
   260
      (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
27770
10d84e124a2f updated type of nested sources;
wenzelm
parents: 27720
diff changeset
   261
  Source.source) Source.source) Source.source) Source.source)
10d84e124a2f updated type of nested sources;
wenzelm
parents: 27720
diff changeset
   262
  Source.source) Source.source) Source.source) Source.source;
26600
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
   263
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38236
diff changeset
   264
fun isar in_stream term : isar =
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38236
diff changeset
   265
  Source.tty in_stream
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38422
diff changeset
   266
  |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   267
  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   268
  |> toplevel_source term (SOME true) lookup_commands_dynamic;
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   269
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   270
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   271
(* side-comments *)
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   272
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   273
local
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   274
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   275
fun cmts (t1 :: t2 :: toks) =
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   276
      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   277
      else cmts (t2 :: toks)
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   278
  | cmts toks = [];
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   279
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   280
in
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   281
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   282
val span_cmts = filter Token.is_proper #> cmts;
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   283
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   284
end;
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   285
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 48864
diff changeset
   286
44478
4fdb1009a370 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents: 44357
diff changeset
   287
(* read toplevel commands -- fail-safe *)
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   288
44658
5bec9c15ef29 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents: 44478
diff changeset
   289
fun read_span outer_syntax toks =
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   290
  let
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   291
    val commands = lookup_commands outer_syntax;
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   292
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48768
diff changeset
   293
    val proper_range = Position.set_range (Command.proper_range toks);
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   294
    val pos =
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   295
      (case find_first Token.is_command toks of
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   296
        SOME tok => Token.position_of tok
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48768
diff changeset
   297
      | NONE => proper_range);
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   298
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   299
    fun command_reports tok =
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   300
      if Token.is_command tok then
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   301
        let val name = Token.content_of tok in
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   302
          (case commands name of
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   303
            NONE => []
48768
abc45de5bb22 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents: 48749
diff changeset
   304
          | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
48647
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   305
        end
a5144c4c26a2 report commands as formal entities, with def/ref positions;
wenzelm
parents: 48646
diff changeset
   306
      else [];
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   307
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   308
    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
48768
abc45de5bb22 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents: 48749
diff changeset
   309
    val _ = Position.reports_text (token_reports @ maps command_reports toks);
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   310
  in
48749
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   311
    if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   312
    else
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   313
      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   314
        [tr] =>
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   315
          if Keyword.is_control (Toplevel.name_of tr) then
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   316
            (Toplevel.malformed pos "Illegal control command", true)
c197b3c3e7fa some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
wenzelm
parents: 48647
diff changeset
   317
          else (tr, true)
48771
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48768
diff changeset
   318
      | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48768
diff changeset
   319
      | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
2ea997196d04 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents: 48768
diff changeset
   320
      handle ERROR msg => (Toplevel.malformed proper_range msg, true)
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   321
  end;
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   322
44478
4fdb1009a370 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents: 44357
diff changeset
   323
fun read_element outer_syntax init {head, proof, proper_proof} =
28436
4faf705a177d load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents: 28432
diff changeset
   324
  let
44658
5bec9c15ef29 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents: 44478
diff changeset
   325
    val read = read_span outer_syntax o Thy_Syntax.span_content;
5bec9c15ef29 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents: 44478
diff changeset
   326
    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
5bec9c15ef29 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
wenzelm
parents: 44478
diff changeset
   327
    val proof_trs = map read proof |> filter #2 |> map #1;
28436
4faf705a177d load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents: 28432
diff changeset
   328
  in
47416
df8fc0567a3d static relevance of proof via syntax keywords;
wenzelm
parents: 47014
diff changeset
   329
    if proper_head andalso proper_proof andalso
df8fc0567a3d static relevance of proof via syntax keywords;
wenzelm
parents: 47014
diff changeset
   330
      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 42129
diff changeset
   331
    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
28436
4faf705a177d load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents: 28432
diff changeset
   332
  end;
28432
944cb67f809a load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents: 28424
diff changeset
   333
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   334
end;
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
   335