diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 26 | ||||
| -rw-r--r-- | ide/idetop.ml | 12 |
2 files changed, 27 insertions, 11 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') diff --git a/ide/idetop.ml b/ide/idetop.ml index 7c6fa8951b..7e55eb4d13 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -56,7 +56,7 @@ let coqide_known_option table = List.mem table [ ["Printing";"Unfocused"]; ["Diffs"]] -let is_known_option cmd = match Vernacprop.under_control cmd with +let is_known_option cmd = match cmd with | VernacSetOption (_, o, OptionSetTrue) | VernacSetOption (_, o, OptionSetString _) | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o @@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) = +let ide_cmd_checks ~last_valid { CAst.loc; v } = let user_error s = try CErrors.user_err ?loc ~hdr:"IDE" (str s) with e -> @@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) = let info = Stateid.add info ~valid:last_valid Stateid.dummy in Exninfo.raise ~info e in - if is_debug cmd then + if is_debug v.expr then user_error "Debug mode not available in the IDE" -let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) = +let ide_cmd_warns ~id { CAst.loc; v } = let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in - if is_known_option cmd then + if is_known_option v.expr then warn "Set this option from the IDE menu instead"; - if is_navigation_vernac cmd || is_undo cmd then + if is_navigation_vernac v.expr || is_undo v.expr then warn "Use IDE navigation instead" (** Interpretation (cf. [Ide_intf.interp]) *) |