From 6736fb9db77be8a6f207b95ae0d5f7b3a843dc89 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 7 Dec 2014 14:02:59 +0100
Subject: Ensuring that ide_slave and stm receive only .v files from CoqIDE. In
 particular, renouncing to original support for existing non .v files in
 CoqIDE (hoping it is ok for anyone). Please amend if better to propose.

---
 ide/coqide.ml    | 5 +----
 ide/ide_slave.ml | 2 ++
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index ba20c771a6..c96a34018a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1328,10 +1328,7 @@ let build_ui () =
 (** {2 Coqide main function } *)
 
 let make_file_buffer f =
-  let f =
-    if Sys.file_exists f || Filename.check_suffix f ".v" then f
-    else f^".v"
-  in
+  let f = if Filename.check_suffix f ".v" then f else f^".v" in
   FileAux.load_file ~maycreate:true f
 
 let make_scratch_buffer () =
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 59d9078bb8..62e1bad431 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -345,6 +345,8 @@ let init =
      match file with
      | None -> Stm.get_current_state ()
      | Some file ->
+         if not (Filename.check_suffix file ".v") then
+           error "A file with suffix .v is expected.";
          let dir = Filename.dirname file in
          let open Loadpath in let open CUnix in
          let initial_id, _ =
-- 
cgit v1.2.3