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