Merge PR #9399: [ide] fail on unavailable commands before adding to the document

Reviewed-by: ejgallego
Ack-by: ppedrot

3 files changed, 22 insertions, 6 deletions

diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml
index 8b0c736f50..4e26cb6095 100644
--- a/ide/fake_ide.ml
+++ b/ide/fake_ide.ml
@@ -241,6 +241,9 @@ let eval_print l coq =
   | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] ->
       let eid, tip = add_sentence ~name phrase in
       after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+  | [ Tok(_,"FAILADD"); Tok(_,phrase) ] ->
+      let eid, tip = add_sentence phrase in
+      after_fail coq (base_eval_call ~fail:false (add ((phrase,eid),(tip,true))) coq)
   | [ Tok(_,"GOALS"); ] ->
       eval_call (goals ()) coq
   | [ Tok(_,"FAILGOALS"); ] ->
@@ -267,7 +270,8 @@ let eval_print l coq =
       prerr_endline "Quitting fake_ide";
       exit 0
   | Tok("#[^\n]*",_) :: _  -> ()
-  | _ -> error "syntax error"
+  | Tok(s,_) :: _ -> error ("syntax error at " ^ s)
+  | _ -> error ("syntax error")
 
 let grammar =
   let open Parser in
@@ -275,6 +279,7 @@ let grammar =
   let eat_phrase = eat_balanced '{' in
   Alt
     [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase]
+    ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase]
     ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
     ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
     ; Seq [Item (eat_rex "WAIT")]
diff --git a/ide/idetop.ml b/ide/idetop.ml
index f91aa569d4..205f4455a3 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -64,11 +64,19 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
 
 (** Check whether a command is forbidden in the IDE *)
 
-let ide_cmd_checks ~id {CAst.loc;v=ast} =
-  let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in
-  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
+let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
+  let user_error s =
+    try CErrors.user_err ?loc ~hdr:"IDE" (str s)
+    with e ->
+      let (e, info) = CErrors.push e in
+      let info = Stateid.add info ~valid:last_valid Stateid.dummy in
+      Exninfo.raise ~info e
+  in
   if is_debug ast then
-    user_error "Debug mode not available in the IDE";
+    user_error "Debug mode not available in the IDE"
+
+let ide_cmd_warns ~id {CAst.loc;v=ast} =
+  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
   if is_known_option ast then
     warn "Set this option from the IDE menu instead";
   if is_navigation_vernac ast || is_undo ast then
@@ -87,10 +95,11 @@ let add ((s,eid),(sid,verbose)) =
   | None -> assert false (* s is not an empty string *)
   | Some (loc, ast) ->
   let loc_ast = CAst.make ~loc ast in
+  ide_cmd_checks ~last_valid:sid loc_ast;
   let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
   set_doc doc;
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  ide_cmd_checks ~id:newid loc_ast;
+  ide_cmd_warns ~id:newid loc_ast;
   (* TODO: the "" parameter is a leftover of the times the protocol
    * used to include stderr/stdout output.
    *
diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake
new file mode 100644
index 0000000000..aa68fad39e
--- /dev/null
+++ b/test-suite/ide/debug_ltac.fake
@@ -0,0 +1,2 @@
+FAILADD { Debug On. }
+ADD { Set Debug On. }