diff options
| author | Maxime Dénès | 2017-03-23 21:36:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-23 21:36:49 +0100 |
| commit | 67f7e1103ffb5dae052595e4db00e0214e54474d (patch) | |
| tree | 589f413f7cfcc3f627201bd0fcb8ba553c10d20e | |
| parent | 62ce0d1ec197d70a81faf12e151a3da618b2d1ba (diff) | |
| parent | 8c42932d1788c8924844d8fa22419f6fb4401030 (diff) | |
Merge PR#503: make check not CoqIDE-specific
| -rw-r--r-- | ide/ide_slave.ml | 12 |
1 files 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. |