author | wenzelm |
Mon, 29 Jul 2013 15:09:20 +0200 | |
changeset 52770 | 8c7cf864e270 |
parent 52712 | 43e48bb554ba |
child 52786 | 9795ea654905 |
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. |
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
|
6 |
|
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
|
7 |
Startup phases: |
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
8 |
- raw Posix process startup with uncontrolled output on stdout/stderr |
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
9 |
- stderr \002: ML running |
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
10 |
- stdin/stdout/stderr freely available (raw ML loop) |
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
11 |
- protocol thread initialization |
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
12 |
- rendezvous on system channel |
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
13 |
- message INIT: channels ready |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
14 |
*) |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
15 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
16 |
signature ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
17 |
sig |
42897 | 18 |
val is_active: unit -> bool |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
19 |
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
|
20 |
val reset_tracing: Document_ID.exec -> unit |
43684 | 21 |
val crashes: exn list Synchronized.var |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
22 |
val init_fifos: string -> string -> unit |
45028 | 23 |
val init_socket: string -> unit |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
24 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
25 |
|
31797 | 26 |
structure Isabelle_Process: ISABELLE_PROCESS = |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
27 |
struct |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
28 |
|
42897 | 29 |
(* print mode *) |
25554 | 30 |
|
25748 | 31 |
val isabelle_processN = "isabelle_process"; |
32 |
||
42897 | 33 |
fun is_active () = Print_Mode.print_mode_active isabelle_processN; |
34 |
||
26550 | 35 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
28036 | 36 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup; |
25841 | 37 |
|
38 |
||
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
39 |
(* protocol commands *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
40 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
41 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
42 |
|
43684 | 43 |
val commands = |
44 |
Synchronized.var "Isabelle_Process.commands" (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
|
45 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
46 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
47 |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
48 |
fun protocol_command name cmd = |
43684 | 49 |
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
|
50 |
(if not (Symtab.defined cmds name) then () |
52582 | 51 |
else warning ("Redefining Isabelle protocol command " ^ quote name); |
43684 | 52 |
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
|
53 |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
54 |
fun run_command name args = |
43684 | 55 |
(case Symtab.lookup (Synchronized.value commands) name of |
52582 | 56 |
NONE => error ("Undefined Isabelle protocol command " ^ quote name) |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
57 |
| SOME cmd => |
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
58 |
(Runtime.debugging cmd args handle exn => |
52582 | 59 |
error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^ |
48056 | 60 |
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
|
61 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
62 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
63 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
64 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
65 |
(* restricted tracing messages *) |
49647 | 66 |
|
52105 | 67 |
val tracing_messages = |
68 |
Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); |
|
49647 | 69 |
|
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
70 |
fun reset_tracing exec_id = |
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
71 |
Synchronized.change tracing_messages (Inttab.delete_safe exec_id); |
49647 | 72 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
73 |
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
|
74 |
(case Position.parse_id (Position.thread_data ()) of |
49647 | 75 |
NONE => () |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
76 |
| SOME exec_id => |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
77 |
let |
52560 | 78 |
val ok = |
52105 | 79 |
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
|
80 |
let |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
81 |
val n = the_default 0 (Inttab.lookup tab exec_id) + 1; |
52105 | 82 |
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
|
83 |
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
|
84 |
in |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
85 |
if ok then () |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
86 |
else |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
87 |
let |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
88 |
val (text, promise) = Active.dialog_text (); |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
89 |
val _ = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
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
|
93 |
handle Fail _ => error "Stopped"; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
94 |
in |
52105 | 95 |
Synchronized.change tracing_messages |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52584
diff
changeset
|
96 |
(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
|
97 |
end |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
98 |
end); |
49647 | 99 |
|
100 |
||
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
|
101 |
(* message channels *) |
25841 | 102 |
|
103 |
local |
|
25810 | 104 |
|
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
|
105 |
fun chunk s = [string_of_int (size s), "\n", s]; |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
106 |
|
52584 | 107 |
fun message do_flush msg_channel name raw_props body = |
43771
fc524449f511
allow empty body for raw_message -- important for Invoke_Scala;
wenzelm
parents:
43746
diff
changeset
|
108 |
let |
43772
c825594fd0c1
clarified YXML.embed_controls -- this is idempotent and cannot be nested;
wenzelm
parents:
43771
diff
changeset
|
109 |
val robust_props = map (pairself YXML.embed_controls) raw_props; |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
110 |
val header = YXML.string_of (XML.Elem ((name, robust_props), [])); |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
111 |
val msg = chunk header @ chunk body; |
52584 | 112 |
in Message_Channel.send msg_channel msg do_flush end; |
52583 | 113 |
|
28188 | 114 |
in |
115 |
||
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
116 |
fun init_channels channel = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
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
|
120 |
|
52584 | 121 |
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
|
122 |
|
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
123 |
fun standard_message opt_serial name body = |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
124 |
if body = "" then () |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
125 |
else |
52584 | 126 |
message false msg_channel name |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
127 |
((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
|
128 |
(Position.properties_of (Position.thread_data ()))) body; |
28044 | 129 |
in |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
130 |
Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN; |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
131 |
Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN; |
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
132 |
Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s); |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
133 |
Output.Private_Hooks.writeln_fn := |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
134 |
(fn s => standard_message (SOME (serial ())) Markup.writelnN s); |
49647 | 135 |
Output.Private_Hooks.tracing_fn := |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
136 |
(fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s)); |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
137 |
Output.Private_Hooks.warning_fn := |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
138 |
(fn s => standard_message (SOME (serial ())) Markup.warningN s); |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
139 |
Output.Private_Hooks.error_fn := |
52580
36aa39694ab4
fall back on synchronous message output for single-threaded SML/NJ;
wenzelm
parents:
52578
diff
changeset
|
140 |
(fn (i, s) => standard_message (SOME i) Markup.errorN s); |
52584 | 141 |
Output.Private_Hooks.protocol_message_fn := message true msg_channel Markup.protocolN; |
40133
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
142 |
Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
143 |
Output.Private_Hooks.prompt_fn := ignore; |
52584 | 144 |
message true msg_channel Markup.initN [] (Session.welcome ()); |
145 |
msg_channel |
|
28044 | 146 |
end; |
25841 | 147 |
|
28188 | 148 |
end; |
149 |
||
25841 | 150 |
|
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38871
diff
changeset
|
151 |
(* protocol loop -- uninterruptible *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
152 |
|
43684 | 153 |
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
|
154 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
155 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
156 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
157 |
fun recover crash = |
43684 | 158 |
(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
|
159 |
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
|
160 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
161 |
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
|
162 |
let |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
163 |
val n = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
164 |
(case Int.fromString len of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
165 |
SOME n => n |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
166 |
| NONE => error ("Isabelle process: malformed chunk header " ^ quote len)); |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
167 |
val chunk = System_Channel.inputN channel n; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
168 |
val m = size chunk; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
169 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
170 |
if m = n then chunk |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
171 |
else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")") |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
172 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
173 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
174 |
fun read_command channel = |
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
175 |
(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
|
176 |
NONE => raise Runtime.TERMINATE |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
177 |
| 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
|
178 |
|
52559
ddaf277e0d8c
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
wenzelm
parents:
52111
diff
changeset
|
179 |
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
|
180 |
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
|
181 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
182 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
183 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
184 |
fun loop channel = |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
185 |
let val continue = |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
186 |
(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
|
187 |
[] => (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
|
188 |
| 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
|
189 |
handle Runtime.TERMINATE => false |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
190 |
| 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
|
191 |
in |
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
192 |
if continue then loop channel |
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
193 |
else (Future.shutdown (); Goal.reset_futures (); ()) |
8c7cf864e270
pro-forma Goal.reset_futures, despite lack of final join/commit;
wenzelm
parents:
52712
diff
changeset
|
194 |
end; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
195 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
196 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
197 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
198 |
|
25554 | 199 |
(* init *) |
200 |
||
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
201 |
val default_modes1 = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
202 |
[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
|
203 |
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]; |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
204 |
|
52578
bd94e26e4388
retain main thread for protocol loop -- no access to raw ML toplevel;
wenzelm
parents:
52560
diff
changeset
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
|
49661
ac48def96b69
enable show_markup by default (approx. double output size);
wenzelm
parents:
49647
diff
changeset
|
209 |
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
|
210 |
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
|
211 |
val _ = |
a250b092ac66
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
wenzelm
parents:
42897
diff
changeset
|
212 |
Unsynchronized.change print_mode |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
213 |
(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
|
214 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
215 |
val channel = rendezvous (); |
52584 | 216 |
val msg_channel = init_channels channel; |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
52105
diff
changeset
|
217 |
val _ = Session.init_protocol_handlers (); |
52583 | 218 |
val _ = loop channel; |
52584 | 219 |
in Message_Channel.shutdown msg_channel end); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
220 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
221 |
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
|
222 |
fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); |
45028 | 223 |
|
50117 | 224 |
|
225 |
(* options *) |
|
226 |
||
227 |
val _ = |
|
228 |
protocol_command "Isabelle_Process.options" |
|
229 |
(fn [options_yxml] => |
|
230 |
let val options = Options.decode (YXML.parse_body options_yxml) in |
|
51941
ead4248aef3b
full default options for Isabelle_Process and Build;
wenzelm
parents:
51554
diff
changeset
|
231 |
Options.set_default options; |
50698
49621c755075
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
wenzelm
parents:
50505
diff
changeset
|
232 |
Future.ML_statistics := true; |
50117 | 233 |
Multithreading.trace := Options.int options "threads_trace"; |
234 |
Multithreading.max_threads := Options.int options "threads"; |
|
52105 | 235 |
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0) |
50117 | 236 |
end); |
237 |
||
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
238 |
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
|
239 |