diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 14:02:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 15:20:31 +0100 |
| commit | 6736fb9db77be8a6f207b95ae0d5f7b3a843dc89 (patch) | |
| tree | 3046794d9942ab4b7a9cc0b596c32fea1630abcb | |
| parent | 48509b6112fc857abdfc442c89821363043ac705 (diff) | |
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.
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index ba20c771a..c96a34018 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 59d9078bb..62e1bad43 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, _ = |