From 5b194f6c4f16b99fe8ebe3c8004c31c01aec0b3b Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 27 Sep 2020 00:49:28 -0700 Subject: Remove prefixes on nonterminal names, e.g. "constr:" and "Prim." --- .../07-commands-and-options/13096-drop-grammar-prefixes.rst | 6 ++++++ doc/sphinx/user-extensions/syntax-extensions.rst | 10 +++------- doc/tools/docgram/fullGrammar | 1 - doc/tools/docgram/orderedGrammar | 1 - 4 files changed, 9 insertions(+), 9 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst (limited to 'doc') diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst new file mode 100644 index 0000000000..0ab9a58e6f --- /dev/null +++ b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst @@ -0,0 +1,6 @@ +- **Changed:** + Drop prefixes from grammar non-terminal names, + e.g. "constr:global" -> "global", "Prim.name" -> "name". + Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. + (`#13096 `_, + by Jim Fehrle). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6ba53b581b..5148fa84c9 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -429,10 +429,6 @@ Displaying information about notations productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` and `tactic_then_gen` which are not shown and can't be printed. - The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify - what part of the grammar a nonterminal is from. If you examine nonterminal definitions - in the source code, they are identified only by the name following the colon. - Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the source code, edits it and inserts it into the documentation files. While the @@ -467,11 +463,11 @@ Displaying information about notations `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, which applies to the productions within it, such as the `try` construct:: - Entry tactic:tactic_expr is + Entry tactic_expr is [ "5" RIGHTA - [ tactic:binder_tactic ] + [ binder_tactic ] | "4" LEFTA - [ SELF; ";"; tactic:binder_tactic + [ SELF; ";"; binder_tactic | SELF; ";"; SELF | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 2ee8e4347e..328175e65c 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1761,7 +1761,6 @@ int_or_id: [ ] language: [ -| "Ocaml" (* extraction plugin *) | "OCaml" (* extraction plugin *) | "Haskell" (* extraction plugin *) | "Scheme" (* extraction plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index aae96fc966..6ae99880b3 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1268,7 +1268,6 @@ int_or_id: [ ] language: [ -| "Ocaml" (* extraction plugin *) | "OCaml" (* extraction plugin *) | "Haskell" (* extraction plugin *) | "Scheme" (* extraction plugin *) -- cgit v1.2.3