src/Pure/Isar/outer_syntax.ML
author wenzelm
Tue May 20 20:05:43 2014 +0200 (2014-05-20)
changeset 57026 90a3e39be0ca
parent 56938 ef44b488bad8
child 57105 bf5ddf4ec64b
permissions -rw-r--r--
afford strict check (see also AFP/a8e08d947f0a);
wenzelm@5829
     1
(*  Title:      Pure/Isar/outer_syntax.ML
wenzelm@5829
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5829
     3
wenzelm@27353
     4
The global Isabelle/Isar outer syntax.
wenzelm@27353
     5
wenzelm@27353
     6
Note: the syntax for files is statically determined at the very
wenzelm@27353
     7
beginning; for interactive processing it may change dynamically.
wenzelm@5829
     8
*)
wenzelm@5829
     9
wenzelm@5829
    10
signature OUTER_SYNTAX =
wenzelm@5829
    11
sig
wenzelm@43711
    12
  type outer_syntax
wenzelm@55448
    13
  val batch_mode: bool Unsynchronized.ref
wenzelm@43712
    14
  val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
wenzelm@43711
    15
  val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
wenzelm@46970
    16
  val check_syntax: unit -> unit
wenzelm@48646
    17
  type command_spec = (string * Keyword.T) * Position.T
wenzelm@46961
    18
  val command: command_spec -> string ->
wenzelm@29311
    19
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@46961
    20
  val markup_command: Thy_Output.markup -> command_spec -> string ->
wenzelm@29311
    21
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@46961
    22
  val improper_command: command_spec -> string ->
wenzelm@43711
    23
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@46961
    24
  val local_theory': command_spec -> string ->
wenzelm@29380
    25
    (bool -> local_theory -> local_theory) parser -> unit
wenzelm@46961
    26
  val local_theory: command_spec -> string ->
wenzelm@29311
    27
    (local_theory -> local_theory) parser -> unit
wenzelm@46961
    28
  val local_theory_to_proof': command_spec -> string ->
wenzelm@29311
    29
    (bool -> local_theory -> Proof.state) parser -> unit
wenzelm@46961
    30
  val local_theory_to_proof: command_spec -> string ->
wenzelm@29311
    31
    (local_theory -> Proof.state) parser -> unit
wenzelm@50213
    32
  val help_outer_syntax: string list -> unit
wenzelm@5883
    33
  val print_outer_syntax: unit -> unit
wenzelm@36959
    34
  val scan: Position.T -> string -> Token.T list
wenzelm@25580
    35
  val parse: Position.T -> string -> Toplevel.transition list
wenzelm@26600
    36
  type isar
wenzelm@38253
    37
  val isar: TextIO.instream -> bool -> isar
wenzelm@52510
    38
  val side_comments: Token.T list -> Token.T list
wenzelm@52510
    39
  val command_reports: outer_syntax -> Token.T -> (Position.report * string) list
wenzelm@52510
    40
  val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
wenzelm@5829
    41
end;
wenzelm@5829
    42
wenzelm@36953
    43
structure Outer_Syntax: OUTER_SYNTAX =
wenzelm@5829
    44
struct
wenzelm@5829
    45
wenzelm@5829
    46
(** outer syntax **)
wenzelm@5829
    47
wenzelm@29311
    48
(* command parsers *)
wenzelm@5829
    49
wenzelm@29311
    50
datatype command = Command of
wenzelm@24868
    51
 {comment: string,
wenzelm@37216
    52
  markup: Thy_Output.markup option,
wenzelm@24868
    53
  int_only: bool,
wenzelm@48647
    54
  parse: (Toplevel.transition -> Toplevel.transition) parser,
wenzelm@48647
    55
  pos: Position.T,
wenzelm@48647
    56
  id: serial};
wenzelm@5829
    57
wenzelm@48647
    58
fun new_command comment markup int_only parse pos =
wenzelm@48647
    59
  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
wenzelm@48647
    60
    pos = pos, id = serial ()};
wenzelm@48647
    61
wenzelm@48647
    62
fun command_markup def (name, Command {pos, id, ...}) =
wenzelm@48647
    63
  Markup.properties (Position.entity_properties_of def id pos)
wenzelm@50201
    64
    (Markup.entity Markup.commandN name);
wenzelm@5829
    65
wenzelm@50213
    66
fun pretty_command (cmd as (name, Command {comment, ...})) =
wenzelm@50213
    67
  Pretty.block
wenzelm@50213
    68
    (Pretty.marks_str
wenzelm@50450
    69
      ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
wenzelm@50215
    70
        command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
wenzelm@50213
    71
wenzelm@5829
    72
wenzelm@5829
    73
(* parse command *)
wenzelm@5829
    74
wenzelm@6860
    75
local
wenzelm@6199
    76
wenzelm@14925
    77
fun terminate false = Scan.succeed ()
wenzelm@44357
    78
  | terminate true =
wenzelm@44357
    79
      Parse.group (fn () => "end of input")
wenzelm@44357
    80
        (Scan.option Parse.sync -- Parse.semicolon >> K ());
wenzelm@14925
    81
wenzelm@26620
    82
fun body cmd (name, _) =
wenzelm@7026
    83
  (case cmd name of
wenzelm@29311
    84
    SOME (Command {int_only, parse, ...}) =>
wenzelm@36950
    85
      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
wenzelm@48191
    86
  | NONE =>
wenzelm@48191
    87
      Scan.succeed (false, Toplevel.imperative (fn () =>
wenzelm@48191
    88
        error ("Bad parser for outer syntax command " ^ quote name))));
wenzelm@6860
    89
wenzelm@6860
    90
in
wenzelm@5829
    91
wenzelm@26620
    92
fun parse_command do_terminate cmd =
wenzelm@36950
    93
  Parse.semicolon >> K NONE ||
wenzelm@36950
    94
  Parse.sync >> K NONE ||
wenzelm@36950
    95
  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
wenzelm@6860
    96
    >> (fn ((name, pos), (int_only, f)) =>
skalberg@15531
    97
      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
wenzelm@6860
    98
        Toplevel.interactive int_only |> f));
wenzelm@5829
    99
wenzelm@6199
   100
end;
wenzelm@6199
   101
wenzelm@5829
   102
wenzelm@43711
   103
(* type outer_syntax *)
wenzelm@43711
   104
wenzelm@43711
   105
datatype outer_syntax = Outer_Syntax of
wenzelm@43711
   106
 {commands: command Symtab.table,
wenzelm@43711
   107
  markups: (string * Thy_Output.markup) list};
wenzelm@43711
   108
wenzelm@43711
   109
fun make_outer_syntax commands markups =
wenzelm@43711
   110
  Outer_Syntax {commands = commands, markups = markups};
wenzelm@43711
   111
wenzelm@43711
   112
val empty_outer_syntax = make_outer_syntax Symtab.empty [];
wenzelm@43711
   113
wenzelm@43711
   114
wenzelm@43711
   115
fun map_commands f (Outer_Syntax {commands, ...}) =
wenzelm@43711
   116
  let
wenzelm@43711
   117
    val commands' = f commands;
wenzelm@43711
   118
    val markups' =
wenzelm@43711
   119
      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
wenzelm@43711
   120
        commands' [];
wenzelm@43711
   121
  in make_outer_syntax commands' markups' end;
wenzelm@43711
   122
wenzelm@43711
   123
fun dest_commands (Outer_Syntax {commands, ...}) =
wenzelm@50213
   124
  commands |> Symtab.dest |> sort_wrt #1;
wenzelm@43711
   125
wenzelm@43711
   126
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
wenzelm@43711
   127
wenzelm@43711
   128
fun is_markup (Outer_Syntax {markups, ...}) kind name =
wenzelm@43711
   129
  AList.lookup (op =) markups name = SOME kind;
wenzelm@43711
   130
wenzelm@43711
   131
wenzelm@5829
   132
wenzelm@9132
   133
(** global outer syntax **)
wenzelm@5829
   134
wenzelm@48646
   135
type command_spec = (string * Keyword.T) * Position.T;
wenzelm@46961
   136
wenzelm@55448
   137
val batch_mode = Unsynchronized.ref false;
wenzelm@55448
   138
wenzelm@7026
   139
local
wenzelm@7026
   140
wenzelm@43711
   141
(*synchronized wrt. Keywords*)
wenzelm@43711
   142
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
wenzelm@5952
   143
wenzelm@48647
   144
fun add_command (name, kind) cmd = CRITICAL (fn () =>
wenzelm@46950
   145
  let
wenzelm@56294
   146
    val context = ML_Context.the_generic_context ();
wenzelm@56294
   147
    val thy = Context.theory_of context;
wenzelm@48647
   148
    val Command {pos, ...} = cmd;
wenzelm@46950
   149
    val _ =
wenzelm@46950
   150
      (case try (Thy_Header.the_keyword thy) name of
wenzelm@46961
   151
        SOME spec =>
wenzelm@48864
   152
          if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
wenzelm@48646
   153
          else error ("Inconsistent outer syntax keyword declaration " ^
wenzelm@48992
   154
            quote name ^ Position.here pos)
wenzelm@46950
   155
      | NONE =>
wenzelm@46961
   156
          if Context.theory_name thy = Context.PureN
wenzelm@46961
   157
          then Keyword.define (name, SOME kind)
wenzelm@48992
   158
          else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
wenzelm@56294
   159
    val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
wenzelm@46950
   160
  in
wenzelm@46950
   161
    Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
wenzelm@46950
   162
     (if not (Symtab.defined commands name) then ()
wenzelm@57026
   163
      else if ! batch_mode then
wenzelm@57026
   164
        error ("Attempt to redefine outer syntax command " ^ quote name)
wenzelm@55448
   165
      else
wenzelm@57026
   166
        warning ("Redefining outer syntax command " ^ quote name ^
wenzelm@57026
   167
          Position.here (Position.thread_data ()));
wenzelm@46950
   168
      Symtab.update (name, cmd) commands)))
wenzelm@46950
   169
  end);
wenzelm@6722
   170
wenzelm@7026
   171
in
wenzelm@7026
   172
wenzelm@43711
   173
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
wenzelm@7789
   174
wenzelm@46970
   175
fun check_syntax () =
wenzelm@46970
   176
  let
wenzelm@46970
   177
    val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
wenzelm@46970
   178
  in
wenzelm@46970
   179
    (case subtract (op =) (map #1 (dest_commands syntax)) major of
wenzelm@46970
   180
      [] => ()
wenzelm@46970
   181
    | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
wenzelm@46970
   182
  end;
wenzelm@46970
   183
wenzelm@43711
   184
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
wenzelm@5829
   185
wenzelm@48647
   186
fun command (spec, pos) comment parse =
wenzelm@48647
   187
  add_command spec (new_command comment NONE false parse pos);
wenzelm@24868
   188
wenzelm@48647
   189
fun markup_command markup (spec, pos) comment parse =
wenzelm@48647
   190
  add_command spec (new_command comment (SOME markup) false parse pos);
wenzelm@7026
   191
wenzelm@48647
   192
fun improper_command (spec, pos) comment parse =
wenzelm@48647
   193
  add_command spec (new_command comment NONE true parse pos);
wenzelm@29311
   194
wenzelm@43711
   195
end;
wenzelm@43711
   196
wenzelm@5829
   197
wenzelm@26990
   198
(* local_theory commands *)
wenzelm@26990
   199
wenzelm@56895
   200
fun local_theory_command trans command_spec comment parse =
wenzelm@56895
   201
  command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
wenzelm@26990
   202
wenzelm@56895
   203
val local_theory' = local_theory_command Toplevel.local_theory';
wenzelm@56895
   204
val local_theory = local_theory_command Toplevel.local_theory;
wenzelm@56895
   205
val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
wenzelm@56895
   206
val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
wenzelm@26990
   207
wenzelm@26990
   208
wenzelm@24872
   209
(* inspect syntax *)
wenzelm@7026
   210
wenzelm@50213
   211
fun help_outer_syntax pats =
wenzelm@50213
   212
  dest_commands (#2 (get_syntax ()))
wenzelm@50213
   213
  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
wenzelm@50213
   214
  |> map pretty_command
wenzelm@56334
   215
  |> Pretty.writeln_chunks;
wenzelm@50213
   216
wenzelm@9223
   217
fun print_outer_syntax () =
wenzelm@7026
   218
  let
wenzelm@46957
   219
    val ((keywords, _), outer_syntax) =
wenzelm@46957
   220
      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
wenzelm@50213
   221
    val (int_cmds, cmds) =
wenzelm@50213
   222
      List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands outer_syntax);
wenzelm@7026
   223
  in
wenzelm@43711
   224
    [Pretty.strs ("syntax keywords:" :: map quote keywords),
wenzelm@50213
   225
      Pretty.big_list "commands:" (map pretty_command cmds),
wenzelm@50213
   226
      Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
wenzelm@56334
   227
    |> Pretty.writeln_chunks
wenzelm@7026
   228
  end;
wenzelm@5829
   229
wenzelm@5829
   230
wenzelm@5829
   231
wenzelm@9132
   232
(** toplevel parsing **)
wenzelm@5829
   233
wenzelm@9132
   234
(* basic sources *)
wenzelm@6860
   235
wenzelm@26620
   236
fun toplevel_source term do_recover cmd src =
wenzelm@9132
   237
  let
wenzelm@9132
   238
    val no_terminator =
wenzelm@36959
   239
      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
wenzelm@23682
   240
    fun recover int =
wenzelm@23682
   241
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
wenzelm@9132
   242
  in
wenzelm@9132
   243
    src
wenzelm@36959
   244
    |> Token.source_proper
wenzelm@36959
   245
    |> Source.source Token.stopper
wenzelm@51627
   246
      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.document_source >> K NONE || Parse.not_eof >> SOME))
wenzelm@23682
   247
        (Option.map recover do_recover)
wenzelm@19482
   248
    |> Source.map_filter I
wenzelm@36959
   249
    |> Source.source Token.stopper
wenzelm@36950
   250
        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
wenzelm@23682
   251
        (Option.map recover do_recover)
wenzelm@19482
   252
    |> Source.map_filter I
wenzelm@9132
   253
  end;
wenzelm@5829
   254
wenzelm@7746
   255
wenzelm@25580
   256
(* off-line scanning/parsing *)
wenzelm@14925
   257
wenzelm@27839
   258
fun scan pos str =
wenzelm@16195
   259
  Source.of_string str
wenzelm@40523
   260
  |> Symbol.source
wenzelm@36959
   261
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
wenzelm@16195
   262
  |> Source.exhaust;
wenzelm@16195
   263
wenzelm@25580
   264
fun parse pos str =
wenzelm@25580
   265
  Source.of_string str
wenzelm@40523
   266
  |> Symbol.source
wenzelm@36959
   267
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
wenzelm@43711
   268
  |> toplevel_source false NONE lookup_commands_dynamic
wenzelm@25580
   269
  |> Source.exhaust;
wenzelm@25580
   270
nipkow@14091
   271
wenzelm@24868
   272
(* interactive source of toplevel transformers *)
wenzelm@24868
   273
wenzelm@26600
   274
type isar =
wenzelm@26600
   275
  (Toplevel.transition, (Toplevel.transition option,
wenzelm@36959
   276
    (Token.T, (Token.T option, (Token.T, (Token.T,
wenzelm@54734
   277
      (Symbol_Pos.T,
wenzelm@54734
   278
        Position.T * (Symbol.symbol, (Symbol.symbol, (string, unit) Source.source) Source.source)
wenzelm@27770
   279
  Source.source) Source.source) Source.source) Source.source)
wenzelm@27770
   280
  Source.source) Source.source) Source.source) Source.source;
wenzelm@26600
   281
wenzelm@38253
   282
fun isar in_stream term : isar =
wenzelm@38253
   283
  Source.tty in_stream
wenzelm@40523
   284
  |> Symbol.source
wenzelm@56203
   285
  |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s)  (*Proof General legacy*)
wenzelm@36959
   286
  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
wenzelm@43711
   287
  |> toplevel_source term (SOME true) lookup_commands_dynamic;
wenzelm@24868
   288
wenzelm@24868
   289
wenzelm@52510
   290
(* side-comments *)
wenzelm@48749
   291
wenzelm@52510
   292
fun cmts (t1 :: t2 :: toks) =
wenzelm@52510
   293
      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
wenzelm@52510
   294
      else cmts (t2 :: toks)
wenzelm@52510
   295
  | cmts _ = [];
wenzelm@52510
   296
wenzelm@52510
   297
val side_comments = filter Token.is_proper #> cmts;
wenzelm@52510
   298
wenzelm@52510
   299
wenzelm@52510
   300
(* read commands *)
wenzelm@48647
   301
wenzelm@52510
   302
fun command_reports outer_syntax tok =
wenzelm@52510
   303
  if Token.is_command tok then
wenzelm@52510
   304
    let val name = Token.content_of tok in
wenzelm@52510
   305
      (case lookup_commands outer_syntax name of
wenzelm@52510
   306
        NONE => []
wenzelm@55708
   307
      | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
wenzelm@52510
   308
    end
wenzelm@52510
   309
  else [];
wenzelm@48749
   310
wenzelm@52510
   311
fun read_spans outer_syntax toks =
wenzelm@52510
   312
  Source.of_list toks
wenzelm@52510
   313
  |> toplevel_source false NONE (K (lookup_commands outer_syntax))
wenzelm@52510
   314
  |> Source.exhaust;
wenzelm@28432
   315
wenzelm@5829
   316
end;
wenzelm@36953
   317