diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 26 |
1 files changed, 21 insertions, 5 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 2c9f116cc3..9cdfd0dc21 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -110,7 +110,13 @@ let make_coqtop_args fname = | None -> args | Some fname -> if List.exists (String.equal "-top") args then args - else "-topfile"::fname::args + else + (* We basically copy the code of Names.check_valid since it is not exported *) + (* to coqide. This is to prevent a possible failure of parsing "-topfile" *) + (* at initialization of coqtop (see #10286) *) + match Unicode.ident_refutation (Filename.chop_extension (Filename.basename fname)) with + | Some (_,x) -> output_string stderr (x^"\n"); exit 1 + | None -> "-topfile"::fname::args in proj, args @@ -878,10 +884,20 @@ let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) let alpha_items menu_name item_name l = let mk_item text = let text' = - let last = String.length text - 1 in - if text.[last] = '.' - then text ^"\n" - else text ^" " + let len = String.length text in + let buf = Buffer.create (len + 1) in + let escaped = ref false in + String.iter (fun c -> + if !escaped then + let () = Buffer.add_char buf c in + escaped := false + else if c = '_' then escaped := true + else Buffer.add_char buf c + ) text; + if text.[len - 1] = '.' + then Buffer.add_char buf '\n' + else Buffer.add_char buf ' '; + Buffer.contents buf in let callback _ = on_current_term (fun sn -> sn.buffer#insert_interactive text') |