author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 34243 | 8821e3293702 |
child 36735 | 42b7f881f5fc |
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 |
28044 | 14 |
val init: 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 |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
37 |
val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, [])); |
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 () = |
60 |
(OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ()); |
|
61 |
in loop end; |
|
62 |
||
63 |
in |
|
64 |
||
28044 | 65 |
fun setup_channels out = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
66 |
let |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
67 |
val path = File.platform_path (Path.explode out); |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
68 |
val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*) |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
69 |
val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*) |
28242 | 70 |
val _ = SimpleThread.fork false (auto_flush out_stream); |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
71 |
val _ = SimpleThread.fork false (auto_flush TextIO.stdOut); |
28242 | 72 |
val _ = SimpleThread.fork false (auto_flush TextIO.stdErr); |
28044 | 73 |
in |
34096
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
74 |
Output.status_fn := standard_message out_stream "B"; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
75 |
Output.writeln_fn := standard_message out_stream "C"; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
76 |
Output.priority_fn := standard_message out_stream "D"; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
77 |
Output.tracing_fn := standard_message out_stream "E"; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
78 |
Output.warning_fn := standard_message out_stream "F"; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
79 |
Output.error_fn := standard_message out_stream "G"; |
e438a5875c16
simplified message format: chunks with explicit size in bytes;
wenzelm
parents:
33225
diff
changeset
|
80 |
Output.debug_fn := standard_message out_stream "H"; |
28498 | 81 |
Output.prompt_fn := ignore; |
28044 | 82 |
out_stream |
83 |
end; |
|
25841 | 84 |
|
28188 | 85 |
end; |
86 |
||
25841 | 87 |
|
25554 | 88 |
(* init *) |
89 |
||
28044 | 90 |
fun init out = |
34243
8821e3293702
report keywords as singleton messages, control message kind via print mode;
wenzelm
parents:
34214
diff
changeset
|
91 |
(Unsynchronized.change print_mode |
8821e3293702
report keywords as singleton messages, control message kind via print mode;
wenzelm
parents:
34214
diff
changeset
|
92 |
(fold (update (op =)) [isabelle_processN, OuterKeyword.keyword_status_reportN]); |
28044 | 93 |
setup_channels out |> init_message; |
28342 | 94 |
OuterKeyword.report (); |
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30173
diff
changeset
|
95 |
Output.status (Markup.markup Markup.ready ""); |
26643 | 96 |
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true}); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
97 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
98 |
end; |