aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/coqdoc/main.py17
-rw-r--r--doc/tools/coqrst/coqdomain.py29
-rw-r--r--doc/tools/coqrst/repl/ansicolors.py5
-rw-r--r--doc/tools/docgram/common.edit_mlg7
-rw-r--r--doc/tools/docgram/dune1
-rw-r--r--doc/tools/docgram/fullGrammar30
-rw-r--r--doc/tools/docgram/orderedGrammar6
7 files changed, 55 insertions, 40 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index 522b9900a5..51e26a9082 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -28,7 +28,7 @@ from bs4 import BeautifulSoup
from bs4.element import NavigableString
COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals',
- '-s', '--html', '--stdout', '--utf8']
+ '-s', '--html', '--stdout', '--utf8', '--parse-comments']
COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"]
COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS)
@@ -68,8 +68,19 @@ def lex(source):
if isinstance(elem, NavigableString):
yield [], elem
elif elem.name == "span":
- cls = "coqdoc-{}".format(elem['title'])
- yield [cls], elem.string
+ if elem.string:
+ cls = "coqdoc-{}".format(elem.get("title", "comment"))
+ yield [cls], elem.string
+ else:
+ # handle multi-line comments
+ children = list(elem.children)
+ mlc = children[0].startswith("(*") and children[-1].endswith ("*)")
+ for elem2 in children:
+ if isinstance(elem2, NavigableString):
+ cls = ["coqdoc-comment"] if mlc else []
+ yield cls, elem2
+ elif elem2.name == 'br':
+ pass
elif elem.name == 'br':
pass
else:
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 1428dae7ef..468b6b648d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -938,10 +938,11 @@ class CoqtopBlocksTransform(Transform):
@staticmethod
def split_lines(source):
- r"""Split Coq input in chunks
+ r"""Split Coq input into chunks, which may include single- or
+ multi-line comments. Nested comments are not supported.
A chunk is a minimal sequence of consecutive lines of the input that
- ends with a '.'
+ ends with a '.' or '*)'
>>> split_lines('A.\nB.''')
['A.', 'B.']
@@ -962,8 +963,14 @@ class CoqtopBlocksTransform(Transform):
>>> split_lines('SearchHead le.\nSearchHead (@eq bool).')
['SearchHead le.', 'SearchHead (@eq bool).']
+
+ >>> split_lines("(* *) x. (* *)\ny.\n")
+ ['(* *) x. (* *)', 'y.']
+
+ >>> split_lines("(* *) x (* \n *)\ny.\n")
+ ['(* *) x (* \n *)', 'y.']
"""
- return re.split(r"(?<=(?<!\.)\.)\n", source.strip())
+ return re.split(r"(?:(?<=(?<!\.)\.)|(?<=\*\)))\n", source.strip())
@staticmethod
def parse_options(node):
@@ -1039,7 +1046,11 @@ class CoqtopBlocksTransform(Transform):
if options['warn']:
repl.sendone('Set Warnings "default".')
for sentence in self.split_lines(node.rawsource):
- pairs.append((sentence, repl.sendone(sentence)))
+ comment = re.compile(r"\s*\(\*.*?\*\)\s*", re.DOTALL)
+ wo_comments = re.sub(comment, "", sentence)
+ has_tac = wo_comments != "" and not wo_comments.isspace()
+ output = repl.sendone(sentence) if has_tac else ""
+ pairs.append((sentence, output))
if options['abort']:
repl.sendone('Abort All.')
if options['fail']:
@@ -1052,9 +1063,10 @@ class CoqtopBlocksTransform(Transform):
# Use Coqdoc to highlight input
in_chunks = highlight_using_coqdoc(sentence)
dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input']))
- # Parse ANSI sequences to highlight output
- out_chunks = AnsiColorsParser().colorize_str(output)
- dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
+ if output:
+ # Parse ANSI sequences to highlight output
+ out_chunks = AnsiColorsParser().colorize_str(output)
+ dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output))
node.clear()
node.rawsource = self.make_rawsource(pairs, options['input'], options['output'])
node['classes'].extend(self.block_classes(options['input'] or options['output']))
@@ -1180,8 +1192,7 @@ class StdGlossaryIndex(Index):
if type == 'term':
entries = content[itemname[0].lower()]
entries.append([itemname, 0, docname, anchor, '', '', ''])
- content = sorted(content.items())
- return content, False
+ return content.items(), False
def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
"""A grammar production not included in a ``prodn`` directive.
diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py
index 9e23be2409..6700c20b1a 100644
--- a/doc/tools/coqrst/repl/ansicolors.py
+++ b/doc/tools/coqrst/repl/ansicolors.py
@@ -91,7 +91,10 @@ def parse_ansi(code):
leading ‘^[[’ or the final ‘m’
"""
classes = []
- parse_style([int(c) for c in code.split(';')], 0, classes)
+ if code == "37":
+ pass # ignore white fg
+ else:
+ parse_style([int(c) for c in code.split(';')], 0, classes)
return ["ansi-" + cls for cls in classes]
if __name__ == '__main__':
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fd1c3c0260..48d399dfd3 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -365,7 +365,6 @@ term100: [
| REPLACE term99 ":" term200
| WITH term99 ":" type
| MOVETO term_cast term99 ":" type
-| MOVETO term_cast term99 ":>"
]
constr: [
@@ -1410,8 +1409,9 @@ syntax_modifier: [
| DELETE "in" "custom" IDENT
| REPLACE "in" "custom" IDENT; "at" "level" natural
| WITH "in" "custom" IDENT OPT ( "at" "level" natural )
-| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level
-| WITH LIST1 IDENT SEP "," "at" level
+| DELETE IDENT; "in" "scope" IDENT
+| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
+| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
]
explicit_subentry: [
@@ -2643,7 +2643,6 @@ SPLICE: [
| quoted_attributes (* todo: splice or not? *)
| printable
| hint
-| only_parsing
| record_fields
| constructor_type
| record_binder
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 4ba60ddd9f..873b2f8dff 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -21,7 +21,6 @@
(glob_files %{project_root}/plugins/ltac/*.mlg)
(glob_files %{project_root}/plugins/micromega/*.mlg)
(glob_files %{project_root}/plugins/nsatz/*.mlg)
- (glob_files %{project_root}/plugins/omega/*.mlg)
(glob_files %{project_root}/plugins/ring/*.mlg)
(glob_files %{project_root}/plugins/rtauto/*.mlg)
(glob_files %{project_root}/plugins/ssr/*.mlg)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ab1a9d4c75..b5a234a86a 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1,6 +1,15 @@
(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)
DOC_GRAMMAR
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
+]
+
Constr.ident: [
| Prim.ident
]
@@ -75,7 +84,6 @@ term100: [
| term99 "<:" term200
| term99 "<<:" term200
| term99 ":" term200
-| term99 ":>"
| term99
]
@@ -478,15 +486,6 @@ strategy_level: [
| "transparent"
]
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
-]
-
opt_hintbases: [
|
| ":" LIST1 IDENT
@@ -1401,18 +1400,13 @@ syntax: [
| "Undelimit" "Scope" IDENT
| "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
| "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
-| "Notation" identref LIST0 ident ":=" constr only_parsing
+| "Notation" identref LIST0 ident ":=" constr syntax_modifiers
| "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
| "Format" "Notation" STRING STRING STRING
| "Reserved" "Infix" ne_lstring syntax_modifiers
| "Reserved" "Notation" ne_lstring syntax_modifiers
]
-only_parsing: [
-| "(" "only" "parsing" ")"
-|
-]
-
level: [
| "level" natural
| "next" "level"
@@ -1428,8 +1422,9 @@ syntax_modifier: [
| "only" "printing"
| "only" "parsing"
| "format" STRING OPT STRING
-| IDENT; "," LIST1 IDENT SEP "," "at" level
+| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
| IDENT; "at" level OPT binder_interp
+| IDENT; "in" "scope" IDENT
| IDENT binder_interp
| IDENT explicit_subentry
]
@@ -1778,7 +1773,6 @@ simple_tactic: [
| "zify_iter_let" tactic (* micromega plugin *)
| "zify_elim_let" (* micromega plugin *)
| "nsatz_compute" constr (* nsatz plugin *)
-| "omega" (* omega plugin *)
| "protect_fv" string "in" ident (* ring plugin *)
| "protect_fv" string (* ring plugin *)
| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 5b19b7fc55..cd96693bf0 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -553,7 +553,6 @@ term_cast: [
| term10 ":" type
| term10 "<:" type
| term10 "<<:" type
-| term10 ":>"
]
term_match: [
@@ -1096,7 +1095,7 @@ command: [
| "Undelimit" "Scope" scope_name
| "Bind" "Scope" scope_name "with" LIST1 class
| "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
-| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
+| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
| "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
| "Format" "Notation" string string string
| "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
@@ -1540,7 +1539,7 @@ class: [
syntax_modifier: [
| "at" "level" natural
| "in" "custom" ident OPT ( "at" "level" natural )
-| LIST1 ident SEP "," "at" level
+| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ]
| ident "at" level OPT binder_interp
| ident explicit_subentry
| ident binder_interp
@@ -1856,7 +1855,6 @@ simple_tactic: [
| "zify_iter_let" ltac_expr (* micromega plugin *)
| "zify_elim_let" (* micromega plugin *)
| "nsatz_compute" one_term (* nsatz plugin *)
-| "omega" (* omega plugin *)
| "protect_fv" string OPT ( "in" ident )
| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *)
| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 05:54:33 +0000