author | wenzelm |
Thu, 27 Mar 2014 17:12:40 +0100 | |
changeset 56303 | 4cc3f4db3447 |
parent 56265 | 785569927666 |
child 56333 | 38f1422ef473 |
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 => |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56265
diff
changeset
|
51 |
(Runtime.debugging NONE cmd args handle exn => |
52582 | 52 |
error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^ |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56265
diff
changeset
|
53 |
Runtime.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 |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
96 |
val serial_props = Markup.serial_properties o serial; |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
97 |
|
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
98 |
fun init_channels channel = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
|
52584 | 103 |
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
|
104 |
|
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
105 |
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
|
106 |
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
|
107 |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
108 |
fun standard_message props name body = |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
109 |
if body = "" then () |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
110 |
else |
52800
1baa5d19ac44
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents:
52799
diff
changeset
|
111 |
message name |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
112 |
(fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body; |
28044 | 113 |
in |
55387
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
114 |
Output.status_fn := standard_message [] Markup.statusN; |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
115 |
Output.report_fn := standard_message [] Markup.reportN; |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
116 |
Output.result_fn := |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
117 |
(fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); |
55387
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
118 |
Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
119 |
Output.tracing_fn := |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
120 |
(fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); |
55387
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
121 |
Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
122 |
Output.error_message_fn := |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52852
diff
changeset
|
123 |
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); |
55387
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
124 |
Output.protocol_message_fn := message Markup.protocolN; |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
125 |
Output.urgent_message_fn := ! Output.writeln_fn; |
51f0876f61df
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
wenzelm
parents:
54671
diff
changeset
|
126 |
Output.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
|
127 |
message Markup.initN [] (Session.welcome ()); |
52584 | 128 |
msg_channel |
28044 | 129 |
end; |
25841 | 130 |
|
131 |
||
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38871
diff
changeset
|
132 |
(* protocol loop -- uninterruptible *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
133 |
|
43684 | 134 |
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
|
135 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
136 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
137 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
138 |
fun recover crash = |
43684 | 139 |
(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
|
140 |
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
|
141 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
142 |
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
|
143 |
let |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
144 |
val n = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
145 |
(case Int.fromString len of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
146 |
SOME n => n |
52799 | 147 |
| NONE => error ("Isabelle process: malformed header " ^ quote len)); |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
148 |
val chunk = System_Channel.inputN channel n; |
52799 | 149 |
val i = size chunk; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
150 |
in |
52799 | 151 |
if i <> n then |
152 |
error ("Isabelle process: bad chunk (unexpected EOF after " ^ |
|
153 |
string_of_int i ^ " of " ^ string_of_int n ^ " bytes)") |
|
154 |
else chunk |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
155 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
156 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
157 |
fun read_command channel = |
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
158 |
(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
|
159 |
NONE => raise Runtime.TERMINATE |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
160 |
| 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
|
161 |
|
54649
99b9249b3e05
more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
wenzelm
parents:
54637
diff
changeset
|
162 |
fun task_context e = |
99b9249b3e05
more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
wenzelm
parents:
54637
diff
changeset
|
163 |
Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e (); |
52559
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52111
diff
changeset
|
164 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
165 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
166 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
167 |
fun loop channel = |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
168 |
let val continue = |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
169 |
(case read_command channel of |
54387 | 170 |
[] => (Output.error_message "Isabelle process: no input"; true) |
54649
99b9249b3e05
more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
wenzelm
parents:
54637
diff
changeset
|
171 |
| name :: args => (task_context (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
|
172 |
handle Runtime.TERMINATE => false |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56265
diff
changeset
|
173 |
| exn => (Runtime.exn_error_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
|
174 |
in |
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
175 |
if continue then loop channel |
53192 | 176 |
else (Future.shutdown (); Execution.reset (); ()) |
52770
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
177 |
end; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
178 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
179 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
180 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
181 |
|
25554 | 182 |
(* init *) |
183 |
||
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
184 |
val default_modes1 = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
185 |
[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
|
186 |
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]; |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
187 |
|
52578
bd94e26e4388
retain main thread for protocol loop -- no access to raw ML toplevel;
wenzelm
parents:
52560
diff
changeset
|
188 |
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
|
189 |
let |
53212
387b9f7cb0ac
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
53192
diff
changeset
|
190 |
val _ = SHA1_Samples.test () |
387b9f7cb0ac
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
53192
diff
changeset
|
191 |
handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn); |
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
|
192 |
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
|
193 |
|
49661
ac48def96b69
enable show_markup by default (approx. double output size);
wenzelm
parents:
49647
diff
changeset
|
194 |
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
|
195 |
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
|
196 |
val _ = |
a250b092ac66
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
wenzelm
parents:
42897
diff
changeset
|
197 |
Unsynchronized.change print_mode |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
198 |
(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
|
199 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
200 |
val channel = rendezvous (); |
52584 | 201 |
val msg_channel = init_channels channel; |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
52105
diff
changeset
|
202 |
val _ = Session.init_protocol_handlers (); |
52583 | 203 |
val _ = loop channel; |
52584 | 204 |
in Message_Channel.shutdown msg_channel end); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
205 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
206 |
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
|
207 |
fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); |
45028 | 208 |
|
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
209 |
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
|
210 |