- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing

  Not_found bug in Theorem with) from V8.2 to trunk.
- Improving indentation in presence of tabulation and utf-8 when
  reporting error messages with "^^^^^^".
- Updating a few svn:ignore properties.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 1 deletions

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7f869c166..a043c404b 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -112,6 +112,19 @@ let dotted_location (b,e) =
   else 
     (String.make (e-b-1) '.', " ")
 
+let blanching_string s i n =
+  let s = String.sub s i n in
+  for i = 0 to String.length s - 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 and trailing null chars; in any case, preserve tabulation so
+    that its effective interpretation in terms of spacing is preserved *)
+    if 0xC0 > n && n >= 0x80 then s.[i] <- '\000'
+    else if s.[i] <> '\t' then s.[i] <- ' '
+  done; s
+
+
 let print_highlight_location ib loc =
   let (bp,ep) = unloc loc in
   let bp = bp - ib.start 
@@ -120,7 +133,7 @@ let print_highlight_location ib loc =
     match get_bols_of_loc ib (bp,ep) with
       | ([],(bl,el)) ->  
 	  (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++
-             str"> " ++ str(String.make (bp-bl) ' ') ++
+             str"> " ++ str(blanching_string ib.str bl (bp-bl)) ++
              str(String.make (ep-bp) '^'))
       | ((b1,e1)::ml,(bn,en)) ->
           let (d1,s1) = dotted_location (b1,bp) in