1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
18
open Protectedtoplevel
20
(* A buffer for the character read from a channel. We store the command
21
* entered to be able to report errors without pretty-printing. *)
24
mutable prompt : unit -> string;
25
mutable str : string; (* buffer of already read characters *)
26
mutable len : int; (* number of chars in the buffer *)
27
mutable bols : int list; (* offsets in str of begining of lines *)
28
mutable tokens : Gram.parsable; (* stream of tokens *)
29
mutable start : int } (* stream count of the first char of the buffer *)
31
(* Double the size of the buffer. *)
33
let resize_buffer ibuf =
34
let nstr = String.create (2 * String.length ibuf.str + 1) in
35
String.blit ibuf.str 0 nstr 0 (String.length ibuf.str);
38
(* Delete all irrelevent lines of the input buffer. Keep the last line
39
in the buffer (useful when there are several commands on the same line. *)
41
let resynch_buffer ibuf =
44
let new_len = ibuf.len - ll in
45
String.blit ibuf.str ll ibuf.str 0 new_len;
48
ibuf.start <- ibuf.start + ll
52
(* emacs special character for prompt end (fast) detection. Prefer
53
(Char.chr 6) since it does not interfere with utf8. For
54
compatibility we let (Char.chr 249) as default for a while. *)
56
let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>"
58
let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>"
60
(* Read a char in an input channel, displaying a prompt at every
62
let prompt_char ic ibuf count =
63
let bol = match ibuf.bols with
64
| ll::_ -> ibuf.len == ll
67
if bol && not !print_emacs then msgerr (str (ibuf.prompt()));
69
let c = input_char ic in
70
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
71
if ibuf.len == String.length ibuf.str then resize_buffer ibuf;
72
ibuf.str.[ibuf.len] <- c;
73
ibuf.len <- ibuf.len + 1;
78
(* Reinitialize the char stream (after a Drop) *)
80
let reset_input_buffer ic ibuf =
84
ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf));
87
(* Functions to print underlined locations from an input buffer. *)
89
(* Given a location, returns the list of locations of each line. The last
90
line is returned separately. It also checks the location bounds. *)
92
let get_bols_of_loc ibuf (bp,ep) =
93
let add_line (b,e) lines =
94
if b < 0 or e < b then anomaly "Bad location";
96
| ([],None) -> ([], Some (b,e))
97
| (fl,oe) -> ((b,e)::fl, oe)
99
let rec lines_rec ba after = function
100
| [] -> add_line (0,ba) after
101
| ll::_ when ll <= bp -> add_line (ll,ba) after
103
let nafter = if ll < ep then add_line (ll,ba) after else after in
104
lines_rec ll nafter fl
106
let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in
109
let dotted_location (b,e) =
111
("", String.make (e-b) ' ')
113
(String.make (e-b-1) '.', " ")
115
let print_highlight_location ib loc =
116
let (bp,ep) = unloc loc in
117
let bp = bp - ib.start
118
and ep = ep - ib.start in
119
let highlight_lines =
120
match get_bols_of_loc ib (bp,ep) with
122
(str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++
123
str"> " ++ str(String.make (bp-bl) ' ') ++
124
str(String.make (ep-bp) '^'))
125
| ((b1,e1)::ml,(bn,en)) ->
126
let (d1,s1) = dotted_location (b1,bp) in
127
let (dn,sn) = dotted_location (ep,en) in
128
let l1 = (str"> " ++ str d1 ++ str s1 ++
129
str(String.sub ib.str bp (e1-bp))) in
131
prlist (fun (bi,ei) ->
132
(str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in
133
let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++
137
let loc = make_loc (bp,ep) in
138
(str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++
139
highlight_lines ++ fnl ())
141
(* Functions to report located errors in a file. *)
143
let print_location_in_file s inlibrary fname loc =
144
let errstrm = str"Error while reading " ++ str s in
145
if loc = dummy_loc then
146
hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
149
if s = fname then mt() else errstrm ++ str":" ++ fnl() in
151
hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
152
str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
154
let (bp,ep) = unloc loc in
155
let ic = open_in fname in
156
let rec line_of_pos lin bol cnt =
158
if input_char ic == '\n'
159
then line_of_pos (lin + 1) (cnt +1) (cnt+1)
160
else line_of_pos lin bol (cnt+1)
164
let (line, bol) = line_of_pos 1 0 0 in
167
(errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
168
hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
170
Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
174
hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
176
let print_command_location ib dloc =
179
(str"Error during interpretation of command:" ++ fnl () ++
180
str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
183
let valid_loc dloc loc =
187
let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
190
let valid_buffer_loc ib dloc loc =
192
let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
194
(*s The Coq prompt is the name of the focused proof, if any, and "Coq"
195
otherwise. We trap all exceptions to prevent the error message printing
199
(Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < "
203
(*let build_pending_list l =
207
while List.length !l' > 1 do
208
pl := !pl ^ "|" Names.string_of_id x;
211
let last = try List.hd !l' with _ -> in
215
(* the coq prompt added to the default one when in emacs mode
216
The prompt contains the current state label [n] (for global
217
backtracking) and the current proof state [p] (for proof
218
backtracking) plus the list of open (nested) proofs (for proof
219
aborting when backtracking). It looks like:
221
"n |lem1|lem2|lem3| p < "
223
let make_emacs_prompt() =
224
let statnum = string_of_int (Lib.current_command_label ()) in
225
let dpth = Pfedit.current_proof_depth() in
226
let pending = Pfedit.get_all_proof_names() in
229
(fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x)
231
let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
232
if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
235
(* A buffer to store the current command read on stdin. It is
236
* initialized when a vernac command is immediately followed by "\n",
237
* or after a Drop. *)
240
emacs_prompt_startstring()
242
^ make_emacs_prompt()
243
^ emacs_prompt_endstring()
249
tokens = Gram.parsable (Stream.of_list []);
252
let set_prompt prompt =
255
emacs_prompt_startstring()
257
^ emacs_prompt_endstring())
259
(* Removes and prints the location of the error. The following exceptions
260
need not be located. *)
261
let rec is_pervasive_exn = function
262
| Out_of_memory | Stack_overflow | Sys.Break -> true
263
| Error_in_file (_,_,e) -> is_pervasive_exn e
264
| Stdpp.Exc_located (_,e) -> is_pervasive_exn e
265
| DuringCommandInterp (_,e) -> is_pervasive_exn e
266
| DuringSyntaxChecking e -> is_pervasive_exn e
269
(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
270
May raise only the following exceptions: Drop and End_of_input,
271
meaning we get out of the Coq loop *)
272
let print_toplevel_error exc =
275
| DuringCommandInterp (loc,ie)
276
| Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
277
if loc = dummy_loc then (None,ie) else (Some loc, ie)
282
| Stdpp.Exc_located (loc, ie) ->
283
if valid_buffer_loc top_buffer dloc loc then
284
(print_highlight_location top_buffer loc, ie)
286
((mt ()) (* print_command_location top_buffer dloc *), ie)
287
| Error_in_file (s, (inlibrary, fname, loc), ie) ->
288
(print_location_in_file s inlibrary fname loc, ie)
290
((mt ()) (* print_command_location top_buffer dloc *), exc)
294
msgerrnl (mt ()); pp_flush(); exit 0
295
| Vernacexpr.Drop -> (* Last chance *)
296
if Mltop.is_ocaml_top() then raise Vernacexpr.Drop;
297
(str"Error: There is no ML toplevel." ++ fnl ())
298
| Vernacexpr.ProtectedLoop ->
299
raise Vernacexpr.ProtectedLoop
301
raise Vernacexpr.Quit
303
(if is_pervasive_exn exc then (mt ()) else locstrm) ++
304
Cerrors.explain_exn exc
306
(* Read the input stream until a dot is encountered *)
308
let rec dot st = match Stream.next st with
310
| ("EOI", "") -> raise End_of_input
313
Gram.Entry.of_parser "Coqtoplevel.dot" dot
315
(* We assume that when a lexer error occurs, at least one char was eaten *)
316
let rec discard_to_dot () =
318
Gram.Entry.parse parse_to_dot top_buffer.tokens
319
with Stdpp.Exc_located(_,Token.Error _) ->
323
(* If the error occured while parsing, we read the input until a dot token
326
let process_error = function
327
| DuringCommandInterp _
328
| Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
330
if is_pervasive_exn e then
336
| End_of_input -> End_of_input
337
| de -> if is_pervasive_exn de then de else e
339
(* do_vernac reads and executes a toplevel phrase, and print error
340
messages when an exception is raised, except for the following:
341
Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
343
End_of_input: Ctrl-D was typed in, we will quit *)
346
if !print_emacs then msgerr (str (top_buffer.prompt()));
347
resynch_buffer top_buffer;
350
raw_do_vernac top_buffer.tokens
352
msgnl (print_toplevel_error (process_error e))
356
(* coq and go read vernacular expressions until Drop is entered.
357
* Ctrl-C will raise the exception Break instead of aborting Coq.
358
* Here we catch the exceptions terminating the Coq loop, and decide
359
* if we really must quit.
360
* The boolean value is used to choose between a protected loop, which
361
* we think is more suited for communication with other programs, or
362
* plain communication. *)
364
let rec coq_switch b =
365
Sys.catch_break true;
366
(* ensure we have a command separator object (DOT) so that the first
367
command can be reseted. *)
368
Lib.mark_end_of_command();
371
reset_input_buffer stdin top_buffer;
372
while true do do_vernac() done
376
| Vernacexpr.Drop -> ()
377
| Vernacexpr.ProtectedLoop ->
378
Lib.declare_initial_state();
380
| End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
381
| Vernacexpr.Quit -> exit 0
383
msgerrnl (str"Anomaly. Please report.");
386
let loop () = coq_switch true
added
removed
toplevel/toplevel.ml
