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