diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 140 |
1 files changed, 71 insertions, 69 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9d64f983..ee821a48 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -15,12 +15,11 @@ open Cerrors open Vernac open Vernacexpr open Pcoq -open Protectedtoplevel (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) -type input_buffer = { +type input_buffer = { mutable prompt : unit -> string; mutable str : string; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) @@ -72,7 +71,7 @@ let prompt_char ic ibuf count = ibuf.str.[ibuf.len] <- c; ibuf.len <- ibuf.len + 1; Some c - with End_of_file -> + with End_of_file -> None (* Reinitialize the char stream (after a Drop) *) @@ -94,34 +93,49 @@ let get_bols_of_loc ibuf (bp,ep) = if b < 0 or e < b then anomaly "Bad location"; match lines with | ([],None) -> ([], Some (b,e)) - | (fl,oe) -> ((b,e)::fl, oe) + | (fl,oe) -> ((b,e)::fl, oe) in let rec lines_rec ba after = function | [] -> add_line (0,ba) after | ll::_ when ll <= bp -> add_line (ll,ba) after | ll::fl -> let nafter = if ll < ep then add_line (ll,ba) after else after in - lines_rec ll nafter fl + lines_rec ll nafter fl in let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in (fl,Option.get ll) let dotted_location (b,e) = - if e-b < 3 then + if e-b < 3 then ("", String.make (e-b) ' ') - else + else (String.make (e-b-1) '.', " ") +let blanch_utf8_string s bp ep = + let s' = String.make (ep-bp) ' ' in + let j = ref 0 in + for i = bp to ep - 1 do + let n = Char.code s.[i] in + (* Heuristic: assume utf-8 chars are printed using a single + fixed-size char and therefore contract all utf-8 code into one + space; in any case, preserve tabulation so + that its effective interpretation in terms of spacing is preserved *) + if s.[i] = '\t' then s'.[!j] <- '\t'; + if n < 0x80 || 0xC0 <= n then incr j + done; + String.sub s' 0 !j + let print_highlight_location ib loc = let (bp,ep) = unloc loc in - let bp = bp - ib.start + let bp = bp - ib.start and ep = ep - ib.start in let highlight_lines = match get_bols_of_loc ib (bp,ep) with - | ([],(bl,el)) -> + | ([],(bl,el)) -> + let shift = blanch_utf8_string ib.str bl bp in + let span = String.length (blanch_utf8_string ib.str bp ep) in (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++ - str"> " ++ str(String.make (bp-bl) ' ') ++ - str(String.make (ep-bp) '^')) + str"> " ++ str(shift) ++ str(String.make span '^')) | ((b1,e1)::ml,(bn,en)) -> let (d1,s1) = dotted_location (b1,bp) in let (dn,sn) = dotted_location (ep,en) in @@ -131,9 +145,9 @@ let print_highlight_location ib loc = prlist (fun (bi,ei) -> (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++ - str sn ++ str dn) in + str sn ++ str dn) in (l1 ++ li ++ ln) - in + in let loc = make_loc (bp,ep) in (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ highlight_lines ++ fnl ()) @@ -171,7 +185,7 @@ let print_location_in_file s inlibrary fname loc = with e -> (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) - + let print_command_location ib dloc = match dloc with | Some (bp,ep) -> @@ -185,10 +199,10 @@ let valid_loc dloc loc = | Some dloc -> let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed | _ -> true - + let valid_buffer_loc ib dloc loc = - valid_loc dloc loc & - let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e + valid_loc dloc loc & + let (b,e) = 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" otherwise. We trap all exceptions to prevent the error message printing @@ -196,35 +210,35 @@ let valid_buffer_loc ib dloc loc = let make_prompt () = try (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < " - with _ -> + with _ -> "Coq < " -(*let build_pending_list l = +(*let build_pending_list l = let pl = ref ">" in let l' = ref l in - let res = - while List.length !l' > 1 do + let res = + while List.length !l' > 1 do pl := !pl ^ "|" Names.string_of_id x; l':=List.tl !l' done in let last = try List.hd !l' with _ -> in "<"^l' -*) +*) (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global backtracking) and the current proof state [p] (for proof backtracking) plus the list of open (nested) proofs (for proof aborting when backtracking). It looks like: - + "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = let statnum = string_of_int (Lib.current_command_label ()) in let dpth = Pfedit.current_proof_depth() in let pending = Pfedit.get_all_proof_names() in - let pendingprompt = - List.fold_left + let pendingprompt = + List.fold_left (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in @@ -235,9 +249,9 @@ let make_emacs_prompt() = * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) let top_buffer = - let pr() = - emacs_prompt_startstring() - ^ make_prompt() + let pr() = + emacs_prompt_startstring() + ^ make_prompt() ^ make_emacs_prompt() ^ emacs_prompt_endstring() in @@ -250,7 +264,7 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> + <- (fun () -> emacs_prompt_startstring() ^ prompt () ^ emacs_prompt_endstring()) @@ -262,7 +276,7 @@ let rec is_pervasive_exn = function | Error_in_file (_,_,e) -> is_pervasive_exn e | Stdpp.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e - | DuringSyntaxChecking e -> is_pervasive_exn e + | DuringSyntaxChecking (_,e) -> is_pervasive_exn e | _ -> false (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D @@ -272,33 +286,31 @@ let print_toplevel_error exc = let (dloc,exc) = match exc with | DuringCommandInterp (loc,ie) - | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) -> + | DuringSyntaxChecking (loc,ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) - | _ -> (None, exc) + | _ -> (None, exc) in let (locstrm,exc) = match exc with | Stdpp.Exc_located (loc, ie) -> if valid_buffer_loc top_buffer dloc loc then (print_highlight_location top_buffer loc, ie) - else + else ((mt ()) (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (inlibrary, fname, loc), ie) -> (print_location_in_file s inlibrary fname loc, ie) - | _ -> + | _ -> ((mt ()) (* print_command_location top_buffer dloc *), exc) in match exc with - | End_of_input -> + | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise Vernacexpr.Drop; (str"Error: There is no ML toplevel." ++ fnl ()) - | Vernacexpr.ProtectedLoop -> - raise Vernacexpr.ProtectedLoop - | Vernacexpr.Quit -> + | Vernacexpr.Quit -> raise Vernacexpr.Quit - | _ -> + | _ -> (if is_pervasive_exn exc then (mt ()) else locstrm) ++ Cerrors.explain_exn exc @@ -308,14 +320,14 @@ let parse_to_dot = | ("", ".") -> () | ("EOI", "") -> raise End_of_input | _ -> dot st - in + in Gram.Entry.of_parser "Coqtoplevel.dot" dot - + (* We assume that when a lexer error occurs, at least one char was eaten *) let rec discard_to_dot () = - try + try Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> + with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> discard_to_dot() @@ -323,14 +335,14 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ - | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e + | DuringCommandInterp _ + | DuringSyntaxChecking _ as e -> e | e -> - if is_pervasive_exn e then + if is_pervasive_exn e then e - else - try - discard_to_dot (); e + else + try + discard_to_dot (); e with | End_of_input -> End_of_input | de -> if is_pervasive_exn de then de else e @@ -344,11 +356,11 @@ let do_vernac () = msgerrnl (mt ()); if !print_emacs then msgerr (str (top_buffer.prompt())); resynch_buffer top_buffer; - begin - try + begin + try raw_do_vernac top_buffer.tokens - with e -> - msgnl (print_toplevel_error (process_error e)) + with e -> + msgnl (print_toplevel_error (process_error e)) end; flush_all() @@ -356,30 +368,20 @@ let do_vernac () = * Ctrl-C will raise the exception Break instead of aborting Coq. * Here we catch the exceptions terminating the Coq loop, and decide * if we really must quit. - * The boolean value is used to choose between a protected loop, which - * we think is more suited for communication with other programs, or - * plain communication. *) + *) -let rec coq_switch b = +let rec loop () = Sys.catch_break true; (* ensure we have a command separator object (DOT) so that the first command can be reseted. *) Lib.mark_end_of_command(); try - if b then begin - reset_input_buffer stdin top_buffer; - while true do do_vernac() done - end else - protected_loop stdin + reset_input_buffer stdin top_buffer; + while true do do_vernac() done with | Vernacexpr.Drop -> () - | Vernacexpr.ProtectedLoop -> - Lib.declare_initial_state(); - coq_switch false | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Quit -> exit 0 | e -> msgerrnl (str"Anomaly. Please report."); - coq_switch b - -let loop () = coq_switch true + loop () |