author | wenzelm |
Tue, 10 Aug 2010 12:29:11 +0200 | |
changeset 38259 | 2b61c5e27399 |
parent 38256 | d2f094d97c91 |
child 38265 | cc9fde54311f |
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 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
4 |
Isabelle process wrapper. |
25631 | 5 |
|
6 |
General format of process output: |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
7 |
(1) message = "\002" header chunk body chunk |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
8 |
(2) chunk = size (ASCII digits) \n content (YXML) |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
9 |
*) |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
10 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
11 |
signature ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
12 |
sig |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
13 |
val isabelle_processN: string |
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 |
||
28 |
(* message markup *) |
|
29 |
||
30 |
local |
|
25810 | 31 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
32 |
fun chunk s = string_of_int (size s) ^ "\n" ^ s; |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
33 |
|
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
34 |
fun message _ _ _ "" = () |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
35 |
| message out_stream ch props body = |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
36 |
let |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37687
diff
changeset
|
37 |
val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), [])); |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
38 |
val msg = Symbol.STX ^ chunk header ^ chunk body; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
39 |
in TextIO.output (out_stream, msg) (*atomic output*) end; |
25554 | 40 |
|
41 |
in |
|
42 |
||
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
43 |
fun standard_message out_stream ch body = |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
44 |
message out_stream ch (Position.properties_of (Position.thread_data ())) body; |
25554 | 45 |
|
28044 | 46 |
fun init_message out_stream = |
34214
99eefb83a35d
simplified init message -- removed redundant session property;
wenzelm
parents:
34206
diff
changeset
|
47 |
message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ()); |
25748 | 48 |
|
25554 | 49 |
end; |
50 |
||
51 |
||
25841 | 52 |
(* channels *) |
53 |
||
28188 | 54 |
local |
55 |
||
56 |
fun auto_flush stream = |
|
57 |
let |
|
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
58 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF); |
28188 | 59 |
fun loop () = |
38256 | 60 |
(OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ()); |
28188 | 61 |
in loop end; |
62 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
63 |
fun rendezvous f fifo = |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
64 |
let |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
val _ = |
fb1b255d6e36
more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
wenzelm
parents:
38253
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
in result end; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
71 |
|
28188 | 72 |
in |
73 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
74 |
fun setup_channels in_fifo out_fifo = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
75 |
let |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
76 |
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
|
77 |
val out_stream = rendezvous TextIO.openOut out_fifo; |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
78 |
val _ = Simple_Thread.fork false (auto_flush out_stream); |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
79 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut); |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37191
diff
changeset
|
80 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr); |
28044 | 81 |
in |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
82 |
Output.status_fn := standard_message out_stream "B"; |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
83 |
Output.report_fn := standard_message out_stream "C"; |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
84 |
Output.writeln_fn := standard_message out_stream "D"; |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
85 |
Output.tracing_fn := standard_message out_stream "E"; |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
86 |
Output.warning_fn := standard_message out_stream "F"; |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
87 |
Output.error_fn := standard_message out_stream "G"; |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
88 |
Output.debug_fn := standard_message out_stream "H"; |
37121
8e51fc35d59f
eliminated obsolete priority message from Isabelle_Process protocol;
wenzelm
parents:
36950
diff
changeset
|
89 |
Output.priority_fn := ! Output.writeln_fn; |
28498 | 90 |
Output.prompt_fn := ignore; |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
91 |
(in_stream, out_stream) |
28044 | 92 |
end; |
25841 | 93 |
|
28188 | 94 |
end; |
95 |
||
25841 | 96 |
|
25554 | 97 |
(* init *) |
98 |
||
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
99 |
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
|
100 |
let |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
101 |
val _ = Unsynchronized.change print_mode |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
102 |
(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
|
103 |
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
|
104 |
val _ = init_message out_stream; |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
105 |
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
|
106 |
val _ = Keyword.status (); |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
107 |
val _ = Output.status (Markup.markup Markup.ready ""); |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38256
diff
changeset
|
108 |
val _ = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38256
diff
changeset
|
109 |
Simple_Thread.fork false (fn () => |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38256
diff
changeset
|
110 |
(Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true}; |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38256
diff
changeset
|
111 |
quit ())); |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38256
diff
changeset
|
112 |
in () end; |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
113 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
114 |
end; |