src/Pure/System/isabelle_process.ML
author wenzelm
Thu, 06 Aug 2020 22:54:22 +0200
changeset 72104 d9a42786fbc9
parent 71878 3cd8449829fa
child 72112 3546dd4ade74
permissions -rw-r--r--
more thorough cleanup, e.g. before ML_Heap.save;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29522
diff changeset
     1
(*  Title:      Pure/System/isabelle_process.ML
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
     3
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57913
diff changeset
     4
Isabelle process wrapper.
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
     5
*)
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
     6
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
     7
signature ISABELLE_PROCESS =
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
     8
sig
42897
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
     9
  val is_active: unit -> bool
71878
3cd8449829fa clarified signature;
wenzelm
parents: 71675
diff changeset
    10
  exception STOP of int
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    11
  val protocol_command: string -> (string list -> unit) -> unit
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    12
  val reset_tracing: Document_ID.exec -> unit
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    13
  val crashes: exn list Synchronized.var
62563
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
    14
  val init_options: unit -> unit
65300
c262653a3b88 clarified signature;
wenzelm
parents: 65212
diff changeset
    15
  val init_options_interactive: unit -> unit
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
    16
  val init: unit -> unit
71644
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
    17
  val init_build: unit -> unit
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    18
end;
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    19
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31384
diff changeset
    20
structure Isabelle_Process: ISABELLE_PROCESS =
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    21
struct
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    22
42897
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
    23
(* print mode *)
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    24
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    25
val isabelle_processN = "isabelle_process";
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    26
42897
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
    27
fun is_active () = Print_Mode.print_mode_active isabelle_processN;
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
    28
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    29
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
28036
wenzelm
parents: 27986
diff changeset
    30
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    31
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
    32
val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
    33
val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
    34
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    35
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    36
(* protocol commands *)
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    37
71878
3cd8449829fa clarified signature;
wenzelm
parents: 71675
diff changeset
    38
exception STOP of int;
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
    39
71878
3cd8449829fa clarified signature;
wenzelm
parents: 71675
diff changeset
    40
val is_protocol_exn = fn STOP _ => true | _ => false;
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
    41
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    42
local
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    43
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    44
val commands =
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
    45
  Synchronized.var "Isabelle_Process.commands"
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
    46
    (Symtab.empty: (string list -> unit) Symtab.table);
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    47
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    48
in
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    49
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    50
fun protocol_command name cmd =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    51
  Synchronized.change commands (fn cmds =>
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    52
   (if not (Symtab.defined cmds name) then ()
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52580
diff changeset
    53
    else warning ("Redefining Isabelle protocol command " ^ quote name);
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    54
    Symtab.update (name, cmd) cmds));
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    55
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    56
fun run_command name args =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    57
  (case Symtab.lookup (Synchronized.value commands) name of
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52580
diff changeset
    58
    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    59
  | SOME cmd =>
59056
cbe9563c03d1 even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents: 59055
diff changeset
    60
      (Runtime.exn_trace_system (fn () => cmd args)
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
    61
        handle exn =>
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
    62
          if is_protocol_exn exn then Exn.reraise exn
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
    63
          else error ("Isabelle protocol command failure: " ^ quote name)));
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    64
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    65
end;
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    66
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    67
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    68
(* restricted tracing messages *)
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    69
52105
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    70
val tracing_messages =
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    71
  Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    72
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    73
fun reset_tracing exec_id =
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    74
  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    75
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    76
fun update_tracing () =
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50715
diff changeset
    77
  (case Position.parse_id (Position.thread_data ()) of
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    78
    NONE => ()
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    79
  | SOME exec_id =>
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    80
      let
52560
wenzelm
parents: 52559
diff changeset
    81
        val ok =
52105
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    82
          Synchronized.change_result tracing_messages (fn tab =>
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    83
            let
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    84
              val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
69103
814a1ab42d70 unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
wenzelm
parents: 68025
diff changeset
    85
              val limit = Options.default_int "editor_tracing_messages";
814a1ab42d70 unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
wenzelm
parents: 68025
diff changeset
    86
              val ok = limit <= 0 orelse n <= limit;
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    87
            in (ok, Inttab.update (exec_id, n) tab) end);
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    88
      in
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    89
        if ok then ()
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    90
        else
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    91
          let
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    92
            val (text, promise) = Active.dialog_text ();
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    93
            val _ =
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    94
              writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
51044
890f502f0e89 more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
wenzelm
parents: 50911
diff changeset
    95
                text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62930
diff changeset
    96
            val m = Value.parse_int (Future.join promise)
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    97
              handle Fail _ => error "Stopped";
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    98
          in
52105
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    99
            Synchronized.change tracing_messages
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
   100
              (Inttab.map_default (exec_id, 0) (fn k => k - m))
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
   101
          end
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
   102
      end);
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
   103
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
   104
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   105
(* init protocol -- uninterruptible *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   106
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   107
val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   108
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   109
local
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   110
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   111
fun recover crash =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   112
  (Synchronized.change crashes (cons crash);
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   113
    Output.physical_stderr
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   114
      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   115
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   116
in
28188
51ccf7fa6f18 auto_flush stdout, stderr as well;
wenzelm
parents: 28182
diff changeset
   117
71644
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   118
fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   119
  let
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   120
    val _ = SHA1.test_samples ()
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   121
      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   122
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   123
    val _ = Output.physical_stderr Symbol.STX;
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52852
diff changeset
   124
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   125
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   126
    (* streams *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   127
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   128
    val (in_stream, out_stream) = Socket_IO.open_streams address;
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   129
    val _ = Byte_Message.write_line out_stream password;
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   130
40134
8baded087d34 explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
wenzelm
parents: 40133
diff changeset
   131
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
8baded087d34 explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
wenzelm
parents: 40133
diff changeset
   132
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
69449
b516fdf8005c more uniform multi-language operations;
wenzelm
parents: 69103
diff changeset
   133
    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
40134
8baded087d34 explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
wenzelm
parents: 40133
diff changeset
   134
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   135
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   136
    (* messages *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   137
69449
b516fdf8005c more uniform multi-language operations;
wenzelm
parents: 69103
diff changeset
   138
    val msg_channel = Message_Channel.make out_stream;
52580
36aa39694ab4 fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents: 52578
diff changeset
   139
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
   140
    fun message name props body =
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
   141
      Message_Channel.send msg_channel (Message_Channel.message name props body);
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
   142
70995
2c17fa0f5187 more direct output of XML material -- bypass Buffer.T;
wenzelm
parents: 70991
diff changeset
   143
    fun standard_message props name ss =
2c17fa0f5187 more direct output of XML material -- bypass Buffer.T;
wenzelm
parents: 70991
diff changeset
   144
      if forall (fn s => s = "") ss then ()
52580
36aa39694ab4 fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents: 52578
diff changeset
   145
      else
57913
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   146
        let
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   147
          val props' =
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   148
            (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   149
              (false, SOME id') => props @ [(Markup.idN, id')]
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   150
            | _ => props);
70995
2c17fa0f5187 more direct output of XML material -- bypass Buffer.T;
wenzelm
parents: 70991
diff changeset
   151
        in message name props' (XML.blob ss) end;
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   152
71675
55cb4271858b less redundant markup reports;
wenzelm
parents: 71667
diff changeset
   153
    fun report_message ss =
55cb4271858b less redundant markup reports;
wenzelm
parents: 71667
diff changeset
   154
      if Context_Position.pide_reports ()
55cb4271858b less redundant markup reports;
wenzelm
parents: 71667
diff changeset
   155
      then standard_message [] Markup.reportN ss else ();
55cb4271858b less redundant markup reports;
wenzelm
parents: 71667
diff changeset
   156
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   157
    val serial_props = Markup.serial_properties o serial;
65212
fd6bc719c98b more robust startup/init: let Session.stop wait for protocol handler initialization;
wenzelm
parents: 63806
diff changeset
   158
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   159
    val message_context =
71675
55cb4271858b less redundant markup reports;
wenzelm
parents: 71667
diff changeset
   160
      Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #>
55cb4271858b less redundant markup reports;
wenzelm
parents: 71667
diff changeset
   161
      Unsynchronized.setmp Private_Output.report_fn report_message #>
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   162
      Unsynchronized.setmp Private_Output.result_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   163
        (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   164
      Unsynchronized.setmp Private_Output.writeln_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   165
        (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   166
      Unsynchronized.setmp Private_Output.state_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   167
        (fn s => standard_message (serial_props ()) Markup.stateN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   168
      Unsynchronized.setmp Private_Output.information_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   169
        (fn s => standard_message (serial_props ()) Markup.informationN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   170
      Unsynchronized.setmp Private_Output.tracing_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   171
        (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   172
      Unsynchronized.setmp Private_Output.warning_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   173
        (fn s => standard_message (serial_props ()) Markup.warningN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   174
      Unsynchronized.setmp Private_Output.legacy_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   175
        (fn s => standard_message (serial_props ()) Markup.legacyN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   176
      Unsynchronized.setmp Private_Output.error_message_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   177
        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   178
      Unsynchronized.setmp Private_Output.system_message_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   179
        (fn ss => message Markup.systemN [] (XML.blob ss)) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   180
      Unsynchronized.setmp Private_Output.protocol_message_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   181
        (fn props => fn body => message Markup.protocolN props body) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   182
      Unsynchronized.setmp print_mode
71644
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   183
        ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes));
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   184
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   185
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   186
    (* protocol *)
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   187
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   188
    fun protocol_loop () =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   189
      let
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   190
        val _ =
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   191
          (case Byte_Message.read_message in_stream of
71878
3cd8449829fa clarified signature;
wenzelm
parents: 71675
diff changeset
   192
            NONE => raise STOP 0
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   193
          | SOME [] => Output.system_message "Isabelle process: no input"
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   194
          | SOME (name :: args) => run_command name args)
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   195
          handle exn =>
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   196
            if is_protocol_exn exn then Exn.reraise exn
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   197
            else (Runtime.exn_system_message exn handle crash => recover crash);
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   198
      in protocol_loop () end;
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   199
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   200
    fun protocol () =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   201
     (Session.init_protocol_handlers ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   202
      message Markup.initN [] [XML.Text (Session.welcome ())];
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   203
      protocol_loop ());
71631
3f02bc5a5a03 more accurate treatment of errors;
wenzelm
parents: 70995
diff changeset
   204
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   205
    val result = Exn.capture (message_context protocol) ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   206
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   207
71637
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   208
    (* shutdown *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   209
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   210
    val _ = Future.shutdown ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   211
    val _ = Execution.reset ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71631
diff changeset
   212
    val _ = Message_Channel.shutdown msg_channel;
71638
ec14ef6dd09b close socket explicitly (idempotent);
wenzelm
parents: 71637
diff changeset
   213
    val _ = BinIO.closeIn in_stream;
ec14ef6dd09b close socket explicitly (idempotent);
wenzelm
parents: 71637
diff changeset
   214
    val _ = BinIO.closeOut out_stream;
71667
4d2de35214c5 proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents: 71656
diff changeset
   215
72104
d9a42786fbc9 more thorough cleanup, e.g. before ML_Heap.save;
wenzelm
parents: 71878
diff changeset
   216
    val _ = Options.reset_default ();
71656
3e121f999120 clarified signature: more direct Isabelle_Process.EXIT;
wenzelm
parents: 71644
diff changeset
   217
  in
3e121f999120 clarified signature: more direct Isabelle_Process.EXIT;
wenzelm
parents: 71644
diff changeset
   218
    (case result of
71878
3cd8449829fa clarified signature;
wenzelm
parents: 71675
diff changeset
   219
      Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
71656
3e121f999120 clarified signature: more direct Isabelle_Process.EXIT;
wenzelm
parents: 71644
diff changeset
   220
    | _ => Exn.release result)
3e121f999120 clarified signature: more direct Isabelle_Process.EXIT;
wenzelm
parents: 71644
diff changeset
   221
  end);
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   222
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   223
end;
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   224
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   225
62563
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   226
(* init options *)
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   227
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   228
fun init_options () =
62878
1cec457e0a03 clarified modules -- simplified bootstrap;
wenzelm
parents: 62713
diff changeset
   229
 (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
62712
22a17cec2efe clarified use of options;
wenzelm
parents: 62666
diff changeset
   230
  Future.ML_statistics := Options.default_bool "ML_statistics";
62563
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   231
  Multithreading.trace := Options.default_int "threads_trace";
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   232
  Multithreading.max_threads_update (Options.default_int "threads");
68025
7fb7a6366a40 clarified modules;
wenzelm
parents: 66020
diff changeset
   233
  Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
70914
05c4c6a99b3f option to export standardized proof terms (not scalable);
wenzelm
parents: 69572
diff changeset
   234
  if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
65448
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65303
diff changeset
   235
  let val proofs = Options.default_int "record_proofs"
9bc3b57c1fa7 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents: 65303
diff changeset
   236
  in if proofs < 0 then () else Proofterm.proofs := proofs end;
65302
3f92d63dad12 clarified init (see also 32755e357a51, ac48def96b69);
wenzelm
parents: 65301
diff changeset
   237
  Printer.show_markup_default := false);
62563
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   238
65300
c262653a3b88 clarified signature;
wenzelm
parents: 65212
diff changeset
   239
fun init_options_interactive () =
c262653a3b88 clarified signature;
wenzelm
parents: 65212
diff changeset
   240
 (init_options ();
68025
7fb7a6366a40 clarified modules;
wenzelm
parents: 66020
diff changeset
   241
  Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
65302
3f92d63dad12 clarified init (see also 32755e357a51, ac48def96b69);
wenzelm
parents: 65301
diff changeset
   242
  Printer.show_markup_default := true);
62599
f35858c831e5 clarified session build options: already provided by ML_Process;
wenzelm
parents: 62564
diff changeset
   243
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   244
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   245
(* generic init *)
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   246
71644
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   247
fun init_modes modes =
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   248
  let
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   249
    val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>;
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   250
    val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   251
  in
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   252
    if address <> "" andalso password <> ""
71644
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   253
    then init_protocol modes (address, password)
69572
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   254
    else init_options ()
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   255
  end;
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69449
diff changeset
   256
71644
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   257
fun init () = init_modes (protocol_modes1, protocol_modes2);
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   258
fun init_build () = init_modes ([], protocol_modes2);
60659474ed36 traditional print_mode for batch build;
wenzelm
parents: 71640
diff changeset
   259
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   260
end;