src/Pure/Isar/outer_syntax.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25 ago)
changeset 27353 71c4dd53d4cb
parent 26990 a91f7741967a
child 27439 7d5c4e73c89e
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
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@16195
    25
  val scan: 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@26611
    30
  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
wenzelm@5829
    31
end;
wenzelm@5829
    32
wenzelm@26600
    33
structure OuterSyntax: OUTER_SYNTAX =
wenzelm@5829
    34
struct
wenzelm@5829
    35
wenzelm@7750
    36
structure T = OuterLex;
wenzelm@6860
    37
structure P = OuterParse;
wenzelm@6860
    38
wenzelm@5829
    39
wenzelm@5829
    40
(** outer syntax **)
wenzelm@5829
    41
wenzelm@5829
    42
(* parsers *)
wenzelm@5829
    43
wenzelm@24868
    44
type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list;
wenzelm@5829
    45
wenzelm@24868
    46
datatype parser = Parser of
wenzelm@24868
    47
 {comment: string,
wenzelm@24868
    48
  markup: ThyOutput.markup option,
wenzelm@24868
    49
  int_only: bool,
wenzelm@24868
    50
  parse: parser_fn};
wenzelm@5829
    51
wenzelm@27353
    52
fun make_parser comment markup int_only parse =
wenzelm@27353
    53
  Parser {comment = comment, markup = markup, int_only = int_only, parse = parse};
wenzelm@5829
    54
wenzelm@5829
    55
wenzelm@5829
    56
(* parse command *)
wenzelm@5829
    57
wenzelm@6860
    58
local
wenzelm@6199
    59
wenzelm@14925
    60
fun terminate false = Scan.succeed ()
wenzelm@14925
    61
  | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
wenzelm@14925
    62
wenzelm@26620
    63
fun body cmd (name, _) =
wenzelm@7026
    64
  (case cmd name of
wenzelm@24868
    65
    SOME (Parser {int_only, parse, ...}) =>
wenzelm@26620
    66
      P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
skalberg@15531
    67
  | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
wenzelm@6860
    68
wenzelm@6860
    69
in
wenzelm@5829
    70
wenzelm@26620
    71
fun parse_command do_terminate cmd =
skalberg@15531
    72
  P.semicolon >> K NONE ||
skalberg@15531
    73
  P.sync >> K NONE ||
wenzelm@26620
    74
  (P.position P.command :-- body cmd) --| terminate do_terminate
wenzelm@6860
    75
    >> (fn ((name, pos), (int_only, f)) =>
skalberg@15531
    76
      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
wenzelm@6860
    77
        Toplevel.interactive int_only |> f));
wenzelm@5829
    78
wenzelm@6199
    79
end;
wenzelm@6199
    80
wenzelm@5829
    81
wenzelm@5829
    82
wenzelm@9132
    83
(** global outer syntax **)
wenzelm@5829
    84
wenzelm@7026
    85
local
wenzelm@7026
    86
wenzelm@24868
    87
val global_parsers = ref (Symtab.empty: parser Symtab.table);
wenzelm@22120
    88
val global_markups = ref ([]: (string * ThyOutput.markup) list);
wenzelm@5952
    89
wenzelm@23939
    90
fun change_parsers f = CRITICAL (fn () =>
wenzelm@23939
    91
 (change global_parsers f;
wenzelm@23939
    92
  global_markups :=
wenzelm@24868
    93
    Symtab.fold (fn (name, Parser {markup = SOME m, ...}) => cons (name, m) | _ => I)
wenzelm@24868
    94
      (! global_parsers) []));
wenzelm@6722
    95
wenzelm@7026
    96
in
wenzelm@7026
    97
wenzelm@9132
    98
(* access current syntax *)
wenzelm@7026
    99
wenzelm@24868
   100
fun get_parsers () = CRITICAL (fn () => ! global_parsers);
wenzelm@24868
   101
fun get_markups () = CRITICAL (fn () => ! global_markups);
wenzelm@7026
   102
wenzelm@24868
   103
fun get_parser () = Symtab.lookup (get_parsers ());
wenzelm@7789
   104
wenzelm@24868
   105
fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
wenzelm@5829
   106
wenzelm@5829
   107
wenzelm@5829
   108
(* augment syntax *)
wenzelm@5829
   109
wenzelm@27353
   110
fun add_parser name kind parser = CRITICAL (fn () =>
wenzelm@27353
   111
 (OuterKeyword.command name kind;
wenzelm@27353
   112
  if not (Symtab.defined (get_parsers ()) name) then ()
wenzelm@24868
   113
  else warning ("Redefining outer syntax command " ^ quote name);
wenzelm@27353
   114
  change_parsers (Symtab.update (name, parser))));
wenzelm@5829
   115
wenzelm@24868
   116
fun command name comment kind parse =
wenzelm@27353
   117
  add_parser name kind (make_parser comment NONE false parse);
wenzelm@5829
   118
wenzelm@24868
   119
fun markup_command markup name comment kind parse =
wenzelm@27353
   120
  add_parser name kind (make_parser comment (SOME markup) false parse);
wenzelm@24868
   121
wenzelm@24868
   122
fun improper_command name comment kind parse =
wenzelm@27353
   123
  add_parser name kind (make_parser comment NONE true parse);
wenzelm@7026
   124
wenzelm@7026
   125
end;
wenzelm@5829
   126
wenzelm@5829
   127
wenzelm@26990
   128
(* local_theory commands *)
wenzelm@26990
   129
wenzelm@26990
   130
fun local_theory_command do_print trans name comment kind parse =
wenzelm@26990
   131
  command name comment kind (P.opt_target -- parse
wenzelm@26990
   132
    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
wenzelm@26990
   133
wenzelm@26990
   134
val local_theory           = local_theory_command false Toplevel.local_theory;
wenzelm@26990
   135
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
wenzelm@26990
   136
val local_theory_to_proof  = local_theory_command true Toplevel.local_theory_to_proof;
wenzelm@26990
   137
wenzelm@26990
   138
wenzelm@24872
   139
(* inspect syntax *)
wenzelm@7026
   140
wenzelm@7026
   141
fun dest_parsers () =
wenzelm@16727
   142
  get_parsers () |> Symtab.dest |> sort_wrt #1
wenzelm@27353
   143
  |> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only));
wenzelm@5829
   144
wenzelm@9223
   145
fun print_outer_syntax () =
wenzelm@7026
   146
  let
wenzelm@27353
   147
    fun pretty_cmd (name, comment, _) =
wenzelm@7026
   148
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
wenzelm@27353
   149
    val (int_cmds, cmds) = List.partition #3 (dest_parsers ());
wenzelm@7026
   150
  in
wenzelm@27353
   151
    [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
wenzelm@18326
   152
      Pretty.big_list "commands:" (map pretty_cmd cmds),
wenzelm@18326
   153
      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
wenzelm@9223
   154
    |> Pretty.chunks |> Pretty.writeln
wenzelm@7026
   155
  end;
wenzelm@5829
   156
wenzelm@5829
   157
wenzelm@5829
   158
wenzelm@9132
   159
(** toplevel parsing **)
wenzelm@5829
   160
wenzelm@9132
   161
(* basic sources *)
wenzelm@6860
   162
wenzelm@26620
   163
fun toplevel_source term do_recover cmd src =
wenzelm@9132
   164
  let
wenzelm@9132
   165
    val no_terminator =
wenzelm@9132
   166
      Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
wenzelm@23682
   167
    fun recover int =
wenzelm@23682
   168
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
wenzelm@9132
   169
  in
wenzelm@9132
   170
    src
wenzelm@12876
   171
    |> T.source_proper
wenzelm@9132
   172
    |> Source.source T.stopper
skalberg@15531
   173
      (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
wenzelm@23682
   174
        (Option.map recover do_recover)
wenzelm@19482
   175
    |> Source.map_filter I
wenzelm@24868
   176
    |> Source.source T.stopper
wenzelm@26620
   177
        (Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs))
wenzelm@23682
   178
        (Option.map recover do_recover)
wenzelm@19482
   179
    |> Source.map_filter I
wenzelm@9132
   180
  end;
wenzelm@5829
   181
wenzelm@7746
   182
wenzelm@25580
   183
(* off-line scanning/parsing *)
wenzelm@14925
   184
aspinall@15144
   185
fun scan str =
wenzelm@16195
   186
  Source.of_string str
wenzelm@16195
   187
  |> Symbol.source false
wenzelm@27353
   188
  |> T.source (SOME false) OuterKeyword.get_lexicons Position.none
wenzelm@16195
   189
  |> Source.exhaust;
wenzelm@16195
   190
wenzelm@25580
   191
fun parse pos str =
wenzelm@25580
   192
  Source.of_string str
wenzelm@25580
   193
  |> Symbol.source false
wenzelm@27353
   194
  |> T.source (SOME false) OuterKeyword.get_lexicons pos
wenzelm@26620
   195
  |> toplevel_source false NONE get_parser
wenzelm@25580
   196
  |> Source.exhaust;
wenzelm@25580
   197
nipkow@14091
   198
wenzelm@26431
   199
(* process file *)
wenzelm@26431
   200
wenzelm@26431
   201
fun process_file path thy =
wenzelm@26431
   202
  let
wenzelm@26431
   203
    val result = ref thy;
wenzelm@26881
   204
    val trs = parse (Path.position path) (File.read path);
wenzelm@26431
   205
    val init = Toplevel.init_theory (K thy) (fn thy' => result := thy') (K ());
wenzelm@26431
   206
    val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
wenzelm@26431
   207
  in ! result end;
wenzelm@26431
   208
wenzelm@26431
   209
wenzelm@24868
   210
(* interactive source of toplevel transformers *)
wenzelm@24868
   211
wenzelm@26600
   212
type isar =
wenzelm@26600
   213
  (Toplevel.transition, (Toplevel.transition option,
wenzelm@26600
   214
    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
wenzelm@26600
   215
      Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
wenzelm@26600
   216
          Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
wenzelm@26600
   217
wenzelm@26600
   218
fun isar term : isar =
wenzelm@24868
   219
  Source.tty
wenzelm@24868
   220
  |> Symbol.source true
wenzelm@27353
   221
  |> T.source (SOME true) OuterKeyword.get_lexicons Position.none
wenzelm@26620
   222
  |> toplevel_source term (SOME true) get_parser;
wenzelm@24868
   223
wenzelm@24868
   224
wenzelm@26611
   225
(* load_thy *)
wenzelm@7746
   226
wenzelm@26323
   227
fun load_thy dir name pos text time =
wenzelm@7683
   228
  let
wenzelm@24065
   229
    val text_src = Source.of_list (Library.untabify text);
wenzelm@27353
   230
    val (lexs, parser) = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ()));
wenzelm@23866
   231
wenzelm@17932
   232
    val _ = Present.init_theory name;
wenzelm@24065
   233
    val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src));
wenzelm@24065
   234
    val toks = text_src
wenzelm@17932
   235
      |> Symbol.source false
wenzelm@27353
   236
      |> T.source NONE (K lexs) pos
wenzelm@17932
   237
      |> Source.exhausted;
wenzelm@17932
   238
    val trs = toks
wenzelm@27353
   239
      |> toplevel_source false NONE (K parser)
wenzelm@17932
   240
      |> Source.exhaust;
wenzelm@23866
   241
wenzelm@23866
   242
    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
wenzelm@25685
   243
    val _ = cond_timeit time "" (fn () =>
wenzelm@27353
   244
      ThyOutput.process_thy (#1 lexs) OuterKeyword.command_tags is_markup trs toks
wenzelm@23866
   245
      |> Buffer.content
wenzelm@23866
   246
      |> Present.theory_output name);
wenzelm@23866
   247
    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
wenzelm@24065
   248
  in () end;
wenzelm@23866
   249
wenzelm@5829
   250
end;
wenzelm@5829
   251