5 files changed, 42 insertions, 27 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index a3fc069e6c..de0d912c03 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -48,28 +48,22 @@ def coqdoc(coq_code, coqdoc_bin=None):
     finally:
         os.remove(filename)
 
-def is_whitespace_string(elem):
-    return isinstance(elem, NavigableString) and elem.strip() == ""
-
-def strip_soup(soup, pred):
-    """Strip elements matching pred from front and tail of soup."""
-    while soup.contents and pred(soup.contents[-1]):
-        soup.contents.pop()
-
-    skip = 0
-    for elem in soup.contents:
-        if not pred(elem):
-            break
-        skip += 1
-
-    soup.contents[:] = soup.contents[skip:]
+def first_string_node(node):
+    """Return the first string node, or None if does not exist"""
+    while node.children:
+        node = next(node.children)
+        if isinstance(node, NavigableString):
+            return node
 
 def lex(source):
     """Convert source into a stream of (css_classes, token_string)."""
     coqdoc_output = coqdoc(source)
     soup = BeautifulSoup(coqdoc_output, "html.parser")
     root = soup.find(class_='code')
-    strip_soup(root, is_whitespace_string)
+    # strip the leading '\n'
+    first = first_string_node(root)
+    if first and first.string[0] == '\n':
+        first.string.replace_with(first.string[1:])
     for elem in root.children:
         if isinstance(elem, NavigableString):
             yield [], elem
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 9d51d2198a..df11960403 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -905,9 +905,13 @@ class CoqtopBlocksTransform(Transform):
         return isinstance(node, nodes.Element) and 'coqtop_options' in node
 
     @staticmethod
-    def split_sentences(source):
-        """Split Coq sentences in source. Could be improved."""
-        return re.split(r"(?<=(?<!\.)\.)\s+", source)
+    def split_lines(source):
+        """Split Coq input in chunks
+
+        A chunk is a minimal sequence of consecutive lines of the input that
+        ends with a '.'
+        """
+        return re.split(r"(?<=(?<!\.)\.)\s+\n", source)
 
     @staticmethod
     def parse_options(node):
@@ -986,7 +990,7 @@ class CoqtopBlocksTransform(Transform):
             repl.sendone('Unset Coqtop Exit On Error.')
         if options['warn']:
             repl.sendone('Set Warnings "default".')
-        for sentence in self.split_sentences(node.rawsource):
+        for sentence in self.split_lines(node.rawsource):
             pairs.append((sentence, repl.sendone(sentence)))
         if options['abort']:
             repl.sendone('Abort All.')
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index c7e3ee18ad..62cc8ea86b 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1839,3 +1839,7 @@ sentence: [
 document: [
 | LIST0 sentence
 ]
+
+strategy_level: [
+| DELETE strategy_level0
+]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 4274dccb40..92e9df51d5 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -451,6 +451,14 @@ bar_cbrace: [
 | test_pipe_closedcurly "|" "}"
 ]
 
+strategy_level: [
+| "expand"
+| "opaque"
+| integer
+| "transparent"
+| strategy_level0
+]
+
 vernac_toplevel: [
 | "Drop" "."
 | "Quit" "."
@@ -1213,13 +1221,6 @@ more_implicits_block: [
 | "{" LIST1 name "}"
 ]
 
-strategy_level: [
-| "expand"
-| "opaque"
-| integer
-| "transparent"
-]
-
 instance_name: [
 | ident_decl binders
 |
@@ -1598,6 +1599,7 @@ simple_tactic: [
 | "guard" test
 | "decompose" "[" LIST1 constr "]" constr
 | "optimize_heap"
+| "with_strategy" strategy_level_or_var "[" LIST1 smart_global "]" tactic3
 | "eassumption"
 | "eexact" constr
 | "trivial" auto_using hintbases
@@ -1855,6 +1857,11 @@ test_lpar_id_colon: [
 | local_test_lpar_id_colon
 ]
 
+strategy_level_or_var: [
+| strategy_level
+| identref
+]
+
 comparison: [
 | "="
 | "<"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index df4e5a22e3..11f06b7b8a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -659,6 +659,11 @@ strategy_level: [
 | "transparent"
 ]
 
+strategy_level_or_var: [
+| strategy_level
+| ident
+]
+
 reserv_list: [
 | LIST1 ( "(" simple_reserv ")" )
 | simple_reserv
@@ -1234,6 +1239,7 @@ simple_tactic: [
 | "guard" int_or_var comparison int_or_var
 | "decompose" "[" LIST1 one_term "]" one_term
 | "optimize_heap"
+| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"