src/Pure/Isar/outer_syntax.ML
author wenzelm
Fri Aug 24 12:35:39 2012 +0200 (2012-08-24 ago)
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);
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@43712
    13
  val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
wenzelm@43711
    14
  val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
wenzelm@46970
    15
  val check_syntax: unit -> unit
wenzelm@48646
    16
  type command_spec = (string * Keyword.T) * Position.T
wenzelm@46961
    17
  val command: command_spec -> string ->
wenzelm@29311
    18
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@46961
    19
  val markup_command: Thy_Output.markup -> command_spec -> string ->
wenzelm@29311
    20
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@46961
    21
  val improper_command: command_spec -> string ->
wenzelm@43711
    22
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@46961
    23
  val local_theory': command_spec -> string ->
wenzelm@29380
    24
    (bool -> local_theory -> local_theory) parser -> unit
wenzelm@46961
    25
  val local_theory: command_spec -> string ->
wenzelm@29311
    26
    (local_theory -> local_theory) parser -> unit
wenzelm@46961
    27
  val local_theory_to_proof': command_spec -> string ->
wenzelm@29311
    28
    (bool -> local_theory -> Proof.state) parser -> unit
wenzelm@46961
    29
  val local_theory_to_proof: command_spec -> string ->
wenzelm@29311
    30
    (local_theory -> Proof.state) parser -> unit
wenzelm@5883
    31
  val print_outer_syntax: unit -> unit
wenzelm@36959
    32
  val scan: Position.T -> string -> Token.T list
wenzelm@25580
    33
  val parse: Position.T -> string -> Toplevel.transition list
wenzelm@26600
    34
  type isar
wenzelm@38253
    35
  val isar: TextIO.instream -> bool -> isar
wenzelm@48918
    36
  val span_cmts: Token.T list -> Token.T list
wenzelm@46876
    37
  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
wenzelm@44478
    38
  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
wenzelm@43712
    39
    (Toplevel.transition * Toplevel.transition list) list
wenzelm@5829
    40
end;
wenzelm@5829
    41
wenzelm@36953
    42
structure Outer_Syntax: OUTER_SYNTAX =
wenzelm@5829
    43
struct
wenzelm@5829
    44
wenzelm@5829
    45
(** outer syntax **)
wenzelm@5829
    46
wenzelm@29311
    47
(* command parsers *)
wenzelm@5829
    48
wenzelm@29311
    49
datatype command = Command of
wenzelm@24868
    50
 {comment: string,
wenzelm@37216
    51
  markup: Thy_Output.markup option,
wenzelm@24868
    52
  int_only: bool,
wenzelm@48647
    53
  parse: (Toplevel.transition -> Toplevel.transition) parser,
wenzelm@48647
    54
  pos: Position.T,
wenzelm@48647
    55
  id: serial};
wenzelm@5829
    56
wenzelm@48647
    57
fun new_command comment markup int_only parse pos =
wenzelm@48647
    58
  Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
wenzelm@48647
    59
    pos = pos, id = serial ()};
wenzelm@48647
    60
wenzelm@48647
    61
fun command_markup def (name, Command {pos, id, ...}) =
wenzelm@48647
    62
  Markup.properties (Position.entity_properties_of def id pos)
wenzelm@48647
    63
    (Isabelle_Markup.entity Isabelle_Markup.commandN name);
wenzelm@5829
    64
wenzelm@5829
    65
wenzelm@5829
    66
(* parse command *)
wenzelm@5829
    67
wenzelm@6860
    68
local
wenzelm@6199
    69
wenzelm@14925
    70
fun terminate false = Scan.succeed ()
wenzelm@44357
    71
  | terminate true =
wenzelm@44357
    72
      Parse.group (fn () => "end of input")
wenzelm@44357
    73
        (Scan.option Parse.sync -- Parse.semicolon >> K ());
wenzelm@14925
    74
wenzelm@26620
    75
fun body cmd (name, _) =
wenzelm@7026
    76
  (case cmd name of
wenzelm@29311
    77
    SOME (Command {int_only, parse, ...}) =>
wenzelm@36950
    78
      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
wenzelm@48191
    79
  | NONE =>
wenzelm@48191
    80
      Scan.succeed (false, Toplevel.imperative (fn () =>
wenzelm@48191
    81
        error ("Bad parser for outer syntax command " ^ quote name))));
wenzelm@6860
    82
wenzelm@6860
    83
in
wenzelm@5829
    84
wenzelm@26620
    85
fun parse_command do_terminate cmd =
wenzelm@36950
    86
  Parse.semicolon >> K NONE ||
wenzelm@36950
    87
  Parse.sync >> K NONE ||
wenzelm@36950
    88
  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
wenzelm@6860
    89
    >> (fn ((name, pos), (int_only, f)) =>
skalberg@15531
    90
      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
wenzelm@6860
    91
        Toplevel.interactive int_only |> f));
wenzelm@5829
    92
wenzelm@6199
    93
end;
wenzelm@6199
    94
wenzelm@5829
    95
wenzelm@43711
    96
(* type outer_syntax *)
wenzelm@43711
    97
wenzelm@43711
    98
datatype outer_syntax = Outer_Syntax of
wenzelm@43711
    99
 {commands: command Symtab.table,
wenzelm@43711
   100
  markups: (string * Thy_Output.markup) list};
wenzelm@43711
   101
wenzelm@43711
   102
fun make_outer_syntax commands markups =
wenzelm@43711
   103
  Outer_Syntax {commands = commands, markups = markups};
wenzelm@43711
   104
wenzelm@43711
   105
val empty_outer_syntax = make_outer_syntax Symtab.empty [];
wenzelm@43711
   106
wenzelm@43711
   107
wenzelm@43711
   108
fun map_commands f (Outer_Syntax {commands, ...}) =
wenzelm@43711
   109
  let
wenzelm@43711
   110
    val commands' = f commands;
wenzelm@43711
   111
    val markups' =
wenzelm@43711
   112
      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
wenzelm@43711
   113
        commands' [];
wenzelm@43711
   114
  in make_outer_syntax commands' markups' end;
wenzelm@43711
   115
wenzelm@43711
   116
fun dest_commands (Outer_Syntax {commands, ...}) =
wenzelm@43711
   117
  commands |> Symtab.dest |> sort_wrt #1
wenzelm@43711
   118
  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
wenzelm@43711
   119
wenzelm@43711
   120
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
wenzelm@43711
   121
wenzelm@43711
   122
fun is_markup (Outer_Syntax {markups, ...}) kind name =
wenzelm@43711
   123
  AList.lookup (op =) markups name = SOME kind;
wenzelm@43711
   124
wenzelm@43711
   125
wenzelm@5829
   126
wenzelm@9132
   127
(** global outer syntax **)
wenzelm@5829
   128
wenzelm@48646
   129
type command_spec = (string * Keyword.T) * Position.T;
wenzelm@46961
   130
wenzelm@7026
   131
local
wenzelm@7026
   132
wenzelm@43711
   133
(*synchronized wrt. Keywords*)
wenzelm@43711
   134
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
wenzelm@5952
   135
wenzelm@48647
   136
fun add_command (name, kind) cmd = CRITICAL (fn () =>
wenzelm@46950
   137
  let
wenzelm@46950
   138
    val thy = ML_Context.the_global_context ();
wenzelm@48647
   139
    val Command {pos, ...} = cmd;
wenzelm@46950
   140
    val _ =
wenzelm@46950
   141
      (case try (Thy_Header.the_keyword thy) name of
wenzelm@46961
   142
        SOME spec =>
wenzelm@48864
   143
          if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
wenzelm@48646
   144
          else error ("Inconsistent outer syntax keyword declaration " ^
wenzelm@48646
   145
            quote name ^ Position.str_of pos)
wenzelm@46950
   146
      | NONE =>
wenzelm@46961
   147
          if Context.theory_name thy = Context.PureN
wenzelm@46961
   148
          then Keyword.define (name, SOME kind)
wenzelm@48646
   149
          else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
wenzelm@48647
   150
    val _ = Position.report pos (command_markup true (name, cmd));
wenzelm@46950
   151
  in
wenzelm@46950
   152
    Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
wenzelm@46950
   153
     (if not (Symtab.defined commands name) then ()
wenzelm@46950
   154
      else warning ("Redefining outer syntax command " ^ quote name);
wenzelm@46950
   155
      Symtab.update (name, cmd) commands)))
wenzelm@46950
   156
  end);
wenzelm@6722
   157
wenzelm@7026
   158
in
wenzelm@7026
   159
wenzelm@43711
   160
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
wenzelm@7789
   161
wenzelm@46970
   162
fun check_syntax () =
wenzelm@46970
   163
  let
wenzelm@46970
   164
    val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
wenzelm@46970
   165
  in
wenzelm@46970
   166
    (case subtract (op =) (map #1 (dest_commands syntax)) major of
wenzelm@46970
   167
      [] => ()
wenzelm@46970
   168
    | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
wenzelm@46970
   169
  end;
wenzelm@46970
   170
wenzelm@43711
   171
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
wenzelm@5829
   172
wenzelm@48647
   173
fun command (spec, pos) comment parse =
wenzelm@48647
   174
  add_command spec (new_command comment NONE false parse pos);
wenzelm@24868
   175
wenzelm@48647
   176
fun markup_command markup (spec, pos) comment parse =
wenzelm@48647
   177
  add_command spec (new_command comment (SOME markup) false parse pos);
wenzelm@7026
   178
wenzelm@48647
   179
fun improper_command (spec, pos) comment parse =
wenzelm@48647
   180
  add_command spec (new_command comment NONE true parse pos);
wenzelm@29311
   181
wenzelm@43711
   182
end;
wenzelm@43711
   183
wenzelm@5829
   184
wenzelm@26990
   185
(* local_theory commands *)
wenzelm@26990
   186
wenzelm@46961
   187
fun local_theory_command do_print trans command_spec comment parse =
wenzelm@46961
   188
  command command_spec comment (Parse.opt_target -- parse
wenzelm@26990
   189
    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
wenzelm@26990
   190
wenzelm@29380
   191
val local_theory' = local_theory_command false Toplevel.local_theory';
wenzelm@29311
   192
val local_theory = local_theory_command false Toplevel.local_theory;
wenzelm@26990
   193
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
wenzelm@29311
   194
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
wenzelm@26990
   195
wenzelm@26990
   196
wenzelm@24872
   197
(* inspect syntax *)
wenzelm@7026
   198
wenzelm@9223
   199
fun print_outer_syntax () =
wenzelm@7026
   200
  let
wenzelm@46957
   201
    val ((keywords, _), outer_syntax) =
wenzelm@46957
   202
      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
wenzelm@27353
   203
    fun pretty_cmd (name, comment, _) =
wenzelm@7026
   204
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
wenzelm@43711
   205
    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
wenzelm@7026
   206
  in
wenzelm@43711
   207
    [Pretty.strs ("syntax keywords:" :: map quote keywords),
wenzelm@18326
   208
      Pretty.big_list "commands:" (map pretty_cmd cmds),
wenzelm@18326
   209
      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
wenzelm@9223
   210
    |> Pretty.chunks |> Pretty.writeln
wenzelm@7026
   211
  end;
wenzelm@5829
   212
wenzelm@5829
   213
wenzelm@5829
   214
wenzelm@9132
   215
(** toplevel parsing **)
wenzelm@5829
   216
wenzelm@9132
   217
(* basic sources *)
wenzelm@6860
   218
wenzelm@26620
   219
fun toplevel_source term do_recover cmd src =
wenzelm@9132
   220
  let
wenzelm@9132
   221
    val no_terminator =
wenzelm@36959
   222
      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
wenzelm@23682
   223
    fun recover int =
wenzelm@23682
   224
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
wenzelm@9132
   225
  in
wenzelm@9132
   226
    src
wenzelm@36959
   227
    |> Token.source_proper
wenzelm@36959
   228
    |> Source.source Token.stopper
wenzelm@36950
   229
      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
wenzelm@23682
   230
        (Option.map recover do_recover)
wenzelm@19482
   231
    |> Source.map_filter I
wenzelm@36959
   232
    |> Source.source Token.stopper
wenzelm@36950
   233
        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
wenzelm@23682
   234
        (Option.map recover do_recover)
wenzelm@19482
   235
    |> Source.map_filter I
wenzelm@9132
   236
  end;
wenzelm@5829
   237
wenzelm@7746
   238
wenzelm@25580
   239
(* off-line scanning/parsing *)
wenzelm@14925
   240
wenzelm@27839
   241
fun scan pos str =
wenzelm@16195
   242
  Source.of_string str
wenzelm@40523
   243
  |> Symbol.source
wenzelm@36959
   244
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
wenzelm@16195
   245
  |> Source.exhaust;
wenzelm@16195
   246
wenzelm@25580
   247
fun parse pos str =
wenzelm@25580
   248
  Source.of_string str
wenzelm@40523
   249
  |> Symbol.source
wenzelm@36959
   250
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
wenzelm@43711
   251
  |> toplevel_source false NONE lookup_commands_dynamic
wenzelm@25580
   252
  |> Source.exhaust;
wenzelm@25580
   253
nipkow@14091
   254
wenzelm@24868
   255
(* interactive source of toplevel transformers *)
wenzelm@24868
   256
wenzelm@26600
   257
type isar =
wenzelm@26600
   258
  (Toplevel.transition, (Toplevel.transition option,
wenzelm@36959
   259
    (Token.T, (Token.T option, (Token.T, (Token.T,
wenzelm@30573
   260
      (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
wenzelm@27770
   261
  Source.source) Source.source) Source.source) Source.source)
wenzelm@27770
   262
  Source.source) Source.source) Source.source) Source.source;
wenzelm@26600
   263
wenzelm@38253
   264
fun isar in_stream term : isar =
wenzelm@38253
   265
  Source.tty in_stream
wenzelm@40523
   266
  |> Symbol.source
wenzelm@36959
   267
  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
wenzelm@43711
   268
  |> toplevel_source term (SOME true) lookup_commands_dynamic;
wenzelm@24868
   269
wenzelm@24868
   270
wenzelm@48918
   271
(* side-comments *)
wenzelm@48918
   272
wenzelm@48918
   273
local
wenzelm@48918
   274
wenzelm@48918
   275
fun cmts (t1 :: t2 :: toks) =
wenzelm@48918
   276
      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
wenzelm@48918
   277
      else cmts (t2 :: toks)
wenzelm@48918
   278
  | cmts toks = [];
wenzelm@48918
   279
wenzelm@48918
   280
in
wenzelm@48918
   281
wenzelm@48918
   282
val span_cmts = filter Token.is_proper #> cmts;
wenzelm@48918
   283
wenzelm@48918
   284
end;
wenzelm@48918
   285
wenzelm@48918
   286
wenzelm@44478
   287
(* read toplevel commands -- fail-safe *)
wenzelm@27839
   288
wenzelm@44658
   289
fun read_span outer_syntax toks =
wenzelm@27839
   290
  let
wenzelm@43711
   291
    val commands = lookup_commands outer_syntax;
wenzelm@48749
   292
wenzelm@48771
   293
    val proper_range = Position.set_range (Command.proper_range toks);
wenzelm@48749
   294
    val pos =
wenzelm@48749
   295
      (case find_first Token.is_command toks of
wenzelm@48749
   296
        SOME tok => Token.position_of tok
wenzelm@48771
   297
      | NONE => proper_range);
wenzelm@48647
   298
wenzelm@48647
   299
    fun command_reports tok =
wenzelm@48749
   300
      if Token.is_command tok then
wenzelm@48647
   301
        let val name = Token.content_of tok in
wenzelm@48647
   302
          (case commands name of
wenzelm@48647
   303
            NONE => []
wenzelm@48768
   304
          | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
wenzelm@48647
   305
        end
wenzelm@48647
   306
      else [];
wenzelm@48749
   307
wenzelm@48749
   308
    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
wenzelm@48768
   309
    val _ = Position.reports_text (token_reports @ maps command_reports toks);
wenzelm@27839
   310
  in
wenzelm@48749
   311
    if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
wenzelm@48749
   312
    else
wenzelm@48749
   313
      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
wenzelm@48749
   314
        [tr] =>
wenzelm@48749
   315
          if Keyword.is_control (Toplevel.name_of tr) then
wenzelm@48749
   316
            (Toplevel.malformed pos "Illegal control command", true)
wenzelm@48749
   317
          else (tr, true)
wenzelm@48771
   318
      | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
wenzelm@48771
   319
      | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
wenzelm@48771
   320
      handle ERROR msg => (Toplevel.malformed proper_range msg, true)
wenzelm@27839
   321
  end;
wenzelm@27839
   322
wenzelm@44478
   323
fun read_element outer_syntax init {head, proof, proper_proof} =
wenzelm@28436
   324
  let
wenzelm@44658
   325
    val read = read_span outer_syntax o Thy_Syntax.span_content;
wenzelm@44658
   326
    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
wenzelm@44658
   327
    val proof_trs = map read proof |> filter #2 |> map #1;
wenzelm@28436
   328
  in
wenzelm@47416
   329
    if proper_head andalso proper_proof andalso
wenzelm@47416
   330
      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
wenzelm@43621
   331
    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
wenzelm@28436
   332
  end;
wenzelm@28432
   333
wenzelm@5829
   334
end;
wenzelm@36953
   335