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