blob: 7af6dcc894377293f4738a81a0bf944e17dd4379 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(* $Id$ *)
open Pp
open Vernac
(* The toplevel parsing loop we propose here is more robust to printing
errors. The philosophy is that all commands should be individually wrapped
in predefined markers. If there is a parsing error, everything down to
the closing marker will be discarded. Also there is always an aknowledge
message associated to a wrapped command. *)
(* It is also possible to have break signals sent by other programs. However,
there are some operations that should not be interrupted, especially, those
operations that are outputing data.
*)
let break_happened = ref false
let output_results_nl stream =
let _ =
Sys.signal Sys.sigint
(Sys.Signal_handle (fun _ -> break_happened := true;()))
in
mSGNL stream
let rearm_break () =
let _ =
Sys.signal Sys.sigint (Sys.Signal_handle(fun _ -> raise Sys.Break)) in
()
let check_break () =
if !break_happened then begin
break_happened := false;
raise Sys.Break
end
(* All commands are acknowledged. *)
let global_request_id = ref 013
let acknowledge_command request_id =
[< 'fNL; 'sTR "message"; 'fNL; 'sTR "acknowledge"; 'fNL;
'iNT request_id; 'fNL; 'sTR "***"; 'fNL >]
(* The markers are chosen to be likely to be different from any
existing text. *)
let start_marker = ref "protected_loop_start_command"
let end_marker = ref "protected_loop_end_command"
let start_length = ref (String.length !start_marker)
let start_marker_buffer = ref (String.make !start_length ' ')
let set_start_marker s =
start_marker := s;
start_length := String.length s;
start_marker_buffer := String.make !start_length ' '
let set_end_marker s =
end_marker := s
let line_oriented_channel_to_option stop_string input_channel =
let count = ref 0 in
let buff = ref "" in
let current_length = ref 0 in
fun i ->
if (i - !count) >= !current_length then begin
count := !count + !current_length + 1;
buff := input_line input_channel;
if !buff = stop_string then
None
else begin
current_length := String.length !buff;
Some '\n'
end
end else
Some (String.get !buff (i - !count))
let flush_until_end_of_stream char_stream =
Stream.iter (function _ -> ()) char_stream
let rec parse_one_command input_channel =
let this_line = input_line input_channel in
if ((String.length this_line) >= !start_length) then begin
String.blit this_line 0 !start_marker_buffer 0 !start_length;
if !start_marker_buffer = !start_marker then
let snd_line = input_line input_channel in
begin
try
global_request_id := int_of_string snd_line
with
| e -> failwith ("could not parse the request identifier |"^
snd_line ^ "|")
end;
let stream_tail =
Stream.from
(line_oriented_channel_to_option !end_marker input_channel) in
begin
try
check_break();
rearm_break();
raw_do_vernac (Pcoq.Gram.parsable stream_tail);
output_results_nl(acknowledge_command !global_request_id);
rearm_break();
with
| e -> begin flush_until_end_of_stream stream_tail; raise e end
end;
flush_until_end_of_stream stream_tail
else
parse_one_command input_channel
end else
parse_one_command input_channel
let protected_loop input_chan =
let rec explain_and_restart e =
output_results_nl(Errors.explain_exn e);
rearm_break();
looprec input_chan;
and looprec input_chan =
try
while true do parse_one_command input_chan done
with
| Vernacinterp.Drop -> raise Vernacinterp.Drop
| Vernacinterp.Quit -> exit 0
| End_of_file -> exit 0
| DuringCommandInterp(loc, Vernacinterp.Quit) -> raise Vernacinterp.Quit
| DuringCommandInterp(loc, Vernacinterp.Drop) -> raise Vernacinterp.Drop
| DuringCommandInterp(loc, e) ->
explain_and_restart e
| e -> explain_and_restart e
in
mSGNL [<'sTR "Starting Centaur Specialized loop" >];
looprec input_chan
|
