src/Pure/PIDE/command.ML
author wenzelm
Wed, 06 Apr 2016 23:45:19 +0200
changeset 62895 54c2abe7e9a4
parent 62826 eb94e570c1a4
child 62924 ce47945ce4fb
permissions -rw-r--r--
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
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
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
    31
  val init_exec: theory option -> exec
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    32
  val no_exec: exec
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
    33
  val exec_ids: exec option -> Document_ID.exec list
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    34
  val exec: Document_ID.execution -> exec -> unit
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    35
end;
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    36
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    37
structure Command: COMMAND =
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    38
struct
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
    39
52536
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    40
(** main phases of execution **)
3a35ce87a55c tuned signature;
wenzelm
parents: 52535
diff changeset
    41
59466
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    42
fun task_context group f =
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    43
  f
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    44
  |> Future.interruptible_task
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    45
  |> Future.task_context "Command.run_process" group;
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    46
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
    47
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
    48
(* read *)
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
    49
55798
985bd3a325ab tuned signature;
wenzelm
parents: 55788
diff changeset
    50
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
    51
  (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
    52
56504
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    53
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
    54
  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
    55
    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
    56
    val _ =
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    57
      (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
    58
        NONE => ()
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    59
      | SOME (Url.File _) => ()
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    60
      | _ =>
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    61
          error ("Prover cannot load remote file " ^
59685
c043306d2598 clarified markup for embedded files, early before execution;
wenzelm
parents: 59472
diff changeset
    62
            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
    63
    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
    64
    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
    65
    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
    66
    val digest = SHA1.digest text;
59685
c043306d2598 clarified markup for embedded files, early before execution;
wenzelm
parents: 59472
diff changeset
    67
  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
    68
  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
    69
56504
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    70
val read_file = read_file_node "";
d71f4be7e287 tuned error -- allow user to click on hyperlink to open remote file;
wenzelm
parents: 56458
diff changeset
    71
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
    72
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
    73
56447
1e77ed11f2f7 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
wenzelm
parents: 56333
diff changeset
    74
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
    75
  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
    76
    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
    77
      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
    78
      (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
    79
        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
    80
      | 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
    81
  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
    82
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    83
fun resolve_files keywords master_dir (blobs, blobs_index) toks =
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 57844
diff changeset
    84
  (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
    85
    [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
    86
      (case try (nth toks) blobs_index of
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    87
        SOME tok =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    88
          let
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    89
            val pos = Token.pos_of tok;
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    90
            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
    91
              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
    92
            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
    93
                  Exn.interruptible_capture (fn () =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
    94
                    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
    95
              | 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
    96
                  (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
    97
                    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
    98
              | 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
    99
            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
   100
            val files =
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   101
              if null blobs then
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   102
                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
   103
              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
   104
                map2 make_file src_paths blobs
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   105
              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
   106
          in
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   107
            toks |> map_index (fn (i, tok) =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   108
              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
   109
          end
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   110
      | NONE => toks)
54519
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 53976
diff changeset
   111
  | _ => toks);
5fed81762406 maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents: 53976
diff changeset
   112
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   113
fun reports_of_token keywords tok =
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   114
  let
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   115
    val malformed_symbols =
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   116
      Input.source_explode (Token.input_of tok)
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   117
      |> map_filter (fn (sym, pos) =>
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   118
          if Symbol.is_malformed sym
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   119
          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   120
    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
   121
    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
   122
  in (is_malformed, reports) end;
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   123
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
   124
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
   125
60095
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 60076
diff changeset
   126
fun read_thy st = Toplevel.theory_of st
35f626b11422 more explicit bootstrap_thy;
wenzelm
parents: 60076
diff changeset
   127
  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
   128
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   129
fun read keywords thy master_dir init blobs_info span =
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   130
  let
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
   131
    val command_reports = Outer_Syntax.command_reports thy;
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   132
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   133
    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   134
    val pos =
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   135
      (case find_first Token.is_command span of
55708
f4b114070675 tuned signature;
wenzelm
parents: 55429
diff changeset
   136
        SOME tok => Token.pos_of tok
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   137
      | NONE => #1 proper_range);
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   138
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   139
    val token_reports = map (reports_of_token keywords) span;
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   140
    val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   141
  in
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61213
diff changeset
   142
    if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   143
    else
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   144
      (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
   145
        [tr] => Toplevel.modify_init init tr
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   146
      | [] => Toplevel.ignored (#1 (Token.range_of span))
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   147
      | _ => 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
   148
      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   149
  end;
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   150
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
   151
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
   152
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   153
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   154
(* eval *)
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   155
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
   156
type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   157
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   158
fun init_eval_state opt_thy =
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   159
 {failed = false,
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   160
  command = Toplevel.empty,
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   161
  state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   162
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
   163
datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   164
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   165
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
   166
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
   167
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   168
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
   169
fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
52772
7764c90680f0 clarified conditions for node traversal;
wenzelm
parents: 52762
diff changeset
   170
59466
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
   171
fun eval_result (Eval {eval_process, ...}) =
6fab87db556c ensure that running into older execution is interruptible (see also b91dc7ab3464);
wenzelm
parents: 59348
diff changeset
   172
  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
   173
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   174
val eval_result_state = #state o eval_result;
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   175
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   176
local
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   177
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   178
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
   179
  let
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   180
    val name = Toplevel.name_of tr;
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   181
    val res =
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   182
      if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   183
      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
   184
      else NONE;
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   185
  in
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   186
    (case res of
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   187
      NONE => st0
60076
e24f59cba23c tuned messages;
wenzelm
parents: 60027
diff changeset
   188
    | 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
   189
  end) ();
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   190
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   191
fun run keywords int tr st =
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   192
  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
   193
    (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
   194
      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
51284
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51266
diff changeset
   195
  else Toplevel.command_errors int tr st;
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   196
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   197
fun check_cmts span tr st' =
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   198
  Toplevel.setmp_thread_position tr
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   199
    (fn () =>
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   200
      Outer_Syntax.side_comments span |> maps (fn cmt =>
61457
3e21699bb83b clarified Antiquote.antiq_reports;
wenzelm
parents: 61379
diff changeset
   201
        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
52619
70d5f2f7d27f reraise interrupts outside command regular transactions -- relevant for memo_stable;
wenzelm
parents: 52609
diff changeset
   202
          handle exn =>
62505
9e2a65912111 clarified modules;
wenzelm
parents: 61457
diff changeset
   203
            if Exn.is_interrupt exn then Exn.reraise exn
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56292
diff changeset
   204
            else Runtime.exn_messages_ids exn)) ();
52510
a4a102237ded tuned signature;
wenzelm
parents: 52509
diff changeset
   205
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
   206
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
   207
  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
   208
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
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
   210
  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
   211
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   212
fun proof_status tr st =
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   213
  (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
   214
    SOME prf => status tr (Proof.status_markup prf)
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   215
  | NONE => ());
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   216
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
   217
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
   218
  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
   219
    val _ = Multithreading.interrupted ();
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   220
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
   221
    val st = reset_state keywords tr state;
56937
d11d11da0d90 smarter recovery from toplevel type error;
wenzelm
parents: 56896
diff changeset
   222
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
   223
    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
   224
    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
   225
    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
   226
    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
   227
    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
   228
  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
   229
    (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
   230
      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
   231
        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
   232
          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
   233
          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
   234
          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
   235
        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
   236
    | 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
   237
        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
   238
          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
   239
          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
   240
        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
   241
  end;
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   242
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   243
in
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   244
59689
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   245
fun eval keywords master_dir init blobs_info span eval0 =
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   246
  let
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   247
    val exec_id = Document_ID.make ();
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   248
    fun process () =
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   249
      let
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58923
diff changeset
   250
        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
   251
        val thy = read_thy (#state eval_state0);
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   252
        val tr =
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   253
          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
   254
            (fn () =>
7968c57ea240 simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents: 59685
diff changeset
   255
              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
   256
      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
   257
  in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
52534
341ae9cd4743 tuned signature;
wenzelm
parents: 52533
diff changeset
   258
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   259
end;
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   260
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   261
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   262
(* print *)
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   263
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   264
datatype print = Print of
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   265
 {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
   266
  exec_id: Document_ID.exec, print_process: unit lazy};
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   267
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   268
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
   269
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
   270
52526
d234cb6b60e3 more Command.memo operations;
wenzelm
parents: 52516
diff changeset
   271
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
52515
0dcadc90550b more print function parameters;
wenzelm
parents: 52511
diff changeset
   272
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   273
type print_function =
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   274
  {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
   275
    {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
   276
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   277
local
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   278
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   279
val print_functions =
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   280
  Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   281
56265
785569927666 discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents: 56034
diff changeset
   282
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
   283
  (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
   284
    handle exn =>
62505
9e2a65912111 clarified modules;
wenzelm
parents: 61457
diff changeset
   285
      if Exn.is_interrupt exn then Exn.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
   286
      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
   287
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
   288
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
   289
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   290
fun print_persistent (Print {persistent, ...}) = persistent;
52596
40298d383463 global management of command execution fragments;
wenzelm
parents: 52586
diff changeset
   291
52853
4ab66773a41f prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents: 52850
diff changeset
   292
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
   293
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   294
in
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   295
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   296
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
   297
  let
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   298
    val print_functions = Synchronized.value print_functions;
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   299
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   300
    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
   301
      let
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   302
        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
   303
        fun process () =
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   304
          let
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   305
            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
   306
            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
   307
            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
   308
          in
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   309
            if failed andalso strict then ()
56265
785569927666 discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents: 56034
diff changeset
   310
            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
   311
          end;
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   312
      in
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   313
        Print {
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   314
          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
   315
          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
   316
      end;
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   317
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   318
    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
   319
      make_print name args {delay = NONE, pri = 0, persistent = false,
62505
9e2a65912111 clarified modules;
wenzelm
parents: 61457
diff changeset
   320
        strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
52999
1f09c98a3232 more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;
wenzelm
parents: 52953
diff changeset
   321
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   322
    fun new_print name args get_pr =
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   323
      let
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   324
        val params =
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   325
         {keywords = keywords,
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   326
          command_name = command_name,
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   327
          args = args,
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   328
          exec_id = eval_exec_id eval};
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   329
      in
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56292
diff changeset
   330
        (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
   331
          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
   332
        | 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
   333
        | Exn.Exn exn => SOME (bad_print name args exn))
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   334
      end;
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   335
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   336
    fun get_print (a, b) =
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   337
      (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
   338
        NONE =>
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   339
          (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
   340
            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
   341
          | 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
   342
      | some => some);
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   343
52570
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   344
    val new_prints =
26d84a0b9209 clarified Command.print: update old prints here;
wenzelm
parents: 52566
diff changeset
   345
      if command_visible then
52853
4ab66773a41f prefer canonical order, to avoid potential fluctuation due to front-end edits;
wenzelm
parents: 52850
diff changeset
   346
        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
   347
        |> sort_distinct overlay_ord
52850
9fff9f78240a support print functions with explicit arguments, as provided by overlays;
wenzelm
parents: 52785
diff changeset
   348
        |> map_filter get_print
52656
9437f440ef3f keep persistent prints only if actually finished;
wenzelm
parents: 52651
diff changeset
   349
      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
   350
  in
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   351
    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
   352
  end;
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   353
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   354
fun print_function name f =
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   355
  Synchronized.change print_functions (fn funs =>
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   356
   (if not (AList.defined (op =) funs name) then ()
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   357
    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
   358
    AList.update (op =) (name, f) funs));
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   359
52571
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
   360
fun no_print_function name =
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
   361
  Synchronized.change print_functions (filter_out (equal name o #1));
344527354323 allow to remove print functions;
wenzelm
parents: 52570
diff changeset
   362
52511
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   363
end;
d5d2093ff224 allow multiple print functions;
wenzelm
parents: 52510
diff changeset
   364
52526
d234cb6b60e3 more Command.memo operations;
wenzelm
parents: 52516
diff changeset
   365
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
   366
  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
   367
    (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
   368
      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
   369
        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
   370
          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
   371
      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
   372
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 56265
diff changeset
   373
val _ =
52647
45ce95b8bf69 determine print function parameters dynamically, e.g. depending on runtime options;
wenzelm
parents: 52619
diff changeset
   374
  print_function "print_state"
58923
cb9b69cca999 more explicit Keyword.keywords;
wenzelm
parents: 58862
diff changeset
   375
    (fn {keywords, command_name, ...} =>
61213
0b1a092385c7 option editor_output_state;
wenzelm
parents: 61208
diff changeset
   376
      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
0b1a092385c7 option editor_output_state;
wenzelm
parents: 61208
diff changeset
   377
      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
   378
        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
   379
          print_fn = fn _ => fn st =>
19118f9b939d separate panel for proof state output;
wenzelm
parents: 60610
diff changeset
   380
            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
   381
            else ()}
56895
f058120aaad4 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents: 56887
diff changeset
   382
      else NONE);
52509
2193d2c7f586 tuned signature;
wenzelm
parents: 51605
diff changeset
   383
52532
c81d76f7f63d tuned signature;
wenzelm
parents: 52530
diff changeset
   384
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   385
(* combined execution *)
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   386
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   387
type exec = eval * print list;
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   388
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   389
fun init_exec opt_thy : exec =
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   390
  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []);
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   391
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62826
diff changeset
   392
val no_exec = init_exec NONE;
52532
c81d76f7f63d tuned signature;
wenzelm
parents: 52530
diff changeset
   393
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   394
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
   395
  | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   396
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   397
local
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   398
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
   399
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
   400
  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
   401
    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
   402
      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
   403
    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
   404
  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
   405
59328
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   406
fun ignore_process process =
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   407
  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
   408
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
   409
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
   410
  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
   411
  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
   412
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
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
   414
  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
   415
  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
   416
  then
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   417
    let
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   418
      val group = Future.worker_subgroup ();
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   419
      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
   420
        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
   421
          {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
   422
          (fn () =>
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   423
            if ignore_process print_process then ()
b83d6c3c439a ignore print process even after fork, to avoid loosing active worker threads;
wenzelm
parents: 59193
diff changeset
   424
            else run_process execution_id exec_id print_process));
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   425
    in
52762
c2a6e220f157 tuned signature;
wenzelm
parents: 52761
diff changeset
   426
      (case delay of
c2a6e220f157 tuned signature;
wenzelm
parents: 52761
diff changeset
   427
        NONE => fork ()
62826
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 62505
diff changeset
   428
      | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
52651
5adb5c69af97 initial delay for automatically tried tools;
wenzelm
parents: 52647
diff changeset
   429
    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
   430
  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
   431
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   432
in
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   433
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
   434
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
   435
  (run_eval execution_id eval; List.app (run_print execution_id) prints);
52532
c81d76f7f63d tuned signature;
wenzelm
parents: 52530
diff changeset
   436
47336
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   437
end;
bed4b2738d8a separate module for prover command execution;
wenzelm
parents:
diff changeset
   438
52600
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   439
end;
75afb82daf5c more abstract types;
wenzelm
parents: 52598
diff changeset
   440