diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 31 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 58 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 107 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 35 |
5 files changed, 133 insertions, 100 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index de0d912c03..522b9900a5 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -36,7 +36,7 @@ COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SY def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN", ""), "coqdoc") - fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") + fd, filename = mkstemp(prefix="coqdoc_", suffix=".v") if platform.system().startswith("CYGWIN"): # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip() diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index df11960403..e59f694aa7 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -27,13 +27,13 @@ from docutils.parsers.rst.roles import code_role #, set_classes from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes -from sphinx.roles import XRefRole -from sphinx.errors import ExtensionError -from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode -from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index -from sphinx.domains.std import token_xrefs +from sphinx.errors import ExtensionError +from sphinx.roles import XRefRole +from sphinx.util.docutils import ReferenceRole +from sphinx.util.logging import getLogger, get_node_location +from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from . import coqdoc from .repl import ansicolors @@ -1162,25 +1162,34 @@ GrammarProductionRole.role_name = "production" def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): """Marks the definition of a glossary term inline in the text. Matching :term:`XXX` - constructs will link to it. The term will also appear in the Glossary Index. + constructs will link to it. Use the form :gdef:`text <term>` to display "text" + for the definition of "term", such as when "term" must be capitalized or plural + for grammatical reasons. The term will also appear in the Glossary Index. - Example:: + Examples:: A :gdef:`prime` number is divisible only by itself and 1. + :gdef:`Composite <composite>` numbers are the non-prime numbers. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env std = env.domaindata['std']['objects'] - key = ('term', text) + m = ReferenceRole.explicit_title_re.match(text) + if m: + (text, term) = m.groups() + text = text.strip() + else: + term = text + key = ('term', term) if key in std: MSG = 'Duplicate object: {}; other is at {}' - msg = MSG.format(text, env.doc2path(std[key][0])) + msg = MSG.format(term, env.doc2path(std[key][0])) inliner.document.reporter.warning(msg, line=lineno) - targetid = nodes.make_id('term-{}'.format(text)) + targetid = nodes.make_id('term-{}'.format(term)) std[key] = (env.docname, targetid) - target = nodes.target('', '', ids=[targetid], names=[text]) + target = nodes.target('', '', ids=[targetid], names=[term]) inliner.document.note_explicit_target(target) node = nodes.inline(rawtext, '', target, nodes.Text(text), classes=['term-defn']) set_role_source_info(inliner, lineno, node) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 62cc8ea86b..a9a243868f 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -59,6 +59,8 @@ DELETE: [ | lookup_at_as_comma | test_only_starredidentrefs | test_bracket_ident +| test_hash_ident +| test_id_colon | test_lpar_id_colon | test_lpar_id_coloneq (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *) | test_lpar_id_rpar @@ -1231,8 +1233,8 @@ query_command: [ | WITH "SearchPattern" constr_pattern in_or_out_modules | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." | WITH "SearchRewrite" constr_pattern in_or_out_modules -| REPLACE "Search" searchabout_query searchabout_queries "." -| WITH "Search" searchabout_queries +| REPLACE "Search" search_query search_queries "." +| WITH "Search" search_queries ] vernac_toplevel: [ @@ -1457,17 +1459,10 @@ ne_in_or_out_modules: [ | DELETE "outside" LIST1 global ] -searchabout_query: [ -| REPLACE positive_search_mark ne_string OPT scope_delimiter -| WITH ne_string OPT scope_delimiter -| REPLACE positive_search_mark constr_pattern -| WITH constr_pattern -] - -searchabout_queries: [ +search_queries: [ | DELETE ne_in_or_out_modules -| REPLACE searchabout_query searchabout_queries -| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules +| REPLACE search_query search_queries +| WITH LIST1 ( search_query ) OPT ne_in_or_out_modules | DELETE (* empty *) ] @@ -1475,6 +1470,27 @@ positive_search_mark: [ | OPTINREF ] +SPLICE: [ +| positive_search_mark +] + +search_query: [ +| REPLACE OPT "-" search_item +| WITH search_item +| "-" search_query +| REPLACE OPT "-" "[" LIST1 ( LIST1 search_query ) SEP "|" "]" +| WITH "[" LIST1 ( LIST1 search_query ) SEP "|" "]" +] + +search_item: [ +| REPLACE search_where ":" ne_string OPT scope_delimiter +| WITH OPT ( search_where ":" ) ne_string OPT scope_delimiter +| DELETE ne_string OPT scope_delimiter +| REPLACE search_where ":" constr_pattern +| WITH OPT ( search_where ":" ) constr_pattern +| DELETE constr_pattern +] + by_notation: [ | REPLACE ne_string OPT [ "%" IDENT ] | WITH ne_string OPT [ "%" scope_key ] @@ -1485,14 +1501,6 @@ scope_delimiter: [ | WITH "%" scope_key ] -(* Don't show these details *) -DELETE: [ -| register_token -| register_prim_token -| register_type_token -] - - decl_notation: [ | REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ] | WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ] @@ -1638,7 +1646,6 @@ SPLICE: [ | record_binder | at_level_opt | table_value -| positive_search_mark | in_or_out_modules | option_setting | orient @@ -1672,11 +1679,14 @@ SPLICE: [ | intropatterns | instance_name | ne_in_or_out_modules -| searchabout_queries +| search_queries | locatable | scope_delimiter | bignat | one_import_filter_name +| register_token +| search_where +| extended_def_token ] (* end SPLICE *) RENAME: [ @@ -1725,7 +1735,9 @@ RENAME: [ | record_binder_body field_body | class_rawexpr class | smart_global smart_qualid +(* | searchabout_query search_item +*) | option_table setting_name | argument_spec_block arg_specs | more_implicits_block implicits_alt @@ -1735,8 +1747,6 @@ RENAME: [ | numnotoption numeral_modifier ] -(* todo: positive_search_mark is a lousy name for OPT "-" *) - (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *) clause_dft_concl: [ | OPTINREF diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 92e9df51d5..1b0a5c28ee 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -798,58 +798,7 @@ gallina: [ ] register_token: [ -| register_prim_token -| register_type_token -] - -register_type_token: [ -| "#int63_type" -| "#float64_type" -] - -register_prim_token: [ -| "#int63_head0" -| "#int63_tail0" -| "#int63_add" -| "#int63_sub" -| "#int63_mul" -| "#int63_div" -| "#int63_mod" -| "#int63_lsr" -| "#int63_lsl" -| "#int63_land" -| "#int63_lor" -| "#int63_lxor" -| "#int63_addc" -| "#int63_subc" -| "#int63_addcarryc" -| "#int63_subcarryc" -| "#int63_mulc" -| "#int63_diveucl" -| "#int63_div21" -| "#int63_addmuldiv" -| "#int63_eq" -| "#int63_lt" -| "#int63_le" -| "#int63_compare" -| "#float64_opp" -| "#float64_abs" -| "#float64_eq" -| "#float64_lt" -| "#float64_le" -| "#float64_compare" -| "#float64_classify" -| "#float64_add" -| "#float64_sub" -| "#float64_mul" -| "#float64_div" -| "#float64_sqrt" -| "#float64_of_int63" -| "#float64_normfr_mantissa" -| "#float64_frshiftexp" -| "#float64_ldshiftexp" -| "#float64_next_up" -| "#float64_next_down" +| test_hash_ident "#" IDENT ] thm_token: [ @@ -1252,7 +1201,7 @@ query_command: [ | "SearchHead" constr_pattern in_or_out_modules "." | "SearchPattern" constr_pattern in_or_out_modules "." | "SearchRewrite" constr_pattern in_or_out_modules "." -| "Search" searchabout_query searchabout_queries "." +| "Search" search_query search_queries "." ] printable: [ @@ -1349,14 +1298,48 @@ positive_search_mark: [ | ] -searchabout_query: [ -| positive_search_mark ne_string OPT scope_delimiter -| positive_search_mark constr_pattern +search_query: [ +| positive_search_mark search_item +| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]" ] -searchabout_queries: [ +search_item: [ +| test_id_colon search_where ":" ne_string OPT scope_delimiter +| "is" ":" logical_kind +| ne_string OPT scope_delimiter +| test_id_colon search_where ":" constr_pattern +| constr_pattern +] + +logical_kind: [ +| thm_token +| assumption_token +| "Context" +| extended_def_token +| "Primitive" +] + +extended_def_token: [ +| def_token +| "Coercion" +| "Instance" +| "Scheme" +| "Canonical" +| "Field" +| "Method" +] + +search_where: [ +| "head" +| "hyp" +| "concl" +| "headhyp" +| "headconcl" +] + +search_queries: [ | ne_in_or_out_modules -| searchabout_query searchabout_queries +| search_query search_queries | ] @@ -1910,9 +1893,13 @@ debug: [ | ] +eauto_search_strategy_name: [ +| "bfs" +| "dfs" +] + eauto_search_strategy: [ -| "(bfs)" -| "(dfs)" +| "(" eauto_search_strategy_name ")" | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 11f06b7b8a..3a327fc748 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -823,7 +823,7 @@ command: [ | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid -| "Typeclasses" "eauto" ":=" OPT "debug" OPT [ "(bfs)" | "(dfs)" ] OPT int +| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ] | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ] | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr @@ -940,7 +940,7 @@ command: [ | "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Time" sentence | "Redirect" string sentence | "Timeout" num sentence @@ -996,9 +996,31 @@ comment: [ | num ] +search_query: [ +| search_item +| "-" search_query +| "[" LIST1 ( LIST1 search_query ) SEP "|" "]" +] + search_item: [ -| one_term -| string OPT ( "%" scope_key ) +| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key ) +| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term +| "is" ":" logical_kind +] + +logical_kind: [ +| thm_token +| assumption_token +| "Context" +| "Definition" +| "Example" +| "Coercion" +| "Instance" +| "Scheme" +| "Canonical" +| "Field" +| "Method" +| "Primitive" ] univ_name_list: [ @@ -1085,6 +1107,11 @@ hints_path: [ | hints_path hints_path ] +eauto_search_strategy_name: [ +| "bfs" +| "dfs" +] + class: [ | "Funclass" | "Sortclass" |