src/Pure/System/isabelle_process.ML
author wenzelm
Wed, 01 Apr 2020 12:56:19 +0200
changeset 71855 494704309099
parent 71853 ec14ef6dd09b
child 71859 60659474ed36
permissions -rw-r--r--
proper context for loading Pure;
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
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    10
  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
    11
  val reset_tracing: Document_ID.exec -> unit
71847
3f02bc5a5a03 more accurate treatment of errors;
wenzelm
parents: 71192
diff changeset
    12
  exception EXIT of exn
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
69584
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
    16
  val init: unit -> unit
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    17
end;
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    18
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31384
diff changeset
    19
structure Isabelle_Process: ISABELLE_PROCESS =
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    20
struct
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    21
42897
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
    22
(* print mode *)
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    23
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    24
val isabelle_processN = "isabelle_process";
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    25
42897
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
    26
fun is_active () = Print_Mode.print_mode_active isabelle_processN;
6bc8a6dcb3e0 added Isabelle_Process.is_active;
wenzelm
parents: 40521
diff changeset
    27
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    28
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
28036
wenzelm
parents: 27986
diff changeset
    29
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    30
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
    31
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: 71847
diff changeset
    32
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: 71847
diff changeset
    33
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    34
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    35
(* protocol commands *)
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    36
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    37
local
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    38
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    39
val commands =
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
    40
  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
    41
    (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
    42
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    43
in
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    44
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    45
fun protocol_command name cmd =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    46
  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
    47
   (if not (Symtab.defined cmds name) then ()
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52580
diff changeset
    48
    else warning ("Redefining Isabelle protocol command " ^ quote name);
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    49
    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
    50
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    51
fun run_command name args =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 43673
diff changeset
    52
  (case Symtab.lookup (Synchronized.value commands) name of
52582
31467a4b1466 tuned signature;
wenzelm
parents: 52580
diff changeset
    53
    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
46119
0d7172a7672c tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents: 45666
diff changeset
    54
  | SOME cmd =>
59056
cbe9563c03d1 even more exception traces for Document.update, which goes through additional execution wrappers;
wenzelm
parents: 59055
diff changeset
    55
      (Runtime.exn_trace_system (fn () => cmd args)
59055
5a7157b8e870 more informative failure of protocol commands, with exception trace;
wenzelm
parents: 58850
diff changeset
    56
        handle _ (*sic!*) => 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
    57
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    58
end;
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    59
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
    60
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    61
(* restricted tracing messages *)
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    62
52105
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    63
val tracing_messages =
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    64
  Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    65
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    66
fun reset_tracing exec_id =
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    67
  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    68
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    69
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
    70
  (case Position.parse_id (Position.thread_data ()) of
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    71
    NONE => ()
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    72
  | SOME exec_id =>
50505
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    73
      let
52560
wenzelm
parents: 52559
diff changeset
    74
        val ok =
52105
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    75
          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
    76
            let
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    77
              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
    78
              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
    79
              val ok = limit <= 0 orelse n <= limit;
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    80
            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
    81
      in
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    82
        if ok then ()
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    83
        else
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    84
          let
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    85
            val (text, promise) = Active.dialog_text ();
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    86
            val _ =
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    87
              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
    88
                text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62930
diff changeset
    89
            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
    90
              handle Fail _ => error "Stopped";
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    91
          in
52105
88b423034d4f proper options;
wenzelm
parents: 52104
diff changeset
    92
            Synchronized.change tracing_messages
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52584
diff changeset
    93
              (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
    94
          end
33c92722cc3d smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents: 50503
diff changeset
    95
      end);
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    96
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49566
diff changeset
    97
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
    98
(* init protocol -- uninterruptible *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
    99
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   100
exception EXIT of exn;
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   101
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   102
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: 71847
diff changeset
   103
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   104
local
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   105
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   106
fun recover crash =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   107
  (Synchronized.change crashes (cons crash);
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   108
    Output.physical_stderr
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   109
      "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: 71847
diff changeset
   110
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   111
in
28188
51ccf7fa6f18 auto_flush stdout, stderr as well;
wenzelm
parents: 28182
diff changeset
   112
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   113
val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   114
  let
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   115
    val _ = SHA1.test_samples ()
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   116
      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: 71847
diff changeset
   117
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   118
    val _ = Output.physical_stderr Symbol.STX;
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52852
diff changeset
   119
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   120
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   121
    (* streams *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   122
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   123
    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: 71847
diff changeset
   124
    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: 71847
diff changeset
   125
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
   126
    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
   127
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
69459
b516fdf8005c more uniform multi-language operations;
wenzelm
parents: 69103
diff changeset
   128
    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
   129
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   130
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   131
    (* messages *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   132
69459
b516fdf8005c more uniform multi-language operations;
wenzelm
parents: 69103
diff changeset
   133
    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
   134
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52799
diff changeset
   135
    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
   136
      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
   137
71192
2c17fa0f5187 more direct output of XML material -- bypass Buffer.T;
wenzelm
parents: 71188
diff changeset
   138
    fun standard_message props name ss =
2c17fa0f5187 more direct output of XML material -- bypass Buffer.T;
wenzelm
parents: 71188
diff changeset
   139
      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
   140
      else
57913
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   141
        let
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   142
          val props' =
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   143
            (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   144
              (false, SOME id') => props @ [(Markup.idN, id')]
8544ef75d1d8 more frugal standard message properties;
wenzelm
parents: 56895
diff changeset
   145
            | _ => props);
71192
2c17fa0f5187 more direct output of XML material -- bypass Buffer.T;
wenzelm
parents: 71188
diff changeset
   146
        in message name props' (XML.blob ss) end;
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   147
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   148
    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
   149
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   150
    val message_context =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   151
      Unsynchronized.setmp Private_Output.status_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   152
        (standard_message [] Markup.statusN) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   153
      Unsynchronized.setmp Private_Output.report_fn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   154
        (standard_message [] Markup.reportN) #>
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   155
      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: 71847
diff changeset
   156
        (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: 71847
diff changeset
   157
      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: 71847
diff changeset
   158
        (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: 71847
diff changeset
   159
      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: 71847
diff changeset
   160
        (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: 71847
diff changeset
   161
      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: 71847
diff changeset
   162
        (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: 71847
diff changeset
   163
      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: 71847
diff changeset
   164
        (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: 71847
diff changeset
   165
      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: 71847
diff changeset
   166
        (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: 71847
diff changeset
   167
      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: 71847
diff changeset
   168
        (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: 71847
diff changeset
   169
      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: 71847
diff changeset
   170
        (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: 71847
diff changeset
   171
      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: 71847
diff changeset
   172
        (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: 71847
diff changeset
   173
      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: 71847
diff changeset
   174
        (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: 71847
diff changeset
   175
      Unsynchronized.setmp print_mode
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   176
        ((! print_mode @ protocol_modes1) |> fold (update op =) protocol_modes2);
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   177
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   178
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   179
    (* protocol *)
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   180
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   181
    fun protocol_loop () =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   182
      let
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   183
        val continue =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   184
          (case Byte_Message.read_message in_stream of
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   185
            NONE => false
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   186
          | SOME [] => (Output.system_message "Isabelle process: no input"; true)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   187
          | SOME (name :: args) => (run_command name args; true))
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   188
          handle EXIT exn => Exn.reraise exn
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   189
            | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   190
      in if continue then protocol_loop () else () end;
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   191
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   192
    fun protocol () =
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   193
     (Session.init_protocol_handlers ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   194
      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: 71847
diff changeset
   195
      protocol_loop ());
71847
3f02bc5a5a03 more accurate treatment of errors;
wenzelm
parents: 71192
diff changeset
   196
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   197
    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: 71847
diff changeset
   198
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   199
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   200
    (* shutdown *)
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   201
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   202
    val _ = Future.shutdown ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   203
    val _ = Execution.reset ();
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   204
    val _ = Message_Channel.shutdown msg_channel;
71853
ec14ef6dd09b close socket explicitly (idempotent);
wenzelm
parents: 71852
diff changeset
   205
    val _ = BinIO.closeIn in_stream;
ec14ef6dd09b close socket explicitly (idempotent);
wenzelm
parents: 71852
diff changeset
   206
    val _ = BinIO.closeOut out_stream;
71852
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   207
45c2b8cf1b26 more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);
wenzelm
parents: 71847
diff changeset
   208
  in Exn.release result end);
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   209
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   210
end;
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   211
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38265
diff changeset
   212
62563
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   213
(* init options *)
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   214
2e352f63d15f separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
wenzelm
parents: 62505
diff changeset
   215
fun init_options () =
62878
1cec457e0a03 clarified modules -- simplified bootstrap;
wenzelm
parents: 62713
diff changeset
   216
 (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
62712
22a17cec2efe clarified use of options;
wenzelm
parents: 62666
diff changeset
   217
  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
   218
  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
   219
  Multithreading.max_threads_update (Options.default_int "threads");
68025
7fb7a6366a40 clarified modules;
wenzelm
parents: 66020
diff changeset
   220
  Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
71104
05c4c6a99b3f option to export standardized proof terms (not scalable);
wenzelm
parents: 69584
diff changeset
   221
  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
   222
  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
   223
  in if proofs < 0 then () else Proofterm.proofs := proofs end;
65302
3f92d63dad12 clarified init (see also 32755e357a51, ac48def96b69);
wenzelm
parents: 65301
diff changeset
   224
  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
   225
65300
c262653a3b88 clarified signature;
wenzelm
parents: 65212
diff changeset
   226
fun init_options_interactive () =
c262653a3b88 clarified signature;
wenzelm
parents: 65212
diff changeset
   227
 (init_options ();
68025
7fb7a6366a40 clarified modules;
wenzelm
parents: 66020
diff changeset
   228
  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
   229
  Printer.show_markup_default := true);
62599
f35858c831e5 clarified session build options: already provided by ML_Process;
wenzelm
parents: 62564
diff changeset
   230
69584
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   231
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   232
(* generic init *)
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   233
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   234
fun init () =
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   235
  let
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   236
    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: 69459
diff changeset
   237
    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: 69459
diff changeset
   238
  in
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   239
    if address <> "" andalso password <> ""
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   240
    then init_protocol (address, password)
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   241
    else init_options ()
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   242
  end;
09a6a7c04b45 more robust system channel via options that are private to the user;
wenzelm
parents: 69459
diff changeset
   243
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   244
end;