diff options
| author | Hugo Herbelin | 2019-07-23 21:25:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-07-23 21:47:56 +0200 |
| commit | 64906d402e9757af850b9562aaae69099abf871f (patch) | |
| tree | 54158ac1b3e8700c51caaa1a0c34cdf78dfd1f66 | |
| parent | d57f262bb39ebbcae630f1439377c51aaa41452b (diff) | |
Fixing #10286 (coqide hangs on invalid filenames).
The hang is caused by a failure in the interpretation by coqtop of the
command line option "-topfile filename" (this happens before a proper
XML communication is set up between coqtop and coqide).
The fix is a bit ad hoc. We copy in coqide the code for checking the
validity of a filename. We copy it to avoid adding a dependency in
either Names.check_valid or Stm.dirpath_of_file. We do a minimal check
(on the basename) while (if it hadn't added extra depencencies or code
duplication) it would have been more consistent to do the exact same
check as in Stm.dirpath_of_file.
| -rw-r--r-- | ide/coqide.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 8d95dcee27..a22c51d36d 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 |