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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: protectedtoplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Line_oriented_parser
open Vernac
open Vernacexpr
(* 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
(* Before outputing any data, output_results makes sure that no interrupt
is going to disturb the process. *)
let output_results_nl stream =
let _ = Sys.signal Sys.sigint
(Sys.Signal_handle(fun i -> 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_ref =
ref(fun request_id command_count opt_exn
-> (fnl () ++ str "acknowledge command number " ++
int request_id ++ fnl () ++
str "successfully executed " ++ int command_count ++ fnl () ++
str "error message" ++ fnl () ++
(match opt_exn with
Some e -> Cerrors.explain_exn e
| None -> (mt ())) ++ fnl () ++
str "E-n-d---M-e-s-s-a-g-e" ++ fnl ()))
let set_acknowledge_command f =
acknowledge_command_ref := f
let acknowledge_command request_id = !acknowledge_command_ref request_id
(* 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
exception E_with_rank of int * exn
let rec parse_one_command_group input_channel =
let count = ref 0 in
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 req_id_line = input_line input_channel in
begin
(try
global_request_id := int_of_string req_id_line
with
| e -> failwith ("could not parse the request identifier |"^
req_id_line ^ "|")) ;
let count_line = input_line input_channel in
begin
(try
count := int_of_string count_line
with
| e -> failwith("could not parse the count|" ^ count_line
^ "|"));
let stream_tail =
Stream.from
(line_oriented_channel_to_option
!end_marker input_channel) in
begin
check_break();
rearm_break();
let rec execute_n_commands rank =
if rank = !count then
None
else
let first_cmd_status =
try
raw_do_vernac
(Pcoq.Gram.parsable stream_tail);
None
with e -> Some(rank,e) in
match first_cmd_status with
None ->
execute_n_commands (rank + 1)
| v -> v in
let r = execute_n_commands 0 in
(match r with
None ->
output_results_nl
(acknowledge_command
!global_request_id !count None)
| Some(rank, e) ->
(match e with
| DuringCommandInterp(a,e1)
| Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
output_results_nl
(acknowledge_command
!global_request_id rank (Some e1))
| e ->
output_results_nl
(acknowledge_command
!global_request_id rank (Some e))));
rearm_break();
flush_until_end_of_stream stream_tail
end
end
end
else
parse_one_command_group input_channel
end else
parse_one_command_group input_channel
let protected_loop input_chan =
let rec explain_and_restart e =
begin
output_results_nl(Cerrors.explain_exn e);
rearm_break();
looprec input_chan;
end
and looprec input_chan =
try
while true do parse_one_command_group input_chan done
with
| Vernacexpr.Drop -> raise Vernacexpr.Drop
| Vernacexpr.Quit -> exit 0
| End_of_file -> exit 0
| DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
| DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
| DuringCommandInterp(loc, e)
| Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
explain_and_restart e
| e -> explain_and_restart e in
begin
msgnl (str "Starting Centaur Specialized loop");
looprec input_chan
end
|
