src/Pure/Isar/outer_syntax.ML
author wenzelm
Thu Mar 15 22:08:53 2012 +0100 (2012-03-15 ago)
changeset 46950 d0181abdbdac
parent 46876 8f3bb485f628
child 46957 0c15caf47040
permissions -rw-r--r--
declare command keywords via theory header, including strict checking outside Pure;
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@36950
    15
  val command: string -> string -> Keyword.T ->
wenzelm@29311
    16
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@37216
    17
  val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
wenzelm@29311
    18
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@36950
    19
  val improper_command: string -> string -> Keyword.T ->
wenzelm@29311
    20
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@43711
    21
  val internal_command: string ->
wenzelm@43711
    22
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@36950
    23
  val local_theory': string -> string -> Keyword.T ->
wenzelm@29380
    24
    (bool -> local_theory -> local_theory) parser -> unit
wenzelm@36950
    25
  val local_theory: string -> string -> Keyword.T ->
wenzelm@29311
    26
    (local_theory -> local_theory) parser -> unit
wenzelm@36950
    27
  val local_theory_to_proof': string -> string -> Keyword.T ->
wenzelm@29311
    28
    (bool -> local_theory -> Proof.state) parser -> unit
wenzelm@36950
    29
  val local_theory_to_proof: string -> string -> Keyword.T ->
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@26431
    34
  val process_file: Path.T -> theory -> theory
wenzelm@26600
    35
  type isar
wenzelm@38253
    36
  val isar: TextIO.instream -> bool -> isar
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@29311
    53
  parse: (Toplevel.transition -> Toplevel.transition) parser};
wenzelm@5829
    54
wenzelm@29311
    55
fun make_command comment markup int_only parse =
wenzelm@29311
    56
  Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
wenzelm@5829
    57
wenzelm@5829
    58
wenzelm@5829
    59
(* parse command *)
wenzelm@5829
    60
wenzelm@6860
    61
local
wenzelm@6199
    62
wenzelm@14925
    63
fun terminate false = Scan.succeed ()
wenzelm@44357
    64
  | terminate true =
wenzelm@44357
    65
      Parse.group (fn () => "end of input")
wenzelm@44357
    66
        (Scan.option Parse.sync -- Parse.semicolon >> K ());
wenzelm@14925
    67
wenzelm@26620
    68
fun body cmd (name, _) =
wenzelm@7026
    69
  (case cmd name of
wenzelm@29311
    70
    SOME (Command {int_only, parse, ...}) =>
wenzelm@36950
    71
      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
wenzelm@37852
    72
  | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
wenzelm@6860
    73
wenzelm@6860
    74
in
wenzelm@5829
    75
wenzelm@26620
    76
fun parse_command do_terminate cmd =
wenzelm@36950
    77
  Parse.semicolon >> K NONE ||
wenzelm@36950
    78
  Parse.sync >> K NONE ||
wenzelm@36950
    79
  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
wenzelm@6860
    80
    >> (fn ((name, pos), (int_only, f)) =>
skalberg@15531
    81
      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
wenzelm@6860
    82
        Toplevel.interactive int_only |> f));
wenzelm@5829
    83
wenzelm@6199
    84
end;
wenzelm@6199
    85
wenzelm@5829
    86
wenzelm@43711
    87
(* type outer_syntax *)
wenzelm@43711
    88
wenzelm@43711
    89
datatype outer_syntax = Outer_Syntax of
wenzelm@43711
    90
 {commands: command Symtab.table,
wenzelm@43711
    91
  markups: (string * Thy_Output.markup) list};
wenzelm@43711
    92
wenzelm@43711
    93
fun make_outer_syntax commands markups =
wenzelm@43711
    94
  Outer_Syntax {commands = commands, markups = markups};
wenzelm@43711
    95
wenzelm@43711
    96
val empty_outer_syntax = make_outer_syntax Symtab.empty [];
wenzelm@43711
    97
wenzelm@43711
    98
wenzelm@43711
    99
fun map_commands f (Outer_Syntax {commands, ...}) =
wenzelm@43711
   100
  let
wenzelm@43711
   101
    val commands' = f commands;
wenzelm@43711
   102
    val markups' =
wenzelm@43711
   103
      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
wenzelm@43711
   104
        commands' [];
wenzelm@43711
   105
  in make_outer_syntax commands' markups' end;
wenzelm@43711
   106
wenzelm@43711
   107
fun dest_commands (Outer_Syntax {commands, ...}) =
wenzelm@43711
   108
  commands |> Symtab.dest |> sort_wrt #1
wenzelm@43711
   109
  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
wenzelm@43711
   110
wenzelm@43711
   111
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
wenzelm@43711
   112
wenzelm@43711
   113
fun is_markup (Outer_Syntax {markups, ...}) kind name =
wenzelm@43711
   114
  AList.lookup (op =) markups name = SOME kind;
wenzelm@43711
   115
wenzelm@43711
   116
wenzelm@5829
   117
wenzelm@9132
   118
(** global outer syntax **)
wenzelm@5829
   119
wenzelm@7026
   120
local
wenzelm@7026
   121
wenzelm@43711
   122
(*synchronized wrt. Keywords*)
wenzelm@43711
   123
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
wenzelm@5952
   124
wenzelm@43711
   125
fun add_command name kind cmd = CRITICAL (fn () =>
wenzelm@46950
   126
  let
wenzelm@46950
   127
    val thy = ML_Context.the_global_context ();
wenzelm@46950
   128
    val _ =
wenzelm@46950
   129
      (case try (Thy_Header.the_keyword thy) name of
wenzelm@46950
   130
        SOME k =>
wenzelm@46950
   131
          if k = SOME kind then ()
wenzelm@46950
   132
          else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
wenzelm@46950
   133
      | NONE =>
wenzelm@46950
   134
          (Keyword.command name kind;
wenzelm@46950
   135
           if Context.theory_name thy = Context.PureN then ()
wenzelm@46950
   136
           else error ("Undeclared outer syntax command " ^ quote name)));
wenzelm@46950
   137
  in
wenzelm@46950
   138
    Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
wenzelm@46950
   139
     (if not (Symtab.defined commands name) then ()
wenzelm@46950
   140
      else warning ("Redefining outer syntax command " ^ quote name);
wenzelm@46950
   141
      Symtab.update (name, cmd) commands)))
wenzelm@46950
   142
  end);
wenzelm@6722
   143
wenzelm@7026
   144
in
wenzelm@7026
   145
wenzelm@43711
   146
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
wenzelm@7789
   147
wenzelm@43711
   148
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
wenzelm@5829
   149
wenzelm@24868
   150
fun command name comment kind parse =
wenzelm@29311
   151
  add_command name kind (make_command comment NONE false parse);
wenzelm@5829
   152
wenzelm@24868
   153
fun markup_command markup name comment kind parse =
wenzelm@29311
   154
  add_command name kind (make_command comment (SOME markup) false parse);
wenzelm@24868
   155
wenzelm@24868
   156
fun improper_command name comment kind parse =
wenzelm@29311
   157
  add_command name kind (make_command comment NONE true parse);
wenzelm@7026
   158
wenzelm@29311
   159
fun internal_command name parse =
wenzelm@36950
   160
  command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
wenzelm@29311
   161
wenzelm@43711
   162
end;
wenzelm@43711
   163
wenzelm@5829
   164
wenzelm@26990
   165
(* local_theory commands *)
wenzelm@26990
   166
wenzelm@26990
   167
fun local_theory_command do_print trans name comment kind parse =
wenzelm@36950
   168
  command name comment kind (Parse.opt_target -- parse
wenzelm@26990
   169
    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
wenzelm@26990
   170
wenzelm@29380
   171
val local_theory' = local_theory_command false Toplevel.local_theory';
wenzelm@29311
   172
val local_theory = local_theory_command false Toplevel.local_theory;
wenzelm@26990
   173
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
wenzelm@29311
   174
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
wenzelm@26990
   175
wenzelm@26990
   176
wenzelm@24872
   177
(* inspect syntax *)
wenzelm@7026
   178
wenzelm@9223
   179
fun print_outer_syntax () =
wenzelm@7026
   180
  let
wenzelm@43711
   181
    val (keywords, outer_syntax) =
wenzelm@43711
   182
      CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ())));
wenzelm@27353
   183
    fun pretty_cmd (name, comment, _) =
wenzelm@7026
   184
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
wenzelm@43711
   185
    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
wenzelm@7026
   186
  in
wenzelm@43711
   187
    [Pretty.strs ("syntax keywords:" :: map quote keywords),
wenzelm@18326
   188
      Pretty.big_list "commands:" (map pretty_cmd cmds),
wenzelm@18326
   189
      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
wenzelm@9223
   190
    |> Pretty.chunks |> Pretty.writeln
wenzelm@7026
   191
  end;
wenzelm@5829
   192
wenzelm@5829
   193
wenzelm@5829
   194
wenzelm@9132
   195
(** toplevel parsing **)
wenzelm@5829
   196
wenzelm@9132
   197
(* basic sources *)
wenzelm@6860
   198
wenzelm@26620
   199
fun toplevel_source term do_recover cmd src =
wenzelm@9132
   200
  let
wenzelm@9132
   201
    val no_terminator =
wenzelm@36959
   202
      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
wenzelm@23682
   203
    fun recover int =
wenzelm@23682
   204
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
wenzelm@9132
   205
  in
wenzelm@9132
   206
    src
wenzelm@36959
   207
    |> Token.source_proper
wenzelm@36959
   208
    |> Source.source Token.stopper
wenzelm@36950
   209
      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
wenzelm@23682
   210
        (Option.map recover do_recover)
wenzelm@19482
   211
    |> Source.map_filter I
wenzelm@36959
   212
    |> Source.source Token.stopper
wenzelm@36950
   213
        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
wenzelm@23682
   214
        (Option.map recover do_recover)
wenzelm@19482
   215
    |> Source.map_filter I
wenzelm@9132
   216
  end;
wenzelm@5829
   217
wenzelm@7746
   218
wenzelm@25580
   219
(* off-line scanning/parsing *)
wenzelm@14925
   220
wenzelm@27839
   221
fun scan pos str =
wenzelm@16195
   222
  Source.of_string str
wenzelm@40523
   223
  |> Symbol.source
wenzelm@36959
   224
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
wenzelm@16195
   225
  |> Source.exhaust;
wenzelm@16195
   226
wenzelm@25580
   227
fun parse pos str =
wenzelm@25580
   228
  Source.of_string str
wenzelm@40523
   229
  |> Symbol.source
wenzelm@36959
   230
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
wenzelm@43711
   231
  |> toplevel_source false NONE lookup_commands_dynamic
wenzelm@25580
   232
  |> Source.exhaust;
wenzelm@25580
   233
nipkow@14091
   234
wenzelm@26431
   235
(* process file *)
wenzelm@26431
   236
wenzelm@26431
   237
fun process_file path thy =
wenzelm@26431
   238
  let
wenzelm@26881
   239
    val trs = parse (Path.position path) (File.read path);
wenzelm@44187
   240
    val init = Toplevel.init_theory (K thy) Toplevel.empty;
wenzelm@28424
   241
    val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
wenzelm@28424
   242
  in
wenzelm@28424
   243
    (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
wenzelm@28424
   244
      (true, Context.Theory thy') => thy'
wenzelm@28424
   245
    | _ => error "Bad result state: global theory expected")
wenzelm@28424
   246
  end;
wenzelm@26431
   247
wenzelm@26431
   248
wenzelm@24868
   249
(* interactive source of toplevel transformers *)
wenzelm@24868
   250
wenzelm@26600
   251
type isar =
wenzelm@26600
   252
  (Toplevel.transition, (Toplevel.transition option,
wenzelm@36959
   253
    (Token.T, (Token.T option, (Token.T, (Token.T,
wenzelm@30573
   254
      (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
wenzelm@27770
   255
  Source.source) Source.source) Source.source) Source.source)
wenzelm@27770
   256
  Source.source) Source.source) Source.source) Source.source;
wenzelm@26600
   257
wenzelm@38253
   258
fun isar in_stream term : isar =
wenzelm@38253
   259
  Source.tty in_stream
wenzelm@40523
   260
  |> Symbol.source
wenzelm@36959
   261
  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
wenzelm@43711
   262
  |> toplevel_source term (SOME true) lookup_commands_dynamic;
wenzelm@24868
   263
wenzelm@24868
   264
wenzelm@44478
   265
(* read toplevel commands -- fail-safe *)
wenzelm@27839
   266
wenzelm@27839
   267
val not_singleton = "Exactly one command expected";
wenzelm@27839
   268
wenzelm@44658
   269
fun read_span outer_syntax toks =
wenzelm@27839
   270
  let
wenzelm@43711
   271
    val commands = lookup_commands outer_syntax;
wenzelm@44658
   272
    val range_pos = Position.set_range (Token.range toks);
wenzelm@44736
   273
    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
wenzelm@27839
   274
  in
wenzelm@29311
   275
    (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
wenzelm@37713
   276
      [tr] =>
wenzelm@37713
   277
        if Keyword.is_control (Toplevel.name_of tr) then
wenzelm@44658
   278
          (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
wenzelm@37713
   279
        else (tr, true)
wenzelm@27839
   280
    | [] => (Toplevel.ignored range_pos, false)
wenzelm@27839
   281
    | _ => (Toplevel.malformed range_pos not_singleton, true))
wenzelm@27839
   282
    handle ERROR msg => (Toplevel.malformed range_pos msg, true)
wenzelm@27839
   283
  end;
wenzelm@27839
   284
wenzelm@44478
   285
fun read_element outer_syntax init {head, proof, proper_proof} =
wenzelm@28436
   286
  let
wenzelm@44658
   287
    val read = read_span outer_syntax o Thy_Syntax.span_content;
wenzelm@44658
   288
    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
wenzelm@44658
   289
    val proof_trs = map read proof |> filter #2 |> map #1;
wenzelm@28436
   290
  in
wenzelm@43621
   291
    if proper_head andalso proper_proof then [(tr, proof_trs)]
wenzelm@43621
   292
    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
wenzelm@28436
   293
  end;
wenzelm@28432
   294
wenzelm@5829
   295
end;
wenzelm@36953
   296