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