src/Pure/PIDE/command.ML
author wenzelm
Fri, 09 Oct 2015 21:16:00 +0200
changeset 61379 c57820ceead3
parent 61213 0b1a092385c7
child 61457 3e21699bb83b
permissions -rw-r--r--
more direct HTML presentation, without print mode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/PIDE/command.ML
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     3
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
     4
Prover command execution: read -- eval -- print.
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     5
*)
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     6
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     7
signature COMMAND =
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
     8
sig
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56447
diff changeset
     9
  type blob = (string * (SHA1.digest * string list) option) Exn.result
54526
92961f196d9e load files that are not provided by PIDE blobs;
wenzelm
parents: 54523
diff changeset
    10
  val read_file: Path.T -> Position.T -> Path.T -> Token.file
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
    11
  val read_thy: Toplevel.state -> theory
58934
385a4cc7426f prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents: 58928
diff changeset
    12
  val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    13
    blob list * int -> Token.T list -> Toplevel.transition
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    14
  type eval
52607
33a133d50616 clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents: 52606
diff changeset
    15
  val eval_eq: eval * eval -> bool
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    16
  val eval_running: eval -> bool
52772
7764c90680f0 clarified conditions for node traversal;
wenzelm
parents: 52762
diff changeset
    17
  val eval_finished: eval -> bool
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    18
  val eval_result_state: eval -> Toplevel.state
58934
385a4cc7426f prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents: 58928
diff changeset
    19
  val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    20
    blob list * int -> Token.T list -> eval -> eval
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    21
  type print
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
    22
  val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
    23
    eval -> print list -> print list option
52526
d234cb6b60e3 more Command.memo operations;
wenzelm
parents: 52516
diff changeset
    24
  type print_fn = Toplevel.transition -> Toplevel.state -> unit
52953
2c927b7501c5 explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents: 52853
diff changeset
    25
  type print_function =
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
    26
    {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
52953
2c927b7501c5 explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents: 52853
diff changeset
    27
      {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
2c927b7501c5 explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents: 52853
diff changeset
    28
  val print_function: string -> print_function -> unit
52571
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
    29
  val no_print_function: string -> unit
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    30
  type exec = eval * print list
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    31
  val no_exec: exec
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    32
  val exec_ids: exec option -> Document_ID.exec list
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    33
  val exec: Document_ID.execution -> exec -> unit
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    34
end;
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    35
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    36
structure Command: COMMAND =
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    37
struct
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    38
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    39
(** main phases of execution **)
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    40
59466
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    41
fun task_context group f =
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    42
  f
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    43
  |> Future.interruptible_task
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    44
  |> Future.task_context "Command.run_process" group;
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    45
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    46
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
    47
(* read *)
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
    48
55798
985bd3a325ab tuned signature;
wenzelm
parents: 55788
diff changeset
    49
type blob =
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56447
diff changeset
    50
  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 53976
diff changeset
    51
56504
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    52
fun read_file_node file_node master_dir pos src_path =
54526
92961f196d9e load files that are not provided by PIDE blobs;
wenzelm
parents: 54523
diff changeset
    53
  let
59944
83071f4c8ae6 recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
wenzelm
parents: 59809
diff changeset
    54
    val _ = Position.report pos Markup.language_path;
56504
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    55
    val _ =
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    56
      (case try Url.explode file_node of
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    57
        NONE => ()
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    58
      | SOME (Url.File _) => ()
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    59
      | _ =>
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    60
          error ("Prover cannot load remote file " ^
59685
c043306d2598 clarified markup for embedded files, early before execution;
wenzelm
parents: 59472
diff changeset
    61
            Markup.markup (Markup.path file_node) (quote file_node)));
54526
92961f196d9e load files that are not provided by PIDE blobs;
wenzelm
parents: 54523
diff changeset
    62
    val full_path = File.check_file (File.full_path master_dir src_path);
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    63
    val text = File.read full_path;
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    64
    val lines = split_lines text;
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    65
    val digest = SHA1.digest text;
59685
c043306d2598 clarified markup for embedded files, early before execution;
wenzelm
parents: 59472
diff changeset
    66
  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
c043306d2598 clarified markup for embedded files, early before execution;
wenzelm
parents: 59472
diff changeset
    67
  handle ERROR msg => error (msg ^ Position.here pos);
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    68
56504
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    69
val read_file = read_file_node "";
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    70
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    71
local
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    72
56447
1e77ed11f2f7 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents: 56333
diff changeset
    73
fun blob_file src_path lines digest file_node =
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    74
  let
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    75
    val file_pos =
56447
1e77ed11f2f7 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents: 56333
diff changeset
    76
      Position.file file_node |>
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    77
      (case Position.get_id (Position.thread_data ()) of
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    78
        NONE => I
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    79
      | SOME exec_id => Position.put_id exec_id);
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
    80
  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
54526
92961f196d9e load files that are not provided by PIDE blobs;
wenzelm
parents: 54523
diff changeset
    81
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    82
fun resolve_files keywords master_dir (blobs, blobs_index) toks =
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57844
diff changeset
    83
  (case Outer_Syntax.parse_spans toks of
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    84
    [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    85
      (case try (nth toks) blobs_index of
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    86
        SOME tok =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    87
          let
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    88
            val pos = Token.pos_of tok;
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    89
            val path = Path.explode (Token.content_of tok)
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    90
              handle ERROR msg => error (msg ^ Position.here pos);
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    91
            fun make_file src_path (Exn.Res (file_node, NONE)) =
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    92
                  Exn.interruptible_capture (fn () =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    93
                    read_file_node file_node master_dir pos src_path) ()
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    94
              | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
60027
c42d65e11b6e clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
wenzelm
parents: 59944
diff changeset
    95
                  (Position.report pos Markup.language_path;
c42d65e11b6e clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
wenzelm
parents: 59944
diff changeset
    96
                    Exn.Res (blob_file src_path lines digest file_node))
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    97
              | make_file _ (Exn.Exn e) = Exn.Exn e;
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    98
            val src_paths = Keyword.command_files keywords cmd path;
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    99
            val files =
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   100
              if null blobs then
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   101
                map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   102
              else if length src_paths = length blobs then
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   103
                map2 make_file src_paths blobs
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   104
              else error ("Misalignment of inlined files" ^ Position.here pos);
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   105
          in
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   106
            toks |> map_index (fn (i, tok) =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   107
              if i = blobs_index then Token.put_files files tok else tok)
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   108
          end
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   109
      | NONE => toks)
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 53976
diff changeset
   110
  | _ => toks);
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 53976
diff changeset
   111
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   112
fun reports_of_token keywords tok =
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   113
  let
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   114
    val malformed_symbols =
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   115
      Input.source_explode (Token.input_of tok)
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   116
      |> map_filter (fn (sym, pos) =>
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   117
          if Symbol.is_malformed sym
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   118
          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   119
    val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   120
    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   121
  in (is_malformed, reports) end;
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   122
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
   123
in
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
   124
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 60076
diff changeset
   125
fun read_thy st = Toplevel.theory_of st
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 60076
diff changeset
   126
  handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy;
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
   127
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   128
fun read keywords thy master_dir init blobs_info span =
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   129
  let
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
   130
    val command_reports = Outer_Syntax.command_reports thy;
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   131
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   132
    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   133
    val pos =
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   134
      (case find_first Token.is_command span of
55708
f4b114070675 tuned signature;
wenzelm
parents: 55429
diff changeset
   135
        SOME tok => Token.pos_of tok
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   136
      | NONE => #1 proper_range);
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   137
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   138
    val token_reports = map (reports_of_token keywords) span;
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   139
    val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   140
  in
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   141
    if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   142
    else
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   143
      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
58853
f8715e7c1be6 discontinued obsolete control command category;
wenzelm
parents: 57905
diff changeset
   144
        [tr] => Toplevel.modify_init init tr
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   145
      | [] => Toplevel.ignored (#1 (Token.range_of span))
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   146
      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   147
      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   148
  end;
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   149
55788
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
   150
end;
67699e08e969 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents: 55709
diff changeset
   151
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   152
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   153
(* eval *)
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   154
59472
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   155
type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   156
val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel};
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   157
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   158
datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   159
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   160
fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58934
diff changeset
   161
val eval_eq = op = o apply2 eval_exec_id;
52607
33a133d50616 clarified execution: maintain running execs only, check "stable" separately via memo (again);
wenzelm
parents: 52606
diff changeset
   162
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   163
val eval_running = Execution.is_running_exec o eval_exec_id;
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   164
fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
52772
7764c90680f0 clarified conditions for node traversal;
wenzelm
parents: 52762
diff changeset
   165
59466
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
   166
fun eval_result (Eval {eval_process, ...}) =
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
   167
  task_context (Future.worker_subgroup ()) Lazy.force eval_process;
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
   168
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   169
val eval_result_state = #state o eval_result;
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   170
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   171
local
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   172
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   173
fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () =>
56937
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   174
  let
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   175
    val name = Toplevel.name_of tr;
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   176
    val res =
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   177
      if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   178
      else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
56937
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   179
      else NONE;
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   180
  in
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   181
    (case res of
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   182
      NONE => st0
60076
e24f59cba23c tuned messages;
wenzelm
parents: 60027
diff changeset
   183
    | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st))
56937
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   184
  end) ();
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   185
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   186
fun run keywords int tr st =
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   187
  if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 53189
diff changeset
   188
    (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
51605
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51603
diff changeset
   189
      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
51284
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51266
diff changeset
   190
  else Toplevel.command_errors int tr st;
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   191
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   192
fun check_cmts span tr st' =
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   193
  Toplevel.setmp_thread_position tr
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   194
    (fn () =>
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   195
      Outer_Syntax.side_comments span |> maps (fn cmt =>
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59689
diff changeset
   196
        (Thy_Output.check_text (Token.input_of cmt) st'; [])
52619
70d5f2f7d27f reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents: 52609
diff changeset
   197
          handle exn =>
70d5f2f7d27f reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents: 52609
diff changeset
   198
            if Exn.is_interrupt exn then reraise exn
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56292
diff changeset
   199
            else Runtime.exn_messages_ids exn)) ();
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   200
54678
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54671
diff changeset
   201
fun report tr m =
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 56303
diff changeset
   202
  Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
54678
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54671
diff changeset
   203
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54671
diff changeset
   204
fun status tr m =
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54671
diff changeset
   205
  Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54671
diff changeset
   206
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   207
fun proof_status tr st =
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   208
  (case try Toplevel.proof_of st of
54678
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54671
diff changeset
   209
    SOME prf => status tr (Proof.status_markup prf)
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   210
  | NONE => ());
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   211
59472
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   212
fun eval_state keywords span tr ({state, ...}: eval_state) =
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   213
  let
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   214
    val _ = Multithreading.interrupted ();
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   215
59472
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   216
    val st = reset_state keywords tr state;
56937
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   217
59472
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   218
    val _ = status tr Markup.running;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   219
    val (errs1, result) = run keywords true tr st;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   220
    val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   221
    val errs = errs1 @ errs2;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   222
    val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   223
  in
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   224
    (case result of
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   225
      NONE =>
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   226
        let
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   227
          val _ = status tr Markup.failed;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   228
          val _ = status tr Markup.finished;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   229
          val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   230
        in {failed = true, command = tr, state = st} end
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   231
    | SOME st' =>
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   232
        let
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   233
          val _ = proof_status tr st';
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   234
          val _ = status tr Markup.finished;
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   235
        in {failed = false, command = tr, state = st'} end)
513300fa2d09 discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
wenzelm
parents: 59466
diff changeset
   236
  end;
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   237
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   238
in
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   239
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   240
fun eval keywords master_dir init blobs_info span eval0 =
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   241
  let
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   242
    val exec_id = Document_ID.make ();
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   243
    fun process () =
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   244
      let
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
   245
        val eval_state0 = eval_result eval0;
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
   246
        val thy = read_thy (#state eval_state0);
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   247
        val tr =
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   248
          Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   249
            (fn () =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   250
              read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
58934
385a4cc7426f prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
wenzelm
parents: 58928
diff changeset
   251
      in eval_state keywords span tr eval_state0 end;
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   252
  in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   253
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   254
end;
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   255
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   256
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   257
(* print *)
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   258
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   259
datatype print = Print of
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   260
 {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   261
  exec_id: Document_ID.exec, print_process: unit lazy};
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   262
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   263
fun print_exec_id (Print {exec_id, ...}) = exec_id;
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58934
diff changeset
   264
val print_eq = op = o apply2 print_exec_id;
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   265
52526
d234cb6b60e3 more Command.memo operations;
wenzelm
parents: 52516
diff changeset
   266
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
52515
0dcadc90550b more print function parameters;
wenzelm
parents: 52511
diff changeset
   267
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   268
type print_function =
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   269
  {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
52953
2c927b7501c5 explicit "strict" flag for print functions (flipped internal meaning);
wenzelm
parents: 52853
diff changeset
   270
    {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   271
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   272
local
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   273
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   274
val print_functions =
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   275
  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   276
56265
785569927666 discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents: 56034
diff changeset
   277
fun print_error tr opt_context e =
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56292
diff changeset
   278
  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
52619
70d5f2f7d27f reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents: 52609
diff changeset
   279
    handle exn =>
70d5f2f7d27f reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents: 52609
diff changeset
   280
      if Exn.is_interrupt exn then reraise exn
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 56303
diff changeset
   281
      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
52516
b5b3c888df9f more exception handling -- make print functions total;
wenzelm
parents: 52515
diff changeset
   282
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   283
fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
52656
9437f440ef3f keep persistent prints only if actually finished;
wenzelm
parents: 52651
diff changeset
   284
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   285
fun print_persistent (Print {persistent, ...}) = persistent;
52596
40298d383463 global management of command execution fragments;
wenzelm
parents: 52586
diff changeset
   286
52853
4ab66773a41f prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents: 52850
diff changeset
   287
val overlay_ord = prod_ord string_ord (list_ord string_ord);
4ab66773a41f prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents: 52850
diff changeset
   288
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   289
in
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   290
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   291
fun print command_visible command_overlays keywords command_name eval old_prints =
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   292
  let
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   293
    val print_functions = Synchronized.value print_functions;
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   294
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   295
    fun make_print name args {delay, pri, persistent, strict, print_fn} =
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   296
      let
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   297
        val exec_id = Document_ID.make ();
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   298
        fun process () =
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   299
          let
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   300
            val {failed, command, state = st', ...} = eval_result eval;
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   301
            val tr = Toplevel.exec_id exec_id command;
56265
785569927666 discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents: 56034
diff changeset
   302
            val opt_context = try Toplevel.generic_theory_of st';
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   303
          in
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   304
            if failed andalso strict then ()
56265
785569927666 discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents: 56034
diff changeset
   305
            else print_error tr opt_context (fn () => print_fn tr st')
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   306
          end;
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   307
      in
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   308
        Print {
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   309
          name = name, args = args, delay = delay, pri = pri, persistent = persistent,
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   310
          exec_id = exec_id, print_process = Lazy.lazy process}
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   311
      end;
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   312
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   313
    fun bad_print name args exn =
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   314
      make_print name args {delay = NONE, pri = 0, persistent = false,
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   315
        strict = false, print_fn = fn _ => fn _ => reraise exn};
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   316
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   317
    fun new_print name args get_pr =
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   318
      let
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   319
        val params =
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   320
         {keywords = keywords,
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   321
          command_name = command_name,
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   322
          args = args,
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   323
          exec_id = eval_exec_id eval};
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   324
      in
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56292
diff changeset
   325
        (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   326
          Exn.Res NONE => NONE
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   327
        | Exn.Res (SOME pr) => SOME (make_print name args pr)
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   328
        | Exn.Exn exn => SOME (bad_print name args exn))
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   329
      end;
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   330
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   331
    fun get_print (a, b) =
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   332
      (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   333
        NONE =>
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   334
          (case AList.lookup (op =) print_functions a of
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   335
            NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a)))
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   336
          | SOME get_pr => new_print a b get_pr)
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   337
      | some => some);
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   338
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   339
    val new_prints =
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   340
      if command_visible then
52853
4ab66773a41f prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents: 52850
diff changeset
   341
        fold (fn (a, _) => cons (a, [])) print_functions command_overlays
4ab66773a41f prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents: 52850
diff changeset
   342
        |> sort_distinct overlay_ord
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   343
        |> map_filter get_print
52656
9437f440ef3f keep persistent prints only if actually finished;
wenzelm
parents: 52651
diff changeset
   344
      else filter (fn print => print_finished print andalso print_persistent print) old_prints;
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   345
  in
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   346
    if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   347
  end;
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   348
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   349
fun print_function name f =
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   350
  Synchronized.change print_functions (fn funs =>
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   351
   (if not (AList.defined (op =) funs name) then ()
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   352
    else warning ("Redefining command print function: " ^ quote name);
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   353
    AList.update (op =) (name, f) funs));
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   354
52571
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
   355
fun no_print_function name =
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
   356
  Synchronized.change print_functions (filter_out (equal name o #1));
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
   357
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   358
end;
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   359
52526
d234cb6b60e3 more Command.memo operations;
wenzelm
parents: 52516
diff changeset
   360
val _ =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   361
  print_function "Execution.print"
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   362
    (fn {args, exec_id, ...} =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   363
      if null args then
60610
f52b4b0c10c4 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents: 60095
diff changeset
   364
        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false,
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   365
          print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   366
      else NONE);
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   367
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   368
val _ =
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   369
  print_function "print_state"
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   370
    (fn {keywords, command_name, ...} =>
61213
0b1a092385c7 option editor_output_state;
wenzelm
parents: 61208
diff changeset
   371
      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
0b1a092385c7 option editor_output_state;
wenzelm
parents: 61208
diff changeset
   372
      then
60610
f52b4b0c10c4 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents: 60095
diff changeset
   373
        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
61208
19118f9b939d separate panel for proof state output;
wenzelm
parents: 60610
diff changeset
   374
          print_fn = fn _ => fn st =>
19118f9b939d separate panel for proof state output;
wenzelm
parents: 60610
diff changeset
   375
            if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
19118f9b939d separate panel for proof state output;
wenzelm
parents: 60610
diff changeset
   376
            else ()}
56895
f058120aaad4 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents: 56887
diff changeset
   377
      else NONE);
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   378
52532
c81d76f7f63d tuned signature;
wenzelm
parents: 52530
diff changeset
   379
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   380
(* combined execution *)
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   381
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   382
type exec = eval * print list;
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   383
val no_exec: exec =
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   384
  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []);
52532
c81d76f7f63d tuned signature;
wenzelm
parents: 52530
diff changeset
   385
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   386
fun exec_ids NONE = []
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   387
  | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   388
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   389
local
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   390
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   391
fun run_process execution_id exec_id process =
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   392
  let val group = Future.worker_subgroup () in
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   393
    if Execution.running execution_id exec_id [group] then
59466
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
   394
      ignore (task_context group Lazy.force_result process)
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   395
    else ()
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   396
  end;
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   397
59328
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   398
fun ignore_process process =
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   399
  Lazy.is_running process orelse Lazy.is_finished process;
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   400
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   401
fun run_eval execution_id (Eval {exec_id, eval_process}) =
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   402
  if Lazy.is_finished eval_process then ()
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   403
  else run_process execution_id exec_id eval_process;
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   404
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   405
fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
59328
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   406
  if ignore_process print_process then ()
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   407
  else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
56875
f6259d6fb565 explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents: 56504
diff changeset
   408
  then
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   409
    let
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   410
      val group = Future.worker_subgroup ();
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   411
      fun fork () =
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   412
        ignore ((singleton o Future.forks)
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   413
          {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
59328
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   414
          (fn () =>
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   415
            if ignore_process print_process then ()
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   416
            else run_process execution_id exec_id print_process));
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   417
    in
52762
c2a6e220f157 tuned signature;
wenzelm
parents: 52761
diff changeset
   418
      (case delay of
c2a6e220f157 tuned signature;
wenzelm
parents: 52761
diff changeset
   419
        NONE => fork ()
c2a6e220f157 tuned signature;
wenzelm
parents: 52761
diff changeset
   420
      | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   421
    end
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   422
  else run_process execution_id exec_id print_process;
52559
ddaf277e0d8c more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents: 52536
diff changeset
   423
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   424
in
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   425
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   426
fun exec execution_id (eval, prints) =
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59188
diff changeset
   427
  (run_eval execution_id eval; List.app (run_print execution_id) prints);
52532
c81d76f7f63d tuned signature;
wenzelm
parents: 52530
diff changeset
   428
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   429
end;
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   430
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   431
end;
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   432