src/Pure/Isar/outer_syntax.ML
author wenzelm
Fri, 08 Jul 2011 20:27:09 +0200
changeset 43711 608d1b451f67
parent 43621 e8858190cccd
child 43712 3c2c912af2ef
permissions -rw-r--r--
less stateful outer_syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/outer_syntax.ML
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     3
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     4
The global Isabelle/Isar outer syntax.
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     5
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     6
Note: the syntax for files is statically determined at the very
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
     7
beginning; for interactive processing it may change dynamically.
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     8
*)
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     9
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    10
signature OUTER_SYNTAX =
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    11
sig
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    12
  type outer_syntax
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    13
  val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    14
  val command: string -> string -> Keyword.T ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    15
    (Toplevel.transition -> Toplevel.transition) parser -> unit
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
    16
  val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    17
    (Toplevel.transition -> Toplevel.transition) parser -> unit
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    18
  val improper_command: string -> string -> Keyword.T ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    19
    (Toplevel.transition -> Toplevel.transition) parser -> unit
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    20
  val internal_command: string ->
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    21
    (Toplevel.transition -> Toplevel.transition) parser -> unit
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    22
  val local_theory': string -> string -> Keyword.T ->
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29315
diff changeset
    23
    (bool -> local_theory -> local_theory) parser -> unit
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    24
  val local_theory: string -> string -> Keyword.T ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    25
    (local_theory -> local_theory) parser -> unit
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    26
  val local_theory_to_proof': string -> string -> Keyword.T ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    27
    (bool -> local_theory -> Proof.state) parser -> unit
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    28
  val local_theory_to_proof: string -> string -> Keyword.T ->
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    29
    (local_theory -> Proof.state) parser -> unit
5883
975c984526b0 tuned names;
wenzelm
parents: 5829
diff changeset
    30
  val print_outer_syntax: unit -> unit
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    31
  val scan: Position.T -> string -> Token.T list
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
    32
  val parse: Position.T -> string -> Toplevel.transition list
26431
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
    33
  val process_file: Path.T -> theory -> theory
26600
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
    34
  type isar
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38236
diff changeset
    35
  val isar: TextIO.instream -> bool -> isar
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
    36
  val prepare_command: Position.T -> string -> Toplevel.transition
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
    37
  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    38
end;
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    39
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
    40
structure Outer_Syntax: OUTER_SYNTAX =
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    41
struct
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    42
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    43
(** outer syntax **)
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    44
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    45
(* command parsers *)
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    46
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    47
datatype command = Command of
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
    48
 {comment: string,
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
    49
  markup: Thy_Output.markup option,
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
    50
  int_only: bool,
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    51
  parse: (Toplevel.transition -> Toplevel.transition) parser};
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    52
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    53
fun make_command comment markup int_only parse =
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    54
  Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    55
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    56
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    57
(* parse command *)
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    58
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    59
local
6199
9b1be867e21a removed load;
wenzelm
parents: 6107
diff changeset
    60
14925
0f86a8a694f8 added read (provides transition names and sources);
wenzelm
parents: 14687
diff changeset
    61
fun terminate false = Scan.succeed ()
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    62
  | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
14925
0f86a8a694f8 added read (provides transition names and sources);
wenzelm
parents: 14687
diff changeset
    63
26620
722cf4fdd4dd eliminated unused trace, read;
wenzelm
parents: 26611
diff changeset
    64
fun body cmd (name, _) =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
    65
  (case cmd name of
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
    66
    SOME (Command {int_only, parse, ...}) =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    67
      Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
37852
a902f158b4fc eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents: 37713
diff changeset
    68
  | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    69
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    70
in
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    71
26620
722cf4fdd4dd eliminated unused trace, read;
wenzelm
parents: 26611
diff changeset
    72
fun parse_command do_terminate cmd =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    73
  Parse.semicolon >> K NONE ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    74
  Parse.sync >> K NONE ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
    75
  (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    76
    >> (fn ((name, pos), (int_only, f)) =>
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15224
diff changeset
    77
      SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
    78
        Toplevel.interactive int_only |> f));
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    79
6199
9b1be867e21a removed load;
wenzelm
parents: 6107
diff changeset
    80
end;
9b1be867e21a removed load;
wenzelm
parents: 6107
diff changeset
    81
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    82
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    83
(* type outer_syntax *)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    84
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    85
datatype outer_syntax = Outer_Syntax of
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    86
 {commands: command Symtab.table,
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    87
  markups: (string * Thy_Output.markup) list};
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    88
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    89
fun make_outer_syntax commands markups =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    90
  Outer_Syntax {commands = commands, markups = markups};
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    91
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    92
val empty_outer_syntax = make_outer_syntax Symtab.empty [];
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    93
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    94
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    95
fun map_commands f (Outer_Syntax {commands, ...}) =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    96
  let
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    97
    val commands' = f commands;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    98
    val markups' =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
    99
      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   100
        commands' [];
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   101
  in make_outer_syntax commands' markups' end;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   102
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   103
fun dest_commands (Outer_Syntax {commands, ...}) =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   104
  commands |> Symtab.dest |> sort_wrt #1
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   105
  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   106
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   107
fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   108
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   109
fun is_markup (Outer_Syntax {markups, ...}) kind name =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   110
  AList.lookup (op =) markups name = SOME kind;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   111
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   112
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   113
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   114
(** global outer syntax **)
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   115
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   116
local
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   117
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   118
(*synchronized wrt. Keywords*)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   119
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
5952
7d4ec8992b23 added commands;
wenzelm
parents: 5923
diff changeset
   120
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   121
fun add_command name kind cmd = CRITICAL (fn () =>
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   122
 (Keyword.command name kind;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   123
  Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   124
   (if not (Symtab.defined commands name) then ()
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   125
    else warning ("Redefining outer syntax command " ^ quote name);
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   126
    Symtab.update (name, cmd) commands)))));
6722
5e82c7196789 added keyword classification;
wenzelm
parents: 6685
diff changeset
   127
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   128
in
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   129
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   130
fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
7789
57d20133224e verbatim markup tokens;
wenzelm
parents: 7774
diff changeset
   131
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   132
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   133
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   134
fun command name comment kind parse =
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   135
  add_command name kind (make_command comment NONE false parse);
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   136
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   137
fun markup_command markup name comment kind parse =
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   138
  add_command name kind (make_command comment (SOME markup) false parse);
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   139
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   140
fun improper_command name comment kind parse =
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   141
  add_command name kind (make_command comment NONE true parse);
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   142
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   143
fun internal_command name parse =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
   144
  command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   145
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   146
end;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   147
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   148
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   149
(* local_theory commands *)
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   150
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   151
fun local_theory_command do_print trans name comment kind parse =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
   152
  command name comment kind (Parse.opt_target -- parse
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   153
    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   154
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29315
diff changeset
   155
val local_theory' = local_theory_command false Toplevel.local_theory';
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   156
val local_theory = local_theory_command false Toplevel.local_theory;
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   157
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   158
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
26990
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   159
a91f7741967a added local_theory command wrappers;
wenzelm
parents: 26881
diff changeset
   160
24872
7fd1aa6671a4 report on keyword/command declarations;
wenzelm
parents: 24868
diff changeset
   161
(* inspect syntax *)
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   162
9223
eb752c2fac22 removed help;
wenzelm
parents: 9213
diff changeset
   163
fun print_outer_syntax () =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   164
  let
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   165
    val (keywords, outer_syntax) =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   166
      CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ())));
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26990
diff changeset
   167
    fun pretty_cmd (name, comment, _) =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   168
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   169
    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   170
  in
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   171
    [Pretty.strs ("syntax keywords:" :: map quote keywords),
18326
2f57579e618f tuned msg;
wenzelm
parents: 18064
diff changeset
   172
      Pretty.big_list "commands:" (map pretty_cmd cmds),
2f57579e618f tuned msg;
wenzelm
parents: 18064
diff changeset
   173
      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
9223
eb752c2fac22 removed help;
wenzelm
parents: 9213
diff changeset
   174
    |> Pretty.chunks |> Pretty.writeln
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6868
diff changeset
   175
  end;
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   176
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   177
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   178
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   179
(** toplevel parsing **)
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   180
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   181
(* basic sources *)
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6733
diff changeset
   182
26620
722cf4fdd4dd eliminated unused trace, read;
wenzelm
parents: 26611
diff changeset
   183
fun toplevel_source term do_recover cmd src =
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   184
  let
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   185
    val no_terminator =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   186
      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   187
    fun recover int =
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   188
      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   189
  in
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   190
    src
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   191
    |> Token.source_proper
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   192
    |> Source.source Token.stopper
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
   193
      (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   194
        (Option.map recover do_recover)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19060
diff changeset
   195
    |> Source.map_filter I
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   196
    |> Source.source Token.stopper
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33223
diff changeset
   197
        (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23679
diff changeset
   198
        (Option.map recover do_recover)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19060
diff changeset
   199
    |> Source.map_filter I
9132
52286129faa5 moved header stuff to thy_header.ML;
wenzelm
parents: 9056
diff changeset
   200
  end;
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   201
7746
b52c1a632e6a simplified;
wenzelm
parents: 7735
diff changeset
   202
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   203
(* off-line scanning/parsing *)
14925
0f86a8a694f8 added read (provides transition names and sources);
wenzelm
parents: 14687
diff changeset
   204
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   205
fun scan pos str =
16195
wenzelm
parents: 15989
diff changeset
   206
  Source.of_string str
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38422
diff changeset
   207
  |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   208
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
16195
wenzelm
parents: 15989
diff changeset
   209
  |> Source.exhaust;
wenzelm
parents: 15989
diff changeset
   210
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   211
fun parse pos str =
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   212
  Source.of_string str
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38422
diff changeset
   213
  |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   214
  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   215
  |> toplevel_source false NONE lookup_commands_dynamic
25580
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   216
  |> Source.exhaust;
6623674df897 added off-line parse;
wenzelm
parents: 25526
diff changeset
   217
14091
ad6ba9c55190 A patch by david aspinall
nipkow
parents: 12943
diff changeset
   218
26431
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
   219
(* process file *)
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
   220
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
   221
fun process_file path thy =
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
   222
  let
26881
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 26700
diff changeset
   223
    val trs = parse (Path.position path) (File.read path);
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 41484
diff changeset
   224
    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
28424
fc6ce1c4d5b7 simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents: 27872
diff changeset
   225
    val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
fc6ce1c4d5b7 simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents: 27872
diff changeset
   226
  in
fc6ce1c4d5b7 simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents: 27872
diff changeset
   227
    (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
fc6ce1c4d5b7 simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents: 27872
diff changeset
   228
      (true, Context.Theory thy') => thy'
fc6ce1c4d5b7 simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents: 27872
diff changeset
   229
    | _ => error "Bad result state: global theory expected")
fc6ce1c4d5b7 simplified process_file, eliminated Toplevel.excursion;
wenzelm
parents: 27872
diff changeset
   230
  end;
26431
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
   231
f1c79c00f1e4 added process_file;
wenzelm
parents: 26415
diff changeset
   232
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   233
(* interactive source of toplevel transformers *)
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   234
26600
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
   235
type isar =
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
   236
  (Toplevel.transition, (Toplevel.transition option,
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   237
    (Token.T, (Token.T option, (Token.T, (Token.T,
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30513
diff changeset
   238
      (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
27770
10d84e124a2f updated type of nested sources;
wenzelm
parents: 27720
diff changeset
   239
  Source.source) Source.source) Source.source) Source.source)
10d84e124a2f updated type of nested sources;
wenzelm
parents: 27720
diff changeset
   240
  Source.source) Source.source) Source.source) Source.source;
26600
f11515535c83 moved structure Isar to isar.ML;
wenzelm
parents: 26431
diff changeset
   241
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38236
diff changeset
   242
fun isar in_stream term : isar =
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38236
diff changeset
   243
  Source.tty in_stream
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38422
diff changeset
   244
  |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   245
  |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   246
  |> toplevel_source term (SOME true) lookup_commands_dynamic;
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   247
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24188
diff changeset
   248
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   249
(* prepare toplevel commands -- fail-safe *)
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   250
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   251
val not_singleton = "Exactly one command expected";
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   252
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   253
fun prepare_span outer_syntax span =
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   254
  let
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   255
    val commands = lookup_commands outer_syntax;
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 40523
diff changeset
   256
    val range_pos = Position.set_range (Thy_Syntax.span_range span);
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
   257
    val toks = Thy_Syntax.span_content span;
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
   258
    val _ = List.app Thy_Syntax.report_token toks;
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   259
  in
29311
4c830711e6f1 added type 'a parser, simplified signature;
wenzelm
parents: 28436
diff changeset
   260
    (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
37713
c82cf6e11669 Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents: 37216
diff changeset
   261
      [tr] =>
c82cf6e11669 Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents: 37216
diff changeset
   262
        if Keyword.is_control (Toplevel.name_of tr) then
c82cf6e11669 Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents: 37216
diff changeset
   263
          (Toplevel.malformed range_pos "Illegal control command", true)
c82cf6e11669 Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
wenzelm
parents: 37216
diff changeset
   264
        else (tr, true)
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   265
    | [] => (Toplevel.ignored range_pos, false)
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   266
    | _ => (Toplevel.malformed range_pos not_singleton, true))
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   267
    handle ERROR msg => (Toplevel.malformed range_pos msg, true)
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   268
  end;
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   269
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   270
fun prepare_element outer_syntax init {head, proof, proper_proof} =
28436
4faf705a177d load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents: 28432
diff changeset
   271
  let
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   272
    val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   273
    val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
28436
4faf705a177d load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents: 28432
diff changeset
   274
  in
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 42129
diff changeset
   275
    if proper_head andalso proper_proof then [(tr, proof_trs)]
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 42129
diff changeset
   276
    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
28436
4faf705a177d load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm
parents: 28432
diff changeset
   277
  end;
28432
944cb67f809a load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm
parents: 28424
diff changeset
   278
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   279
fun prepare_command pos str =
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   280
  let val (lexs, outer_syntax) = get_syntax () in
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
   281
    (case Thy_Syntax.parse_spans lexs pos str of
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   282
      [span] => #1 (prepare_span outer_syntax span)
27839
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   283
    | _ => Toplevel.malformed pos not_singleton)
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   284
  end;
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   285
0be8644c45eb Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27831
diff changeset
   286
26611
03455add4801 export load_thy -- no backpatching;
wenzelm
parents: 26600
diff changeset
   287
(* load_thy *)
7746
b52c1a632e6a simplified;
wenzelm
parents: 7735
diff changeset
   288
37977
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37953
diff changeset
   289
fun load_thy name init pos text =
7683
e74f43f1d8a3 export token_source;
wenzelm
parents: 7676
diff changeset
   290
  let
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   291
    val (lexs, outer_syntax) = get_syntax ();
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 41711
diff changeset
   292
    val time = ! Toplevel.timing;
23866
5295671034f8 moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents: 23796
diff changeset
   293
17932
677f7bec354e removed old-style theory format;
wenzelm
parents: 17412
diff changeset
   294
    val _ = Present.init_theory name;
27855
b1bf607e06c2 load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
wenzelm
parents: 27839
diff changeset
   295
37902
4e7864f3643d deps_thy/load_thy: store compact text to reduce space by factor 12;
wenzelm
parents: 37873
diff changeset
   296
    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
   297
    val spans = Source.exhaust (Thy_Syntax.span_source toks);
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 37977
diff changeset
   298
    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   299
    val elements =
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   300
      Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   301
      |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element outer_syntax init)
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   302
      |> flat;
23866
5295671034f8 moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents: 23796
diff changeset
   303
27855
b1bf607e06c2 load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
wenzelm
parents: 27839
diff changeset
   304
    val _ = Present.theory_source name
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36959
diff changeset
   305
      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
27855
b1bf607e06c2 load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
wenzelm
parents: 27839
diff changeset
   306
23866
5295671034f8 moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents: 23796
diff changeset
   307
    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 42129
diff changeset
   308
    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
23866
5295671034f8 moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents: 23796
diff changeset
   309
    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
29428
3ab54b42ded8 load_thy: explicit after_load phase for presentation;
wenzelm
parents: 29380
diff changeset
   310
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   311
    val present =
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   312
      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   313
        deps = map Future.task_of results, pri = 0})
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   314
      (fn () =>
43711
608d1b451f67 less stateful outer_syntax;
wenzelm
parents: 43621
diff changeset
   315
        Thy_Output.present_thy (#1 lexs) Keyword.command_tags (is_markup outer_syntax)
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   316
          (maps Future.join results) toks
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   317
        |> Buffer.content
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   318
        |> Present.theory_output name);
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   319
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   320
  in (thy, present) end;
23866
5295671034f8 moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents: 23796
diff changeset
   321
5829
0acb30dd92bc The global Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   322
end;
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
   323