author | wenzelm |
Fri, 04 Jan 2013 12:33:25 +0100 | |
changeset 50715 | 8cfd585b9162 |
parent 50698 | 49621c755075 |
child 50911 | ee7fe4230642 |
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 |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
20 |
val tracing_messages: int Unsynchronized.ref; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
21 |
val reset_tracing: unit -> unit |
43684 | 22 |
val crashes: exn list Synchronized.var |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
23 |
val init_fifos: string -> string -> unit |
45028 | 24 |
val init_socket: 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 |
|
42897 | 30 |
(* print mode *) |
25554 | 31 |
|
25748 | 32 |
val isabelle_processN = "isabelle_process"; |
33 |
||
42897 | 34 |
fun is_active () = Print_Mode.print_mode_active isabelle_processN; |
35 |
||
26550 | 36 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
28036 | 37 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup; |
25841 | 38 |
|
39 |
||
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
40 |
(* protocol commands *) |
38270
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 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
43 |
|
43684 | 44 |
val commands = |
45 |
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
|
46 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
47 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
48 |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
49 |
fun protocol_command name cmd = |
43684 | 50 |
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
|
51 |
(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
|
52 |
else warning ("Redefining Isabelle process command " ^ quote name); |
43684 | 53 |
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
|
54 |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
55 |
fun run_command name args = |
43684 | 56 |
(case Symtab.lookup (Synchronized.value commands) name of |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
57 |
NONE => error ("Undefined Isabelle process command " ^ quote name) |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
58 |
| SOME cmd => |
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45666
diff
changeset
|
59 |
(Runtime.debugging cmd args handle exn => |
48056 | 60 |
error ("Isabelle process protocol failure: " ^ quote name ^ "\n" ^ |
61 |
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
|
62 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
63 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
64 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
65 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
66 |
(* restricted tracing messages *) |
49647 | 67 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
68 |
val tracing_messages = Unsynchronized.ref 100; |
49647 | 69 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
70 |
val command_tracing_messages = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
71 |
Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table); |
49647 | 72 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
73 |
fun reset_tracing () = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
74 |
Synchronized.change command_tracing_messages (K Inttab.empty); |
49647 | 75 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
76 |
fun update_tracing () = |
49647 | 77 |
(case Position.get_id (Position.thread_data ()) of |
78 |
NONE => () |
|
79 |
| SOME id => |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
80 |
let |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
81 |
val i = Markup.parse_int id; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
82 |
val (n, ok) = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
83 |
Synchronized.change_result command_tracing_messages (fn tab => |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
84 |
let |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
85 |
val n = the_default 0 (Inttab.lookup tab i) + 1; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
86 |
val ok = n <= ! tracing_messages; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
87 |
in ((n, ok), Inttab.update (i, n) tab) end); |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
88 |
in |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
89 |
if ok then () |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
90 |
else |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
91 |
let |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
92 |
val (text, promise) = Active.dialog_text (); |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
93 |
val _ = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
94 |
writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
95 |
text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?") |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
96 |
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
|
97 |
handle Fail _ => error "Stopped"; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
98 |
in |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
99 |
Synchronized.change command_tracing_messages |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
100 |
(Inttab.map_default (i, 0) (fn k => k - m)) |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
101 |
end |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
102 |
end); |
49647 | 103 |
|
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 |
(* message channels *) |
25841 | 106 |
|
107 |
local |
|
25810 | 108 |
|
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
|
109 |
fun chunk s = [string_of_int (size s), "\n", s]; |
26574
560d07845442
support "YXML" mode for output transfer notation;
wenzelm
parents:
26550
diff
changeset
|
110 |
|
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
111 |
fun message do_flush mbox name raw_props body = |
43771
fc524449f511
allow empty body for raw_message -- important for Invoke_Scala;
wenzelm
parents:
43746
diff
changeset
|
112 |
let |
43772
c825594fd0c1
clarified YXML.embed_controls -- this is idempotent and cannot be nested;
wenzelm
parents:
43771
diff
changeset
|
113 |
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
|
114 |
val header = YXML.string_of (XML.Elem ((name, robust_props), [])); |
44731
8f7b3a89fc15
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
wenzelm
parents:
44389
diff
changeset
|
115 |
in Mailbox.send mbox (chunk header @ chunk body, do_flush) end; |
25554 | 116 |
|
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
117 |
fun standard_message mbox opt_serial name body = |
43771
fc524449f511
allow empty body for raw_message -- important for Invoke_Scala;
wenzelm
parents:
43746
diff
changeset
|
118 |
if body = "" then () |
fc524449f511
allow empty body for raw_message -- important for Invoke_Scala;
wenzelm
parents:
43746
diff
changeset
|
119 |
else |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
120 |
message false mbox name |
50254
935ac0ad7e83
prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents:
50201
diff
changeset
|
121 |
((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) |
43771
fc524449f511
allow empty body for raw_message -- important for Invoke_Scala;
wenzelm
parents:
43746
diff
changeset
|
122 |
(Position.properties_of (Position.thread_data ()))) body; |
25554 | 123 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
124 |
fun message_output mbox channel = |
28188 | 125 |
let |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
126 |
fun flush () = ignore (try System_Channel.flush channel); |
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
|
127 |
fun loop receive = |
8baded087d34
explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
wenzelm
parents:
40133
diff
changeset
|
128 |
(case receive mbox of |
44731
8f7b3a89fc15
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
wenzelm
parents:
44389
diff
changeset
|
129 |
SOME (msg, do_flush) => |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
130 |
(List.app (fn s => System_Channel.output channel s) msg; |
44731
8f7b3a89fc15
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
wenzelm
parents:
44389
diff
changeset
|
131 |
if do_flush then flush () else (); |
40301 | 132 |
loop (Mailbox.receive_timeout (seconds 0.02))) |
44731
8f7b3a89fc15
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
wenzelm
parents:
44389
diff
changeset
|
133 |
| NONE => (flush (); loop (SOME o Mailbox.receive))); |
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
|
134 |
in fn () => loop (SOME o Mailbox.receive) end; |
28188 | 135 |
|
136 |
in |
|
137 |
||
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
138 |
fun init_channels channel = |
28189
fbad2eb5be9e
auto_flush: uniform block buffering for all output streams;
wenzelm
parents:
28188
diff
changeset
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
|
44731
8f7b3a89fc15
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
wenzelm
parents:
44389
diff
changeset
|
143 |
val mbox = Mailbox.create () : (string list * bool) Mailbox.T; |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
144 |
val _ = Simple_Thread.fork false (message_output mbox channel); |
28044 | 145 |
in |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
146 |
Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN; |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
147 |
Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN; |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50455
diff
changeset
|
148 |
Output.Private_Hooks.result_fn := |
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50455
diff
changeset
|
149 |
(fn (i, s) => standard_message mbox (SOME i) Markup.resultN s); |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
150 |
Output.Private_Hooks.writeln_fn := |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
151 |
(fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s); |
49647 | 152 |
Output.Private_Hooks.tracing_fn := |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
153 |
(fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s)); |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
154 |
Output.Private_Hooks.warning_fn := |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
155 |
(fn s => standard_message mbox (SOME (serial ())) Markup.warningN s); |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49661
diff
changeset
|
156 |
Output.Private_Hooks.error_fn := |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
157 |
(fn (i, s) => standard_message mbox (SOME i) Markup.errorN s); |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
158 |
Output.Private_Hooks.protocol_message_fn := message true mbox 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
|
159 |
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
|
160 |
Output.Private_Hooks.prompt_fn := ignore; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50119
diff
changeset
|
161 |
message true mbox Markup.initN [] (Session.welcome ()) |
28044 | 162 |
end; |
25841 | 163 |
|
28188 | 164 |
end; |
165 |
||
25841 | 166 |
|
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38871
diff
changeset
|
167 |
(* protocol loop -- uninterruptible *) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
168 |
|
43684 | 169 |
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
|
170 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
171 |
local |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
172 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
173 |
fun recover crash = |
43684 | 174 |
(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
|
175 |
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
|
176 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
177 |
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
|
178 |
let |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
179 |
val n = |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
180 |
(case Int.fromString len of |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
181 |
SOME n => n |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
182 |
| NONE => error ("Isabelle process: malformed chunk header " ^ quote len)); |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
183 |
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
|
184 |
val m = size chunk; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
185 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
186 |
if m = n then chunk |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
187 |
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
|
188 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
189 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
190 |
fun read_command channel = |
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
191 |
(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
|
192 |
NONE => raise Runtime.TERMINATE |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
193 |
| 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
|
194 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
195 |
in |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
196 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
197 |
fun loop channel = |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
198 |
let val continue = |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
199 |
(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
|
200 |
[] => (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
|
201 |
| 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
|
202 |
handle Runtime.TERMINATE => false |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
203 |
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true); |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
204 |
in if continue then loop channel else () end; |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
205 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
206 |
end; |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
207 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38265
diff
changeset
|
208 |
|
25554 | 209 |
(* init *) |
210 |
||
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
211 |
val default_modes1 = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50698
diff
changeset
|
212 |
[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
|
213 |
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]; |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
214 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
215 |
fun init rendezvous = 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
|
216 |
let |
40301 | 217 |
val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*) |
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
|
218 |
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
|
219 |
|
49661
ac48def96b69
enable show_markup by default (approx. double output size);
wenzelm
parents:
49647
diff
changeset
|
220 |
val _ = Printer.show_markup_default := true; |
47396
c1d297ef7969
enable parallel proofs (cf. e8552cba702d), only affects packages so far;
wenzelm
parents:
46774
diff
changeset
|
221 |
val _ = quick_and_dirty := false; |
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
|
222 |
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
|
223 |
val _ = |
a250b092ac66
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
wenzelm
parents:
42897
diff
changeset
|
224 |
Unsynchronized.change print_mode |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49108
diff
changeset
|
225 |
(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
|
226 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
227 |
val channel = rendezvous (); |
48712
6b7a9bcc0bae
simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents:
48710
diff
changeset
|
228 |
val _ = init_channels channel; |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
229 |
in loop channel end)); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
230 |
|
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45028
diff
changeset
|
231 |
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
|
232 |
fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); |
45028 | 233 |
|
50117 | 234 |
|
235 |
(* options *) |
|
236 |
||
237 |
val _ = |
|
238 |
protocol_command "Isabelle_Process.options" |
|
239 |
(fn [options_yxml] => |
|
240 |
let val options = Options.decode (YXML.parse_body options_yxml) in |
|
50698
49621c755075
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
wenzelm
parents:
50505
diff
changeset
|
241 |
Future.ML_statistics := true; |
50117 | 242 |
Multithreading.trace := Options.int options "threads_trace"; |
243 |
Multithreading.max_threads := Options.int options "threads"; |
|
244 |
if Multithreading.max_threads_value () < 2 |
|
245 |
then Multithreading.max_threads := 2 else (); |
|
246 |
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0); |
|
50119
5c370a036de7
more generous tracing_limit, with explicit system option;
wenzelm
parents:
50117
diff
changeset
|
247 |
Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold"; |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50503
diff
changeset
|
248 |
tracing_messages := Options.int options "editor_tracing_messages" |
50117 | 249 |
end); |
250 |
||
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
251 |
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
|
252 |