diff options
| -rw-r--r-- | toplevel/ide_slave.ml | 1 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 102 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 32 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 2 |
4 files changed, 42 insertions, 95 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 205890977..7758daf65 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -291,7 +291,6 @@ let eval_call c = match e with | Errors.Drop -> None, "Drop is not allowed by coqide!" | Errors.Quit -> None, "Quit is not allowed by coqide!" - | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner | Error_in_file (_,_,inner) -> None, pr_exn inner | e -> let loc = match Loc.get_loc e with diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 93a1c21f8..6947d95e7 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -182,15 +182,8 @@ let print_location_in_file s inlibrary fname loc = (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) -let valid_loc dloc loc = - not (Loc.is_ghost loc) - && match dloc with - | Some dloc -> - let (bd,ed) = Loc.unloc dloc in let (b,e) = Loc.unloc loc in bd<=b && e<=ed - | _ -> true - -let valid_buffer_loc ib dloc loc = - valid_loc dloc loc & +let valid_buffer_loc ib loc = + not (Loc.is_ghost loc) && let (b,e) = Loc.unloc loc in b-ib.start >= 0 & e-ib.start < ib.len && b<=e (*s The Coq prompt is the name of the focused proof, if any, and "Coq" @@ -263,43 +256,20 @@ let set_prompt prompt = let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e - | DuringCommandInterp (_,e) -> is_pervasive_exn e | _ -> false (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D May raise only the following exceptions: Drop and End_of_input, meaning we get out of the Coq loop *) -let print_toplevel_error exc = - let (dloc,exc) = - match exc with - | DuringCommandInterp (loc,ie) -> - if Loc.is_ghost loc then (None,ie) else (Some loc, ie) - | _ -> (None, exc) - in - let (locstrm,exc) = - match exc with - | Error_in_file (s, (inlibrary, fname, loc), ie) -> - (print_location_in_file s inlibrary fname loc, ie) - | ie -> - match Loc.get_loc ie with - | None -> (mt (), ie) - | Some loc -> - if valid_buffer_loc top_buffer dloc loc then - (print_highlight_location top_buffer loc, ie) - else - (mt () (* print_command_location top_buffer dloc *), ie) - in - match exc with - | End_of_input -> - msgerrnl (mt ()); pp_flush(); exit 0 - | Errors.Drop -> (* Last chance *) - if Mltop.is_ocaml_top() then raise Errors.Drop; - (str"Error: There is no ML toplevel." ++ fnl ()) - | Errors.Quit -> - raise Errors.Quit - | _ -> - (if is_pervasive_exn exc then (mt ()) else locstrm) ++ - Errors.print exc +let print_toplevel_error = function + | Error_in_file (s, (inlibrary, fname, loc), e) -> + print_location_in_file s inlibrary fname loc ++ Errors.print e + | e -> + if is_pervasive_exn e then Errors.print e + else match Loc.get_loc e with + | Some loc when valid_buffer_loc top_buffer loc -> + print_highlight_location top_buffer loc ++ Errors.print e + | _ -> Errors.print e (* Read the input stream until a dot is encountered *) let parse_to_dot = @@ -310,45 +280,40 @@ let parse_to_dot = in Gram.Entry.of_parser "Coqtoplevel.dot" dot -(* We assume that when a lexer error occurs, at least one char was eaten *) +(* If an error occured while parsing, we try to read the input until a dot + token is encountered. + We assume that when a lexer error occurs, at least one char was eaten *) + let rec discard_to_dot () = try Gram.entry_parse parse_to_dot top_buffer.tokens - with (Compat.Token.Error _|Lexer.Error.E _) -> - discard_to_dot() - - -(* If the error occured while parsing, we read the input until a dot token - * in encountered. *) + with + | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot () + | End_of_input -> raise End_of_input + | e when Errors.noncritical e -> () -let process_error = function - | DuringCommandInterp _ as e -> e - | e -> - if is_pervasive_exn e then - e - else - try - discard_to_dot (); e - with - | End_of_input -> End_of_input - | any -> if is_pervasive_exn any then any else e +let read_sentence () = + try Vernac.parse_sentence (top_buffer.tokens, None) + with reraise -> discard_to_dot (); raise reraise (* do_vernac reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists. Otherwise, exit. End_of_input: Ctrl-D was typed in, we will quit *) + let do_vernac () = msgerrnl (mt ()); if !print_emacs then msgerr (str (top_buffer.prompt())); resynch_buffer top_buffer; - begin - try - ignore (raw_do_vernac top_buffer.tokens) - with any -> - ppnl (print_toplevel_error (process_error any)) - end; - flush_all() + try ignore (Vernac.eval_expr (read_sentence ())) + with + | End_of_input | Errors.Quit -> + msgerrnl (mt ()); pp_flush(); raise Errors.Quit + | Errors.Drop -> (* Last chance *) + if Mltop.is_ocaml_top() then raise Errors.Drop + else ppnl (str"Error: There is no ML toplevel." ++ fnl ()) + | any -> ppnl (print_toplevel_error any) (* coq and go read vernacular expressions until Drop is entered. * Ctrl-C will raise the exception Break instead of aborting Coq. @@ -360,11 +325,10 @@ let rec loop () = Sys.catch_break true; try reset_input_buffer stdin top_buffer; - while true do do_vernac() done + while true do do_vernac(); flush_all() done with | Errors.Drop -> () - | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Errors.Quit -> exit 0 | any -> - msgerrnl (str"Anomaly. Please report."); + msgerrnl (str"Anomaly: main loop exited. Please report."); loop () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 733bd52b9..a2563a676 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -20,8 +20,6 @@ open Vernacinterp Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -exception DuringCommandInterp of Loc.t * exn - exception HasNotFailed (* The navigation vernac commands will be handled separately *) @@ -101,20 +99,14 @@ let _ = if the error ocurred during interpretation or not *) let raise_with_file file exc = - let (cmdloc,re) = - match exc with - | DuringCommandInterp(loc,e) -> (loc,e) - | e -> (Loc.ghost,e) - in let (inner,inex) = - match re with + match exc with | Error_in_file (_, (b,f,loc), e) when not (Loc.is_ghost loc) -> ((b, f, loc), e) | e -> match Loc.get_loc e with - | Some loc when not (Loc.is_ghost loc) -> - ((false,file, loc), e) - | _ -> ((false,file,cmdloc), e) + | Some loc when not (Loc.is_ghost loc) -> ((false,file,loc), e) + | _ -> ((false,file,Loc.ghost), e) in raise (Error_in_file (file, inner, disable_drop inex)) @@ -350,11 +342,11 @@ let rec vernac_com interpfun checknav (loc,com) = if !time then display_cmd_header loc com; let com = if !time then VernacTime com else com in interp com - with e -> (* TODO: restrict to Errors.noncritical or not ? - Morally, this is a reraise ... *) - let e = Errors.push e in + with reraise -> + let reraise = Errors.push reraise in Format.set_formatter_out_channel stdout; - raise (DuringCommandInterp (loc, e)) + if Loc.is_ghost loc || Loc.get_loc reraise != None then raise reraise + else Loc.raise loc reraise and read_vernac_file verbosely s = Flags.make_warn verbosely; @@ -415,10 +407,6 @@ let eval_expr ?(preserving=false) loc_ast = Backtrack.mark_command (snd loc_ast); status -(* raw_do_vernac : Pcoq.Gram.parsable -> unit - * vernac_step . parse_sentence *) -let raw_do_vernac po = eval_expr (parse_sentence (po,None)) - (* XML output hooks *) let xml_start_library = ref (fun _ -> ()) let xml_end_library = ref (fun _ -> ()) @@ -434,10 +422,8 @@ let load_vernac verb file = Lib.mark_end_of_command (); (* in case we're still in coqtop init *) let _ = read_vernac_file verb file in if !Flags.beautify_file then close_out !chan_beautify; - with e -> - (* TODO: restrict to Errors.noncritical or not ? - Morally, this is a reraise ... *) - let e = Errors.push e in + with any -> + let e = Errors.push any in if !Flags.beautify_file then close_out !chan_beautify; raise_with_file file e diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 8f1fbc54f..e0ca6db46 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -17,7 +17,6 @@ val parse_sentence : Pcoq.Gram.parsable * in_channel option -> (** Reads and executes vernac commands from a stream. The boolean [just_parsing] disables interpretation of commands. *) -exception DuringCommandInterp of Loc.t * exn exception End_of_input val just_parsing : bool ref @@ -30,7 +29,6 @@ val just_parsing : bool ref (* spiwack: return value: [true] if safe (general case), [false] if unsafe (like [Admitted]). *) val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> bool -val raw_do_vernac : Pcoq.Gram.parsable -> bool (** Set XML hooks *) val set_xml_start_library : (unit -> unit) -> unit |