Imported Upstream snapshot 8.3~beta0+13298

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 ()