[vernac] Refactor Vernacular Control Attributes into a list

We place control attributes on their own, datatype, similarly to
regular attributes.

This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.

1 files changed, 6 insertions, 6 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7c6fa8951b..7e55eb4d13 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -56,7 +56,7 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Unfocused"];
   ["Diffs"]]
 
-let is_known_option cmd = match Vernacprop.under_control cmd with
+let is_known_option cmd = match cmd with
   | VernacSetOption (_, o, OptionSetTrue)
   | VernacSetOption (_, o, OptionSetString _)
   | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
@@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
 
 (** Check whether a command is forbidden in the IDE *)
 
-let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
+let ide_cmd_checks ~last_valid { CAst.loc; v } =
   let user_error s =
     try CErrors.user_err ?loc ~hdr:"IDE" (str s)
     with e ->
@@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
       let info = Stateid.add info ~valid:last_valid Stateid.dummy in
       Exninfo.raise ~info e
   in
-  if is_debug cmd then
+  if is_debug v.expr then
     user_error "Debug mode not available in the IDE"
 
-let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) =
+let ide_cmd_warns ~id { CAst.loc; v } =
   let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
-  if is_known_option cmd then
+  if is_known_option v.expr then
     warn "Set this option from the IDE menu instead";
-  if is_navigation_vernac cmd || is_undo cmd then
+  if is_navigation_vernac v.expr || is_undo v.expr then
     warn "Use IDE navigation instead"
 
 (** Interpretation (cf. [Ide_intf.interp]) *)