author | wenzelm |
Fri, 17 Sep 2010 20:56:32 +0200 | |
changeset 39509 | cab2719398a7 |
parent 39234 | d76a2fd129b5 |
child 39513 | fce2202892c4 |
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. |
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 |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
10 |
val isabelle_processN: string |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
11 |
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
|
12 |
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
|
13 |
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
|
14 |
val init: string -> string -> unit |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
15 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
16 |
|
31797 | 17 |
structure Isabelle_Process: ISABELLE_PROCESS = |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
18 |
struct |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
19 |
|
26550 | 20 |
(* print modes *) |
25554 | 21 |
|
25748 | 22 |
val isabelle_processN = "isabelle_process"; |
23 |
||
26550 | 24 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
28036 | 25 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup; |
25841 | 26 |
|
27 |
||
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
28 |
(* commands *) |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
29 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
30 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
31 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
32 |
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
|
33 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
34 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
35 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
(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
|
39 |
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
|
40 |
Symtab.update (name, cmd) cmds))); |
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 |
fun command name args = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
43 |
(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
|
44 |
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
|
45 |
| SOME cmd => cmd args); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
46 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
47 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
48 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
49 |
|
25841 | 50 |
(* message markup *) |
51 |
||
52 |
local |
|
25810 | 53 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
54 |
fun chunk s = string_of_int (size s) ^ "\n" ^ s; |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
55 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
56 |
fun message _ _ _ "" = () |
38445
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
57 |
| message out_stream ch raw_props body = |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
58 |
let |
38445
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38270
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end; |
25554 | 62 |
|
63 |
in |
|
64 |
||
39509
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
65 |
fun standard_message out_stream with_serial ch body = |
38871 | 66 |
message out_stream ch |
39509
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
67 |
((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
|
68 |
(Position.properties_of (Position.thread_data ()))) body; |
25554 | 69 |
|
28044 | 70 |
fun init_message out_stream = |
34214
99eefb83a35d
simplified init message -- removed redundant session property;
wenzelm
parents:
34206
diff
changeset
|
71 |
message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ()); |
25748 | 72 |
|
25554 | 73 |
end; |
74 |
||
75 |
||
25841 | 76 |
(* channels *) |
77 |
||
28188 | 78 |
local |
79 |
||
80 |
fun auto_flush stream = |
|
81 |
let |
|
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
82 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF); |
28188 | 83 |
fun loop () = |
38256 | 84 |
(OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ()); |
28188 | 85 |
in loop end; |
86 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
87 |
fun rendezvous f fifo = |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
88 |
let |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
89 |
val path = File.platform_path (Path.explode fifo); |
38254
fb1b255d6e36
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
wenzelm
parents:
38253
diff
changeset
|
90 |
val result = f fifo; (*should block until peer is ready*) |
fb1b255d6e36
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
wenzelm
parents:
38253
diff
changeset
|
91 |
val _ = |
fb1b255d6e36
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
wenzelm
parents:
38253
diff
changeset
|
92 |
if String.isSuffix "cygwin" ml_platform then () (*Cygwin 1.7: no proper blocking on open*) |
fb1b255d6e36
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
wenzelm
parents:
38253
diff
changeset
|
93 |
else OS.FileSys.remove path; (*prevent future access*) |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
94 |
in result end; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
95 |
|
28188 | 96 |
in |
97 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
98 |
fun setup_channels in_fifo out_fifo = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
99 |
let |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
100 |
val in_stream = rendezvous TextIO.openIn in_fifo; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
101 |
val out_stream = rendezvous TextIO.openOut out_fifo; |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
102 |
val _ = Simple_Thread.fork false (auto_flush out_stream); |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
103 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut); |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
104 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr); |
28044 | 105 |
in |
39509
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
106 |
Output.status_fn := standard_message out_stream false "B"; |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
107 |
Output.report_fn := standard_message out_stream false "C"; |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
108 |
Output.writeln_fn := standard_message out_stream true "D"; |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
109 |
Output.tracing_fn := standard_message out_stream true "E"; |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
110 |
Output.warning_fn := standard_message out_stream true "F"; |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
111 |
Output.error_fn := standard_message out_stream true "G"; |
cab2719398a7
Isabelle_Process: status/report do not require serial numbers;
wenzelm
parents:
39234
diff
changeset
|
112 |
Output.debug_fn := standard_message out_stream true "H"; |
37121
8e51fc35d59f
eliminated obsolete priority message from Isabelle_Process protocol;
wenzelm
parents:
36950
diff
changeset
|
113 |
Output.priority_fn := ! Output.writeln_fn; |
28498 | 114 |
Output.prompt_fn := ignore; |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
115 |
(in_stream, out_stream) |
28044 | 116 |
end; |
25841 | 117 |
|
28188 | 118 |
end; |
119 |
||
25841 | 120 |
|
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38871
diff
changeset
|
121 |
(* protocol loop -- uninterruptible *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
122 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
123 |
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
|
124 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
125 |
local |
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 |
fun recover crash = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
128 |
(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
|
129 |
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
|
130 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
131 |
fun read_chunk stream len = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
132 |
let |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
133 |
val n = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
134 |
(case Int.fromString len of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
135 |
SOME n => n |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
136 |
| 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
|
137 |
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
|
138 |
val m = size chunk; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
139 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
140 |
if m = n then chunk |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
141 |
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
|
142 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
143 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
144 |
fun read_command stream = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
145 |
(case TextIO.inputLine stream of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
146 |
NONE => raise Runtime.TERMINATE |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
147 |
| 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
|
148 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
149 |
fun run_command name args = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
150 |
Runtime.debugging (command name) args |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
151 |
handle exn => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
152 |
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
|
153 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
154 |
in |
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 |
fun loop stream = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
157 |
let val continue = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
158 |
(case read_command stream of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
159 |
[] => (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
|
160 |
| 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
|
161 |
handle Runtime.TERMINATE => false |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
162 |
| 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
|
163 |
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
|
164 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
165 |
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 |
|
25554 | 168 |
(* init *) |
169 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
170 |
fun init in_fifo out_fifo = |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
171 |
let |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
172 |
val _ = Unsynchronized.change print_mode |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
173 |
(fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]); |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
174 |
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
|
175 |
val _ = init_message out_stream; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
176 |
val _ = quick_and_dirty := true; (* FIXME !? *) |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
177 |
val _ = Keyword.status (); |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
178 |
val _ = Output.status (Markup.markup Markup.ready ""); |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
179 |
val _ = Context.set_thread_data NONE; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
180 |
val _ = Simple_Thread.fork false (fn () => (loop in_stream; quit ())); |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38256
diff
changeset
|
181 |
in () end; |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
182 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
183 |
end; |