diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 15 |
2 files changed, 17 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 50c78d0ed..70087ecbf 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1132,9 +1132,9 @@ let look_for_mutual_statements thms = let n = List.length thms in let inds = List.map (fun (id,(t,_) as x) -> let (hyps,ccl) = decompose_prod_assum t in - let whnf_hyp_hds = map_rel_context_with_binders - (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) - hyps in + let whnf_hyp_hds = fold_map_rel_context + (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) + (Global.env()) hyps in let ind_hyps = List.flatten (list_map_i (fun i (_,b,t) -> match kind_of_term t with 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 |