author | wenzelm |
Fri, 02 Aug 2013 20:47:02 +0200 | |
changeset 52852 | 08ecbffaf25c |
parent 52800 | 1baa5d19ac44 |
child 52854 | 92932931bd82 |
permissions | -rw-r--r-- |
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 |
|
38445
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
4 |
Isabelle process wrapper, based on private fifos for maximum |
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
5 |
robustness and performance, or local socket for maximum portability. |
25528
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 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
8 |
signature ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
9 |
sig |
42897 | 10 |
val is_active: unit -> bool |
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 | 13 |
val crashes: exn list Synchronized.var |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
14 |
val init_fifos: string -> string -> unit |
45028 | 15 |
val init_socket: string -> unit |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
16 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
17 |
|
31797 | 18 |
structure Isabelle_Process: ISABELLE_PROCESS = |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
19 |
struct |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
20 |
|
42897 | 21 |
(* print mode *) |
25554 | 22 |
|
25748 | 23 |
val isabelle_processN = "isabelle_process"; |
24 |
||
42897 | 25 |
fun is_active () = Print_Mode.print_mode_active isabelle_processN; |
26 |
||
26550 | 27 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
28036 | 28 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup; |
25841 | 29 |
|
30 |
||
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
31 |
(* protocol commands *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
32 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
33 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
34 |
|
43684 | 35 |
val commands = |
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
36 |
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
|
37 |
(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
|
38 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
39 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
40 |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
41 |
fun protocol_command name cmd = |
43684 | 42 |
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
|
43 |
(if not (Symtab.defined cmds name) then () |
52582 | 44 |
else warning ("Redefining Isabelle protocol command " ^ quote name); |
43684 | 45 |
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
|
46 |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
47 |
fun run_command name args = |
43684 | 48 |
(case Symtab.lookup (Synchronized.value commands) name of |
52582 | 49 |
NONE => error ("Undefined Isabelle protocol command " ^ quote name) |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
50 |
| SOME cmd => |
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
51 |
(Runtime.debugging cmd args handle exn => |
52582 | 52 |
error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^ |
48056 | 53 |
ML_Compiler.exn_message exn))); |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
54 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
55 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
56 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
57 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
58 |
(* restricted tracing messages *) |
49647 | 59 |
|
52105 | 60 |
val tracing_messages = |
61 |
Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); |
|
49647 | 62 |
|
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
63 |
fun reset_tracing exec_id = |
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
64 |
Synchronized.change tracing_messages (Inttab.delete_safe exec_id); |
49647 | 65 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
66 |
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
|
67 |
(case Position.parse_id (Position.thread_data ()) of |
49647 | 68 |
NONE => () |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
69 |
| SOME exec_id => |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
70 |
let |
52560 | 71 |
val ok = |
52105 | 72 |
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
|
73 |
let |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
74 |
val n = the_default 0 (Inttab.lookup tab exec_id) + 1; |
52105 | 75 |
val ok = n <= Options.default_int "editor_tracing_messages"; |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
76 |
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
|
77 |
in |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
78 |
if ok then () |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
79 |
else |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
80 |
let |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
81 |
val (text, promise) = Active.dialog_text (); |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
82 |
val _ = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
83 |
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
|
84 |
text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
85 |
val m = Markup.parse_int (Future.join promise) |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
86 |
handle Fail _ => error "Stopped"; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
87 |
in |
52105 | 88 |
Synchronized.change tracing_messages |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
89 |
(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
|
90 |
end |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
91 |
end); |
49647 | 92 |
|
93 |
||
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
94 |
(* output channels *) |
28188 | 95 |
|
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
96 |
fun init_channels channel = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
97 |
let |
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
|
98 |
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
|
99 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, 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
|
100 |
|
52584 | 101 |
val msg_channel = Message_Channel.make channel; |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
102 |
|
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
103 |
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
|
104 |
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
|
105 |
|
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
106 |
fun standard_message opt_serial name body = |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
107 |
if body = "" then () |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
108 |
else |
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
109 |
message name |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
110 |
((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
111 |
(Position.properties_of (Position.thread_data ()))) body; |
28044 | 112 |
in |
52852 | 113 |
Output.Internal.status_fn := standard_message NONE Markup.statusN; |
114 |
Output.Internal.report_fn := standard_message NONE Markup.reportN; |
|
115 |
Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s); |
|
116 |
Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s); |
|
117 |
Output.Internal.tracing_fn := |
|
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
118 |
(fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s)); |
52852 | 119 |
Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s); |
120 |
Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s); |
|
121 |
Output.Internal.protocol_message_fn := message Markup.protocolN; |
|
122 |
Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn; |
|
123 |
Output.Internal.prompt_fn := ignore; |
|
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
124 |
message Markup.initN [] (Session.welcome ()); |
52584 | 125 |
msg_channel |
28044 | 126 |
end; |
25841 | 127 |
|
128 |
||
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38871
diff
changeset
|
129 |
(* protocol loop -- uninterruptible *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
130 |
|
43684 | 131 |
val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
132 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
133 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
134 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
135 |
fun recover crash = |
43684 | 136 |
(Synchronized.change crashes (cons crash); |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
137 |
warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes"); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
138 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
139 |
fun read_chunk channel len = |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
140 |
let |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
141 |
val n = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
142 |
(case Int.fromString len of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
143 |
SOME n => n |
52799 | 144 |
| NONE => error ("Isabelle process: malformed header " ^ quote len)); |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
145 |
val chunk = System_Channel.inputN channel n; |
52799 | 146 |
val i = size chunk; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
147 |
in |
52799 | 148 |
if i <> n then |
149 |
error ("Isabelle process: bad chunk (unexpected EOF after " ^ |
|
150 |
string_of_int i ^ " of " ^ string_of_int n ^ " bytes)") |
|
151 |
else chunk |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
152 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
153 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
154 |
fun read_command channel = |
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
155 |
(case System_Channel.input_line channel of |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
156 |
NONE => raise Runtime.TERMINATE |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
157 |
| SOME line => map (read_chunk channel) (space_explode "," line)); |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
158 |
|
52559
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52111
diff
changeset
|
159 |
fun worker_guest e = |
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52111
diff
changeset
|
160 |
Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e (); |
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52111
diff
changeset
|
161 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
162 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
163 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
164 |
fun loop channel = |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
165 |
let val continue = |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
166 |
(case read_command channel of |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
167 |
[] => (Output.error_msg "Isabelle process: no input"; true) |
52559
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52111
diff
changeset
|
168 |
| name :: args => (worker_guest (fn () => run_command name args); true)) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
169 |
handle Runtime.TERMINATE => false |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
170 |
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true); |
52770
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
171 |
in |
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
172 |
if continue then loop channel |
52787
c143ad7811fc
pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents:
52786
diff
changeset
|
173 |
else (Future.shutdown (); Goal.reset_futures (); Execution.reset ()) |
52770
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
174 |
end; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
175 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
176 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
177 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
178 |
|
25554 | 179 |
(* init *) |
180 |
||
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
181 |
val default_modes1 = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
182 |
[Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN]; |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
183 |
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]; |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
184 |
|
52578
bd94e26e4388
retain main thread for protocol loop -- no access to raw ML toplevel;
wenzelm
parents:
52560
diff
changeset
|
185 |
val init = uninterruptible (fn _ => fn rendezvous => |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
186 |
let |
46548
c54a4a22501c
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents:
46121
diff
changeset
|
187 |
val _ = Output.physical_stderr Symbol.STX; |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39513
diff
changeset
|
188 |
|
49661
ac48def96b69
enable show_markup by default (approx. double output size);
wenzelm
parents:
49647
diff
changeset
|
189 |
val _ = Printer.show_markup_default := true; |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39513
diff
changeset
|
190 |
val _ = Context.set_thread_data NONE; |
43671
a250b092ac66
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
wenzelm
parents:
42897
diff
changeset
|
191 |
val _ = |
a250b092ac66
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
wenzelm
parents:
42897
diff
changeset
|
192 |
Unsynchronized.change print_mode |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
193 |
(fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39513
diff
changeset
|
194 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
195 |
val channel = rendezvous (); |
52584 | 196 |
val msg_channel = init_channels channel; |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
52105
diff
changeset
|
197 |
val _ = Session.init_protocol_handlers (); |
52583 | 198 |
val _ = loop channel; |
52584 | 199 |
in Message_Channel.shutdown msg_channel end); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
200 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
201 |
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2); |
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
202 |
fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); |
45028 | 203 |
|
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
204 |
end; |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39513
diff
changeset
|
205 |