From 8c42932d1788c8924844d8fa22419f6fb4401030 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 22 Mar 2017 14:50:23 -0400
Subject: make check not CoqIDE-specific

---
 ide/ide_slave.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 2ec79dc585..8cadf1a263 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -79,23 +79,23 @@ let is_undo cmd = match cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
 
-(** Check whether a command is forbidden by CoqIDE *)
+(** Check whether a command is forbidden in the IDE *)
 
-let coqide_cmd_checks (loc,ast) =
+let ide_cmd_checks (loc,ast) =
   let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
   if is_debug ast then
-    user_error "Debug mode not available within CoqIDE";
+    user_error "Debug mode not available in the IDE";
   if is_known_option ast then
-    Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead");
+    Feedback.msg_warning (strbrk "Set this option from the IDE menu instead");
   if Vernac.is_navigation_vernac ast || is_undo ast then
-    Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead");
+    Feedback.msg_warning (strbrk "Use IDE navigation instead");
   if is_query ast then
     Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
 let add ((s,eid),(sid,verbose)) =
-  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in
+  let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
   (* TODO: the "" parameter is a leftover of the times the protocol
    * used to include stderr/stdout output.
-- 
cgit v1.2.3