src/Pure/Isar/outer_syntax.ML
author wenzelm
Mon May 14 22:22:47 2018 +0200 (13 months ago)
changeset 68184 6c693b2700b3
parent 67499 bbb86f719d4b
child 68729 3a02b424d5fb
permissions -rw-r--r--
support for dynamic document output while editing;
wenzelm@5829
     1
(*  Title:      Pure/Isar/outer_syntax.ML
wenzelm@5829
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5829
     3
wenzelm@58928
     4
Isabelle/Isar outer syntax.
wenzelm@5829
     5
*)
wenzelm@5829
     6
wenzelm@5829
     7
signature OUTER_SYNTAX =
wenzelm@5829
     8
sig
wenzelm@58930
     9
  val help: theory -> string list -> unit
wenzelm@58930
    10
  val print_commands: theory -> unit
wenzelm@59935
    11
  type command_keyword = string * Position.T
wenzelm@59935
    12
  val command: command_keyword -> string ->
wenzelm@29311
    13
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@63273
    14
  val maybe_begin_local_theory: command_keyword -> string ->
wenzelm@63273
    15
    (local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit
wenzelm@59935
    16
  val local_theory': command_keyword -> string ->
wenzelm@29380
    17
    (bool -> local_theory -> local_theory) parser -> unit
wenzelm@59935
    18
  val local_theory: command_keyword -> string ->
wenzelm@29311
    19
    (local_theory -> local_theory) parser -> unit
wenzelm@59935
    20
  val local_theory_to_proof': command_keyword -> string ->
wenzelm@29311
    21
    (bool -> local_theory -> Proof.state) parser -> unit
wenzelm@59935
    22
  val local_theory_to_proof: command_keyword -> string ->
wenzelm@29311
    23
    (local_theory -> Proof.state) parser -> unit
wenzelm@60095
    24
  val bootstrap: bool Config.T
wenzelm@67499
    25
  val parse_tokens: theory -> Token.T list -> Toplevel.transition list
wenzelm@58928
    26
  val parse: theory -> Position.T -> string -> Toplevel.transition list
wenzelm@57905
    27
  val parse_spans: Token.T list -> Command_Span.span list
wenzelm@68184
    28
  val make_span: Token.T list -> Command_Span.span
wenzelm@58928
    29
  val command_reports: theory -> Token.T -> Position.report_text list
wenzelm@63274
    30
  val check_command: Proof.context -> command_keyword -> string
wenzelm@5829
    31
end;
wenzelm@5829
    32
wenzelm@36953
    33
structure Outer_Syntax: OUTER_SYNTAX =
wenzelm@5829
    34
struct
wenzelm@5829
    35
wenzelm@5829
    36
(** outer syntax **)
wenzelm@5829
    37
wenzelm@58928
    38
(* errors *)
wenzelm@58928
    39
wenzelm@58928
    40
fun err_command msg name ps =
wenzelm@58928
    41
  error (msg ^ quote (Markup.markup Markup.keyword1 name) ^ Position.here_list ps);
wenzelm@58928
    42
wenzelm@58928
    43
fun err_dup_command name ps =
wenzelm@58928
    44
  err_command "Duplicate outer syntax command " name ps;
wenzelm@58928
    45
wenzelm@58928
    46
wenzelm@29311
    47
(* command parsers *)
wenzelm@5829
    48
wenzelm@59924
    49
datatype command_parser =
wenzelm@59924
    50
  Parser of (Toplevel.transition -> Toplevel.transition) parser |
wenzelm@60691
    51
  Restricted_Parser of
wenzelm@59939
    52
    (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
wenzelm@59924
    53
wenzelm@29311
    54
datatype command = Command of
wenzelm@24868
    55
 {comment: string,
wenzelm@59924
    56
  command_parser: command_parser,
wenzelm@48647
    57
  pos: Position.T,
wenzelm@48647
    58
  id: serial};
wenzelm@5829
    59
wenzelm@58928
    60
fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2;
wenzelm@58928
    61
wenzelm@59924
    62
fun new_command comment command_parser pos =
wenzelm@59924
    63
  Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()};
wenzelm@48647
    64
wenzelm@58928
    65
fun command_pos (Command {pos, ...}) = pos;
wenzelm@58928
    66
wenzelm@48647
    67
fun command_markup def (name, Command {pos, id, ...}) =
wenzelm@48647
    68
  Markup.properties (Position.entity_properties_of def id pos)
wenzelm@50201
    69
    (Markup.entity Markup.commandN name);
wenzelm@5829
    70
wenzelm@50213
    71
fun pretty_command (cmd as (name, Command {comment, ...})) =
wenzelm@50213
    72
  Pretty.block
wenzelm@50213
    73
    (Pretty.marks_str
wenzelm@50450
    74
      ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
wenzelm@50215
    75
        command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
wenzelm@50213
    76
wenzelm@5829
    77
wenzelm@58999
    78
(* theory data *)
wenzelm@43711
    79
wenzelm@58928
    80
structure Data = Theory_Data
wenzelm@58928
    81
(
wenzelm@58999
    82
  type T = command Symtab.table;
wenzelm@58999
    83
  val empty = Symtab.empty;
wenzelm@58928
    84
  val extend = I;
wenzelm@58999
    85
  fun merge data : T =
wenzelm@58999
    86
    data |> Symtab.join (fn name => fn (cmd1, cmd2) =>
wenzelm@58999
    87
      if eq_command (cmd1, cmd2) then raise Symtab.SAME
wenzelm@58999
    88
      else err_dup_command name [command_pos cmd1, command_pos cmd2]);
wenzelm@58928
    89
);
wenzelm@43711
    90
wenzelm@58999
    91
val get_commands = Data.get;
wenzelm@60924
    92
val dest_commands = get_commands #> Symtab.dest #> sort_by #1;
wenzelm@58999
    93
val lookup_commands = Symtab.lookup o get_commands;
wenzelm@58928
    94
wenzelm@58930
    95
fun help thy pats =
wenzelm@58928
    96
  dest_commands thy
wenzelm@58928
    97
  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
wenzelm@58928
    98
  |> map pretty_command
wenzelm@58928
    99
  |> Pretty.writeln_chunks;
wenzelm@58928
   100
wenzelm@58930
   101
fun print_commands thy =
wenzelm@43711
   102
  let
wenzelm@58928
   103
    val keywords = Thy_Header.get_keywords thy;
wenzelm@58928
   104
    val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);
wenzelm@58928
   105
    val commands = dest_commands thy;
wenzelm@58928
   106
  in
wenzelm@58928
   107
    [Pretty.strs ("keywords:" :: map quote minor),
wenzelm@58928
   108
      Pretty.big_list "commands:" (map pretty_command commands)]
wenzelm@58928
   109
    |> Pretty.writeln_chunks
wenzelm@58928
   110
  end;
wenzelm@58928
   111
wenzelm@58928
   112
wenzelm@58999
   113
(* maintain commands *)
wenzelm@58928
   114
wenzelm@58999
   115
fun add_command name cmd thy =
wenzelm@63022
   116
  if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
wenzelm@63022
   117
  else
wenzelm@63022
   118
    let
wenzelm@63022
   119
      val _ =
wenzelm@63022
   120
        Keyword.is_command (Thy_Header.get_keywords thy) name orelse
wenzelm@63022
   121
          err_command "Undeclared outer syntax command " name [command_pos cmd];
wenzelm@63022
   122
      val _ =
wenzelm@63022
   123
        (case lookup_commands thy name of
wenzelm@63022
   124
          NONE => ()
wenzelm@63022
   125
        | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
wenzelm@63022
   126
      val _ =
wenzelm@63022
   127
        Context_Position.report_generic (Context.the_generic_context ())
wenzelm@63022
   128
          (command_pos cmd) (command_markup true (name, cmd));
wenzelm@63022
   129
    in Data.map (Symtab.update (name, cmd)) thy end;
wenzelm@43711
   130
wenzelm@58928
   131
val _ = Theory.setup (Theory.at_end (fn thy =>
wenzelm@58928
   132
  let
wenzelm@58999
   133
    val command_keywords =
wenzelm@58999
   134
      Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy));
wenzelm@58928
   135
    val _ =
wenzelm@58999
   136
      (case subtract (op =) (map #1 (dest_commands thy)) command_keywords of
wenzelm@58928
   137
        [] => ()
wenzelm@58928
   138
      | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
wenzelm@58928
   139
  in NONE end));
wenzelm@43711
   140
wenzelm@5829
   141
wenzelm@58928
   142
(* implicit theory setup *)
wenzelm@46961
   143
wenzelm@59935
   144
type command_keyword = string * Position.T;
wenzelm@5952
   145
wenzelm@59924
   146
fun raw_command (name, pos) comment command_parser =
wenzelm@59932
   147
  let val setup = add_command name (new_command comment command_parser pos)
wenzelm@59932
   148
  in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
wenzelm@26990
   149
wenzelm@59924
   150
fun command (name, pos) comment parse =
wenzelm@59924
   151
  raw_command (name, pos) comment (Parser parse);
wenzelm@59923
   152
wenzelm@63273
   153
fun maybe_begin_local_theory command_keyword comment parse_local parse_global =
wenzelm@63273
   154
  raw_command command_keyword comment
wenzelm@63273
   155
    (Restricted_Parser (fn restricted =>
wenzelm@63273
   156
      Parse.opt_target -- parse_local
wenzelm@63273
   157
        >> (fn (target, f) => Toplevel.local_theory restricted target f) ||
wenzelm@63273
   158
      (if is_some restricted then Scan.fail
wenzelm@63273
   159
       else parse_global >> Toplevel.begin_local_theory true)));
wenzelm@63273
   160
wenzelm@59935
   161
fun local_theory_command trans command_keyword comment parse =
wenzelm@59935
   162
  raw_command command_keyword comment
wenzelm@60691
   163
    (Restricted_Parser (fn restricted =>
wenzelm@60691
   164
      Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
wenzelm@26990
   165
wenzelm@56895
   166
val local_theory' = local_theory_command Toplevel.local_theory';
wenzelm@56895
   167
val local_theory = local_theory_command Toplevel.local_theory;
wenzelm@56895
   168
val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
wenzelm@56895
   169
val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
wenzelm@26990
   170
wenzelm@26990
   171
wenzelm@5829
   172
wenzelm@9132
   173
(** toplevel parsing **)
wenzelm@5829
   174
wenzelm@58928
   175
(* parse commands *)
wenzelm@58928
   176
wenzelm@60095
   177
val bootstrap =
wenzelm@64556
   178
  Config.bool (Config.declare ("Outer_Syntax.bootstrap", \<^here>) (K (Config.Bool true)));
wenzelm@60095
   179
wenzelm@58928
   180
local
wenzelm@58928
   181
wenzelm@59939
   182
val before_command =
wenzelm@59990
   183
  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
wenzelm@59939
   184
wenzelm@58928
   185
fun parse_command thy =
wenzelm@67136
   186
  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
wenzelm@58928
   187
    let
wenzelm@60693
   188
      val keywords = Thy_Header.get_keywords thy;
wenzelm@67136
   189
      val command_tags = Parse.command -- Parse.tags;
wenzelm@60693
   190
      val tr0 =
wenzelm@60693
   191
        Toplevel.empty
wenzelm@60693
   192
        |> Toplevel.name name
wenzelm@60693
   193
        |> Toplevel.position pos
wenzelm@60693
   194
        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
wenzelm@60693
   195
        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
wenzelm@58928
   196
    in
wenzelm@58928
   197
      (case lookup_commands thy name of
wenzelm@59924
   198
        SOME (Command {command_parser = Parser parse, ...}) =>
wenzelm@59924
   199
          Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
wenzelm@60691
   200
      | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
wenzelm@60691
   201
          before_command :|-- (fn restricted =>
wenzelm@60691
   202
            Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0)
wenzelm@60095
   203
      | NONE =>
wenzelm@60095
   204
          Scan.fail_with (fn _ => fn _ =>
wenzelm@60095
   205
            let
wenzelm@60095
   206
              val msg =
wenzelm@60095
   207
                if Config.get_global thy bootstrap
wenzelm@60095
   208
                then "missing theory context for command "
wenzelm@60095
   209
                else "undefined command ";
wenzelm@60095
   210
            in msg ^ quote (Markup.markup Markup.keyword1 name) end))
wenzelm@58928
   211
    end);
wenzelm@58928
   212
wenzelm@60073
   213
in
wenzelm@58928
   214
wenzelm@67499
   215
fun parse_tokens thy =
wenzelm@67499
   216
  filter Token.is_proper
wenzelm@63936
   217
  #> Source.of_list
wenzelm@67499
   218
  #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs))
wenzelm@63936
   219
  #> Source.exhaust;
wenzelm@58928
   220
wenzelm@67499
   221
fun parse thy pos text =
wenzelm@67499
   222
  Symbol_Pos.explode (text, pos)
wenzelm@67499
   223
  |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
wenzelm@67499
   224
  |> parse_tokens thy;
wenzelm@57918
   225
wenzelm@60073
   226
end;
wenzelm@60073
   227
wenzelm@57905
   228
wenzelm@57905
   229
(* parse spans *)
wenzelm@57905
   230
wenzelm@57905
   231
local
wenzelm@57905
   232
wenzelm@57905
   233
fun ship span =
wenzelm@57905
   234
  let
wenzelm@57905
   235
    val kind =
wenzelm@59924
   236
      if forall Token.is_improper span then Command_Span.Ignored_Span
wenzelm@59924
   237
      else if exists Token.is_error span then Command_Span.Malformed_Span
wenzelm@59924
   238
      else
wenzelm@59924
   239
        (case find_first Token.is_command span of
wenzelm@59924
   240
          NONE => Command_Span.Malformed_Span
wenzelm@59924
   241
        | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
wenzelm@57905
   242
  in cons (Command_Span.Span (kind, span)) end;
wenzelm@57905
   243
wenzelm@57905
   244
fun flush (result, content, improper) =
wenzelm@57905
   245
  result
wenzelm@57905
   246
  |> not (null content) ? ship (rev content)
wenzelm@57905
   247
  |> not (null improper) ? ship (rev improper);
wenzelm@57905
   248
wenzelm@57905
   249
fun parse tok (result, content, improper) =
wenzelm@59924
   250
  if Token.is_improper tok then (result, content, tok :: improper)
wenzelm@59939
   251
  else if Token.is_command_modifier tok orelse
wenzelm@59924
   252
    Token.is_command tok andalso
wenzelm@59939
   253
      (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
wenzelm@59924
   254
  then (flush (result, content, improper), [tok], [])
wenzelm@57905
   255
  else (result, tok :: (improper @ content), []);
wenzelm@57905
   256
wenzelm@57905
   257
in
wenzelm@57905
   258
wenzelm@57905
   259
fun parse_spans toks =
wenzelm@57905
   260
  fold parse toks ([], [], []) |> flush |> rev;
wenzelm@57905
   261
wenzelm@57905
   262
end;
wenzelm@57905
   263
wenzelm@68184
   264
fun make_span toks =
wenzelm@68184
   265
  (case parse_spans toks of
wenzelm@68184
   266
    [span] => span
wenzelm@68184
   267
  | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
wenzelm@68184
   268
nipkow@14091
   269
wenzelm@61618
   270
(* check commands *)
wenzelm@48647
   271
wenzelm@58928
   272
fun command_reports thy tok =
wenzelm@52510
   273
  if Token.is_command tok then
wenzelm@52510
   274
    let val name = Token.content_of tok in
wenzelm@58928
   275
      (case lookup_commands thy name of
wenzelm@52510
   276
        NONE => []
wenzelm@55708
   277
      | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
wenzelm@52510
   278
    end
wenzelm@52510
   279
  else [];
wenzelm@48749
   280
wenzelm@61618
   281
fun check_command ctxt (name, pos) =
wenzelm@61618
   282
  let
wenzelm@61618
   283
    val thy = Proof_Context.theory_of ctxt;
wenzelm@61618
   284
    val keywords = Thy_Header.get_keywords thy;
wenzelm@61618
   285
  in
wenzelm@61618
   286
    if Keyword.is_command keywords name then
wenzelm@61618
   287
      let
wenzelm@61618
   288
        val markup =
wenzelm@67495
   289
          Token.explode0 keywords name
wenzelm@61618
   290
          |> maps (command_reports thy)
wenzelm@61618
   291
          |> map (#2 o #1);
wenzelm@61618
   292
        val _ = Context_Position.reports ctxt (map (pair pos) markup);
wenzelm@61618
   293
      in name end
wenzelm@61618
   294
    else
wenzelm@61618
   295
      let
wenzelm@61618
   296
        val completion =
wenzelm@61618
   297
          Completion.make (name, pos)
wenzelm@61618
   298
            (fn completed =>
wenzelm@61618
   299
              Keyword.dest_commands keywords
wenzelm@61618
   300
              |> filter completed
wenzelm@61618
   301
              |> sort_strings
wenzelm@61618
   302
              |> map (fn a => (a, (Markup.commandN, a))));
wenzelm@61618
   303
        val report = Markup.markup_report (Completion.reported_text completion);
wenzelm@61618
   304
      in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
wenzelm@61618
   305
  end;
wenzelm@61618
   306
wenzelm@62849
   307
wenzelm@62849
   308
(* 'ML' command -- required for bootstrapping Isar *)
wenzelm@62849
   309
wenzelm@62849
   310
val _ =
wenzelm@64556
   311
  command ("ML", \<^here>) "ML text within theory or local theory"
wenzelm@62849
   312
    (Parse.ML_source >> (fn source =>
wenzelm@62849
   313
      Toplevel.generic_theory
wenzelm@62849
   314
        (ML_Context.exec (fn () =>
wenzelm@62849
   315
            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
wenzelm@62849
   316
          Local_Theory.propagate_ml_env)));
wenzelm@62849
   317
wenzelm@5829
   318
end;