From 64906d402e9757af850b9562aaae69099abf871f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 23 Jul 2019 21:25:12 +0200
Subject: 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.
---
 ide/coqide.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3