author | wenzelm |
Mon, 25 Oct 2010 21:23:09 +0200 | |
changeset 40133 | b61d52de66f0 |
parent 40132 | 7ee65dbffa31 |
child 40134 | 8baded087d34 |
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 |
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
5 |
robustness and performance. |
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: |
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
|
8 |
. raw Posix process startup with uncontrolled output on stdout/stderr |
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
|
9 |
. stdout \002: ML running |
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
|
10 |
.. stdin/stdout/stderr freely available (raw ML loop) |
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
|
11 |
.. protocol thread initialization |
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
|
12 |
... switch to in_fifo/out_fifo channels (rendezvous via open) |
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
|
13 |
... out_fifo INIT(pid): channels ready |
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
|
14 |
... out_fifo STATUS(keywords) |
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
|
15 |
... out_fifo READY: main loop ready |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
16 |
*) |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
17 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
18 |
signature ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
19 |
sig |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
20 |
val isabelle_processN: string |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
21 |
val add_command: string -> (string list -> unit) -> unit |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
22 |
val command: string -> string list -> unit |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
23 |
val crashes: exn list Unsynchronized.ref |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
24 |
val init: string -> string -> unit |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
25 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
26 |
|
31797 | 27 |
structure Isabelle_Process: ISABELLE_PROCESS = |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
28 |
struct |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
29 |
|
26550 | 30 |
(* print modes *) |
25554 | 31 |
|
25748 | 32 |
val isabelle_processN = "isabelle_process"; |
33 |
||
26550 | 34 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
28036 | 35 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup; |
25841 | 36 |
|
37 |
||
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
38 |
(* commands *) |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
39 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
40 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
41 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
42 |
val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
43 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
44 |
in |
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 |
fun add_command name cmd = CRITICAL (fn () => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
47 |
Unsynchronized.change global_commands (fn cmds => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
48 |
(if not (Symtab.defined cmds name) then () |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
49 |
else warning ("Redefining Isabelle process command " ^ quote name); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
50 |
Symtab.update (name, cmd) cmds))); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
51 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
52 |
fun command name args = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
53 |
(case Symtab.lookup (! global_commands) name of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
54 |
NONE => error ("Undefined Isabelle process command " ^ quote name) |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
55 |
| SOME cmd => cmd args); |
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 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
58 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
59 |
|
25841 | 60 |
(* message markup *) |
61 |
||
62 |
local |
|
25810 | 63 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
64 |
fun chunk s = string_of_int (size s) ^ "\n" ^ s; |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
65 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
66 |
fun message _ _ _ "" = () |
38445
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
67 |
| message out_stream ch raw_props body = |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
68 |
let |
38445
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
69 |
val robust_props = map (pairself YXML.escape_controls) raw_props; |
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
70 |
val header = YXML.string_of (XML.Elem ((ch, robust_props), [])); |
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
71 |
in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end; |
25554 | 72 |
|
73 |
in |
|
74 |
||
39509
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
75 |
fun standard_message out_stream with_serial ch body = |
38871 | 76 |
message out_stream ch |
39509
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
77 |
((if with_serial then cons (Markup.serialN, serial_string ()) else I) |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
78 |
(Position.properties_of (Position.thread_data ()))) body; |
25554 | 79 |
|
28044 | 80 |
fun init_message out_stream = |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39530
diff
changeset
|
81 |
message out_stream "A" [] (Session.welcome ()); |
25748 | 82 |
|
25554 | 83 |
end; |
84 |
||
85 |
||
25841 | 86 |
(* channels *) |
87 |
||
28188 | 88 |
local |
89 |
||
90 |
fun auto_flush stream = |
|
91 |
let |
|
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
92 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF); |
28188 | 93 |
fun loop () = |
38256 | 94 |
(OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ()); |
28188 | 95 |
in loop end; |
96 |
||
97 |
in |
|
98 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
99 |
fun setup_channels in_fifo out_fifo = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
100 |
let |
39530
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
101 |
(*rendezvous*) |
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
102 |
val in_stream = TextIO.openIn in_fifo; |
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
103 |
val out_stream = TextIO.openOut out_fifo; |
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
104 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
105 |
val _ = Simple_Thread.fork false (auto_flush out_stream); |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
106 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut); |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
107 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr); |
28044 | 108 |
in |
40133
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
109 |
Output.Private_Hooks.status_fn := standard_message out_stream false "B"; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
110 |
Output.Private_Hooks.report_fn := standard_message out_stream false "C"; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
111 |
Output.Private_Hooks.writeln_fn := standard_message out_stream true "D"; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
112 |
Output.Private_Hooks.tracing_fn := standard_message out_stream true "E"; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
113 |
Output.Private_Hooks.warning_fn := standard_message out_stream true "F"; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
114 |
Output.Private_Hooks.error_fn := standard_message out_stream true "G"; |
b61d52de66f0
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
wenzelm
parents:
40132
diff
changeset
|
115 |
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
|
116 |
Output.Private_Hooks.prompt_fn := ignore; |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
117 |
(in_stream, out_stream) |
28044 | 118 |
end; |
25841 | 119 |
|
28188 | 120 |
end; |
121 |
||
25841 | 122 |
|
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38871
diff
changeset
|
123 |
(* protocol loop -- uninterruptible *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
124 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
125 |
val crashes = Unsynchronized.ref ([]: exn list); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
126 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
127 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
128 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
129 |
fun recover crash = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
130 |
(CRITICAL (fn () => Unsynchronized.change crashes (cons crash)); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
131 |
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
|
132 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
133 |
fun read_chunk stream len = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
134 |
let |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
135 |
val n = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
136 |
(case Int.fromString len of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
137 |
SOME n => n |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
138 |
| NONE => error ("Isabelle process: malformed chunk header " ^ quote len)); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
139 |
val chunk = TextIO.inputN (stream, n); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
140 |
val m = size chunk; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
141 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
142 |
if m = n then chunk |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
143 |
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
|
144 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
145 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
146 |
fun read_command stream = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
147 |
(case TextIO.inputLine stream of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
148 |
NONE => raise Runtime.TERMINATE |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
149 |
| SOME line => map (read_chunk stream) (space_explode "," line)); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
150 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
151 |
fun run_command name args = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
152 |
Runtime.debugging (command name) args |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
153 |
handle exn => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
154 |
error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
155 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
156 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
157 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
158 |
fun loop stream = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
159 |
let val continue = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
160 |
(case read_command stream of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
161 |
[] => (Output.error_msg "Isabelle process: no input"; true) |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
162 |
| name :: args => (run_command name args; true)) |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
163 |
handle Runtime.TERMINATE => false |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
164 |
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
165 |
in if continue then loop stream else () end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
166 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
167 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
168 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
169 |
|
25554 | 170 |
(* init *) |
171 |
||
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
|
172 |
fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () => |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
173 |
let |
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
|
174 |
val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*) |
39733
6d373e9dcb9d
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
wenzelm
parents:
39626
diff
changeset
|
175 |
val _ = Output.raw_stdout 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
|
176 |
|
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
|
177 |
val _ = quick_and_dirty := true; (* FIXME !? *) |
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
|
178 |
val _ = Context.set_thread_data NONE; |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
179 |
val _ = Unsynchronized.change print_mode |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
180 |
(fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]); |
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
|
181 |
|
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
182 |
val (in_stream, out_stream) = setup_channels in_fifo out_fifo; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
183 |
val _ = init_message out_stream; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
184 |
val _ = Keyword.status (); |
39626
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39591
diff
changeset
|
185 |
val _ = Output.status (Markup.markup Markup.ready "process ready"); |
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
|
186 |
in loop in_stream end)); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
187 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
188 |
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
|
189 |