From 92696abcaab68c70461c285ada87e50dacf3bb34 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Apr 2009 12:58:07 +0000 Subject: - 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 --- toplevel/toplevel.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'toplevel/toplevel.ml') 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 -- cgit v1.2.3