Merge pull request #667 from LPCIC/name-commands

Display elpi commands/tactics in the outline
LPCIC · Jul 19, 2024 · 24869e9 · 24869e9
2 parents 5827121 + 4023435
commit 24869e9
Showing 1 changed file with 36 additions and 30 deletions.
diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg
@@ -106,7 +106,42 @@ END
 
 (* Syntax **************************************************************** *)
 
-VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF
+{
+let classify_named_vernac (_,p) = Vernacextend.VtSideff([Names.Id.of_string_soft @@ String.concat "." p],VtNow)
+}
+
+VERNAC COMMAND EXTEND ElpiNamed
+| #[ atts = any_attribute ] [ "Elpi" "Program" qualified_name(p) elpi_string(s) ] => { classify_named_vernac p } SYNTERP AS atts 
+   { 
+     let atts = validate_attributes raw_args_attributes atts in
+     EV.Synterp.create_program ~atts ~init:s p;
+     atts
+   } -> {
+     EV.Interp.create_program ~atts ~init:s p
+   }
+| #[ atts = any_attribute ] [ "Elpi" "Command" qualified_name(p) ] => { classify_named_vernac p }  SYNTERP AS atts
+   { 
+     let atts = validate_attributes raw_args_attributes atts in
+     EV.Synterp.create_command ~atts p;
+     atts
+   } -> {
+     EV.Interp.create_command ~atts p }
+| #[ atts = any_attribute ] [ "Elpi" "Tactic" qualified_name(p) ] => { classify_named_vernac p }  SYNTERP AS _ 
+   { 
+     let () = ignore_unknown_attributes atts in
+     EV.Synterp.create_tactic p
+   } -> {
+     EV.Interp.create_tactic p }
+| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] => { classify_named_vernac d }  SYNTERP AS atts
+   { 
+     let atts = validate_attributes synterp_attribute atts in
+     EV.Synterp.create_db ~atts d ~init:s;
+     atts
+   } -> {
+     EV.Interp.create_db ~atts d ~init:s }
+END
+
+VERNAC COMMAND EXTEND ElpiUnnamed CLASSIFIED AS SIDEFF
 | #[ atts = any_attribute ] [ "Elpi" "Accumulate" "File" ne_ident_list(ids) ] SYNTERP AS atts {
      let atts = validate_attributes skip_and_synterp_attributes atts in
      EV.Synterp.accumulate_extra_deps ~atts  ids;
@@ -262,35 +297,6 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF
    } -> {
      EV.Interp.print  ~atts (snd p) s }
 
-| #[ atts = any_attribute ] [ "Elpi" "Program" qualified_name(p) elpi_string(s) ] SYNTERP AS atts 
-   { 
-     let atts = validate_attributes raw_args_attributes atts in
-     EV.Synterp.create_program ~atts ~init:s p;
-     atts
-   } -> {
-     EV.Interp.create_program ~atts ~init:s p
-   }
-| #[ atts = any_attribute ] [ "Elpi" "Command" qualified_name(p) ] SYNTERP AS atts
-   { 
-     let atts = validate_attributes raw_args_attributes atts in
-     EV.Synterp.create_command ~atts p;
-     atts
-   } -> {
-     EV.Interp.create_command ~atts p }
-| #[ atts = any_attribute ] [ "Elpi" "Tactic" qualified_name(p) ] SYNTERP AS _ 
-   { 
-     let () = ignore_unknown_attributes atts in
-     EV.Synterp.create_tactic p
-   } -> {
-     EV.Interp.create_tactic p }
-| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] SYNTERP AS atts
-   { 
-     let atts = validate_attributes synterp_attribute atts in
-     EV.Synterp.create_db ~atts d ~init:s;
-     atts
-   } -> {
-     EV.Interp.create_db ~atts d ~init:s }
-
 | #[ atts = any_attribute ] [ "Elpi" "Typecheck" ] SYNTERP AS _ 
    { 
      let () = ignore_unknown_attributes atts in