src/Pure/Isar/outer_syntax.ML
author wenzelm
Wed Jan 07 12:08:22 2009 +0100 (2009-01-07 ago)
changeset 29380 a9ee3475abf4
parent 29315 b074c05f00ad
child 29428 3ab54b42ded8
permissions -rw-r--r--
added local_theory';
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@29311
    12
  type 'a parser = 'a OuterParse.parser
wenzelm@29311
    13
  val command: string -> string -> OuterKeyword.T ->
wenzelm@29311
    14
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@29311
    15
  val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
wenzelm@29311
    16
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@29311
    17
  val improper_command: string -> string -> OuterKeyword.T ->
wenzelm@29311
    18
    (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@29311
    19
  val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
wenzelm@29380
    20
  val local_theory': string -> string -> OuterKeyword.T ->
wenzelm@29380
    21
    (bool -> local_theory -> local_theory) parser -> unit
wenzelm@26990
    22
  val local_theory: string -> string -> OuterKeyword.T ->
wenzelm@29311
    23
    (local_theory -> local_theory) parser -> unit
wenzelm@26990
    24
  val local_theory_to_proof': string -> string -> OuterKeyword.T ->
wenzelm@29311
    25
    (bool -> local_theory -> Proof.state) parser -> unit
wenzelm@26990
    26
  val local_theory_to_proof: string -> string -> OuterKeyword.T ->
wenzelm@29311
    27
    (local_theory -> Proof.state) parser -> unit
wenzelm@5883
    28
  val print_outer_syntax: unit -> unit
wenzelm@27839
    29
  val scan: Position.T -> string -> OuterLex.token list
wenzelm@25580
    30
  val parse: Position.T -> string -> Toplevel.transition list
wenzelm@26431
    31
  val process_file: Path.T -> theory -> theory
wenzelm@26600
    32
  type isar
wenzelm@26600
    33
  val isar: bool -> isar
wenzelm@27839
    34
  val prepare_command: Position.T -> string -> Toplevel.transition
wenzelm@27839
    35
  val load_thy: string -> Position.T -> string list -> bool -> unit
wenzelm@5829
    36
end;
wenzelm@5829
    37
wenzelm@26600
    38
structure OuterSyntax: OUTER_SYNTAX =
wenzelm@5829
    39
struct
wenzelm@5829
    40
wenzelm@7750
    41
structure T = OuterLex;
wenzelm@6860
    42
structure P = OuterParse;
wenzelm@29311
    43
type 'a parser = 'a P.parser;
wenzelm@29311
    44
wenzelm@6860
    45
wenzelm@5829
    46
wenzelm@5829
    47
(** outer syntax **)
wenzelm@5829
    48
wenzelm@29311
    49
(* command parsers *)
wenzelm@5829
    50
wenzelm@29311
    51
datatype command = Command of
wenzelm@24868
    52
 {comment: string,
wenzelm@24868
    53
  markup: ThyOutput.markup option,
wenzelm@24868
    54
  int_only: bool,
wenzelm@29311
    55
  parse: (Toplevel.transition -> Toplevel.transition) parser};
wenzelm@5829
    56
wenzelm@29311
    57
fun make_command comment markup int_only parse =
wenzelm@29311
    58
  Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
wenzelm@5829
    59
wenzelm@5829
    60
wenzelm@5829
    61
(* parse command *)
wenzelm@5829
    62
wenzelm@6860
    63
local
wenzelm@6199
    64
wenzelm@14925
    65
fun terminate false = Scan.succeed ()
wenzelm@14925
    66
  | terminate true = P.group "end of input" (Scan.option P.sync -- P.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@26620
    71
      P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
skalberg@15531
    72
  | NONE => sys_error ("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 =
skalberg@15531
    77
  P.semicolon >> K NONE ||
skalberg@15531
    78
  P.sync >> K NONE ||
wenzelm@26620
    79
  (P.position P.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@5829
    87
wenzelm@9132
    88
(** global outer syntax **)
wenzelm@5829
    89
wenzelm@7026
    90
local
wenzelm@7026
    91
wenzelm@29311
    92
val global_commands = ref (Symtab.empty: command Symtab.table);
wenzelm@22120
    93
val global_markups = ref ([]: (string * ThyOutput.markup) list);
wenzelm@5952
    94
wenzelm@29311
    95
fun change_commands f = CRITICAL (fn () =>
wenzelm@29311
    96
 (change global_commands f;
wenzelm@23939
    97
  global_markups :=
wenzelm@29311
    98
    Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
wenzelm@29311
    99
      (! global_commands) []));
wenzelm@6722
   100
wenzelm@7026
   101
in
wenzelm@7026
   102
wenzelm@9132
   103
(* access current syntax *)
wenzelm@7026
   104
wenzelm@29311
   105
fun get_commands () = CRITICAL (fn () => ! global_commands);
wenzelm@24868
   106
fun get_markups () = CRITICAL (fn () => ! global_markups);
wenzelm@7026
   107
wenzelm@29311
   108
fun get_command () = Symtab.lookup (get_commands ());
wenzelm@29311
   109
fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
wenzelm@7789
   110
wenzelm@24868
   111
fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
wenzelm@5829
   112
wenzelm@5829
   113
wenzelm@5829
   114
(* augment syntax *)
wenzelm@5829
   115
wenzelm@29311
   116
fun add_command name kind cmd = CRITICAL (fn () =>
wenzelm@27353
   117
 (OuterKeyword.command name kind;
wenzelm@29311
   118
  if not (Symtab.defined (get_commands ()) name) then ()
wenzelm@24868
   119
  else warning ("Redefining outer syntax command " ^ quote name);
wenzelm@29311
   120
  change_commands (Symtab.update (name, cmd))));
wenzelm@5829
   121
wenzelm@24868
   122
fun command name comment kind parse =
wenzelm@29311
   123
  add_command name kind (make_command comment NONE false parse);
wenzelm@5829
   124
wenzelm@24868
   125
fun markup_command markup name comment kind parse =
wenzelm@29311
   126
  add_command name kind (make_command comment (SOME markup) false parse);
wenzelm@24868
   127
wenzelm@24868
   128
fun improper_command name comment kind parse =
wenzelm@29311
   129
  add_command name kind (make_command comment NONE true parse);
wenzelm@7026
   130
wenzelm@7026
   131
end;
wenzelm@5829
   132
wenzelm@29311
   133
fun internal_command name parse =
wenzelm@29311
   134
  command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
wenzelm@29311
   135
wenzelm@5829
   136
wenzelm@26990
   137
(* local_theory commands *)
wenzelm@26990
   138
wenzelm@26990
   139
fun local_theory_command do_print trans name comment kind parse =
wenzelm@26990
   140
  command name comment kind (P.opt_target -- parse
wenzelm@26990
   141
    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
wenzelm@26990
   142
wenzelm@29380
   143
val local_theory' = local_theory_command false Toplevel.local_theory';
wenzelm@29311
   144
val local_theory = local_theory_command false Toplevel.local_theory;
wenzelm@26990
   145
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
wenzelm@29311
   146
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
wenzelm@26990
   147
wenzelm@26990
   148
wenzelm@24872
   149
(* inspect syntax *)
wenzelm@7026
   150
wenzelm@29311
   151
fun dest_commands () =
wenzelm@29311
   152
  get_commands () |> Symtab.dest |> sort_wrt #1
wenzelm@29311
   153
  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
wenzelm@5829
   154
wenzelm@9223
   155
fun print_outer_syntax () =
wenzelm@7026
   156
  let
wenzelm@27353
   157
    fun pretty_cmd (name, comment, _) =
wenzelm@7026
   158
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
wenzelm@29311
   159
    val (int_cmds, cmds) = List.partition #3 (dest_commands ());
wenzelm@7026
   160
  in
wenzelm@27353
   161
    [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
wenzelm@18326
   162
      Pretty.big_list "commands:" (map pretty_cmd cmds),
wenzelm@18326
   163
      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
wenzelm@9223
   164
    |> Pretty.chunks |> Pretty.writeln
wenzelm@7026
   165
  end;
wenzelm@5829
   166
wenzelm@5829
   167
wenzelm@5829
   168
wenzelm@9132
   169
(** toplevel parsing **)
wenzelm@5829
   170
wenzelm@9132
   171
(* basic sources *)
wenzelm@6860
   172
wenzelm@26620
   173
fun toplevel_source term do_recover cmd src =
wenzelm@9132
   174
  let
wenzelm@9132
   175
    val no_terminator =
wenzelm@9132
   176
      Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
wenzelm@23682
   177
    fun recover int =
wenzelm@23682
   178
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
wenzelm@9132
   179
  in
wenzelm@9132
   180
    src
wenzelm@12876
   181
    |> T.source_proper
wenzelm@9132
   182
    |> Source.source T.stopper
wenzelm@27872
   183
      (Scan.bulk (P.$$$ "--" -- P.!!! P.doc_source >> K NONE || P.not_eof >> SOME))
wenzelm@23682
   184
        (Option.map recover do_recover)
wenzelm@19482
   185
    |> Source.map_filter I
wenzelm@24868
   186
    |> Source.source T.stopper
wenzelm@26620
   187
        (Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs))
wenzelm@23682
   188
        (Option.map recover do_recover)
wenzelm@19482
   189
    |> Source.map_filter I
wenzelm@9132
   190
  end;
wenzelm@5829
   191
wenzelm@7746
   192
wenzelm@25580
   193
(* off-line scanning/parsing *)
wenzelm@14925
   194
wenzelm@27839
   195
fun scan pos str =
wenzelm@16195
   196
  Source.of_string str
wenzelm@27839
   197
  |> Symbol.source {do_recover = false}
wenzelm@27839
   198
  |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
wenzelm@16195
   199
  |> Source.exhaust;
wenzelm@16195
   200
wenzelm@25580
   201
fun parse pos str =
wenzelm@25580
   202
  Source.of_string str
wenzelm@27839
   203
  |> Symbol.source {do_recover = false}
wenzelm@27839
   204
  |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
wenzelm@29311
   205
  |> toplevel_source false NONE get_command
wenzelm@25580
   206
  |> Source.exhaust;
wenzelm@25580
   207
nipkow@14091
   208
wenzelm@26431
   209
(* process file *)
wenzelm@26431
   210
wenzelm@26431
   211
fun process_file path thy =
wenzelm@26431
   212
  let
wenzelm@26881
   213
    val trs = parse (Path.position path) (File.read path);
wenzelm@28424
   214
    val init = Toplevel.init_theory "" (K thy) (K ()) Toplevel.empty;
wenzelm@28424
   215
    val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
wenzelm@28424
   216
  in
wenzelm@28424
   217
    (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
wenzelm@28424
   218
      (true, Context.Theory thy') => thy'
wenzelm@28424
   219
    | _ => error "Bad result state: global theory expected")
wenzelm@28424
   220
  end;
wenzelm@26431
   221
wenzelm@26431
   222
wenzelm@24868
   223
(* interactive source of toplevel transformers *)
wenzelm@24868
   224
wenzelm@26600
   225
type isar =
wenzelm@26600
   226
  (Toplevel.transition, (Toplevel.transition option,
wenzelm@26600
   227
    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
wenzelm@27770
   228
      (SymbolPos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
wenzelm@27770
   229
  Source.source) Source.source) Source.source) Source.source)
wenzelm@27770
   230
  Source.source) Source.source) Source.source) Source.source;
wenzelm@26600
   231
wenzelm@26600
   232
fun isar term : isar =
wenzelm@24868
   233
  Source.tty
wenzelm@27839
   234
  |> Symbol.source {do_recover = true}
wenzelm@27839
   235
  |> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none
wenzelm@29311
   236
  |> toplevel_source term (SOME true) get_command;
wenzelm@24868
   237
wenzelm@24868
   238
wenzelm@27839
   239
(* prepare toplevel commands -- fail-safe *)
wenzelm@27839
   240
wenzelm@27839
   241
val not_singleton = "Exactly one command expected";
wenzelm@27839
   242
wenzelm@29311
   243
fun prepare_span commands span =
wenzelm@27839
   244
  let
wenzelm@29315
   245
    val range_pos = Position.encode_range (ThySyntax.span_range span);
wenzelm@29315
   246
    val toks = ThySyntax.span_content span;
wenzelm@29315
   247
    val _ = List.app ThySyntax.report_token toks;
wenzelm@27839
   248
  in
wenzelm@29311
   249
    (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
wenzelm@27839
   250
      [tr] => (tr, true)
wenzelm@27839
   251
    | [] => (Toplevel.ignored range_pos, false)
wenzelm@27839
   252
    | _ => (Toplevel.malformed range_pos not_singleton, true))
wenzelm@27839
   253
    handle ERROR msg => (Toplevel.malformed range_pos msg, true)
wenzelm@27839
   254
  end;
wenzelm@27839
   255
wenzelm@29311
   256
fun prepare_unit commands (cmd, proof, proper_proof) =
wenzelm@28436
   257
  let
wenzelm@29311
   258
    val (tr, proper_cmd) = prepare_span commands cmd;
wenzelm@29311
   259
    val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
wenzelm@28436
   260
  in
wenzelm@28436
   261
    if proper_cmd andalso proper_proof then [(tr, proof_trs)]
wenzelm@28436
   262
    else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
wenzelm@28436
   263
  end;
wenzelm@28432
   264
wenzelm@27839
   265
fun prepare_command pos str =
wenzelm@29311
   266
  let val (lexs, commands) = get_syntax () in
wenzelm@29315
   267
    (case ThySyntax.parse_spans lexs pos str of
wenzelm@29311
   268
      [span] => #1 (prepare_span commands span)
wenzelm@27839
   269
    | _ => Toplevel.malformed pos not_singleton)
wenzelm@27839
   270
  end;
wenzelm@27839
   271
wenzelm@27839
   272
wenzelm@26611
   273
(* load_thy *)
wenzelm@7746
   274
wenzelm@27839
   275
fun load_thy name pos text time =
wenzelm@7683
   276
  let
wenzelm@29311
   277
    val (lexs, commands) = get_syntax ();
wenzelm@23866
   278
wenzelm@17932
   279
    val _ = Present.init_theory name;
wenzelm@27855
   280
wenzelm@29315
   281
    val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
wenzelm@29315
   282
    val spans = Source.exhaust (ThySyntax.span_source toks);
wenzelm@29315
   283
    val _ = List.app ThySyntax.report_span spans;
wenzelm@29315
   284
    val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
wenzelm@29311
   285
      |> maps (prepare_unit commands);
wenzelm@23866
   286
wenzelm@27855
   287
    val _ = Present.theory_source name
wenzelm@29315
   288
      (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
wenzelm@27855
   289
wenzelm@23866
   290
    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
wenzelm@25685
   291
    val _ = cond_timeit time "" (fn () =>
wenzelm@28424
   292
      let
wenzelm@28432
   293
        val (results, commit_exit) = Toplevel.excursion units;
wenzelm@28424
   294
        val _ =
wenzelm@28432
   295
          ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup results toks
wenzelm@28424
   296
          |> Buffer.content
wenzelm@28424
   297
          |> Present.theory_output name
wenzelm@28424
   298
        val _ = commit_exit ();
wenzelm@28424
   299
      in () end);
wenzelm@23866
   300
    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
wenzelm@24065
   301
  in () end;
wenzelm@23866
   302
wenzelm@5829
   303
end;