Disallow unmatched inline code guards (#1414)

fredrik-bakke · web-flow · commit 30ba73e13679 · 2025-04-30T15:40:53.000+01:00
diff --git a/scripts/markdown_conventions.py b/scripts/markdown_conventions.py
@@ -13,13 +13,17 @@
 empty_block_pattern = re.compile(
     r'^```\S+.*\n(\s*\n)*\n```\s*$(?!\n(\s*\n)*</details>)', flags=re.MULTILINE)
 
+# Pattern to detect unmatched inline code guards
+unclosed_backtick_pattern = re.compile(r'^([^`]*`[^`]*`)*[^`]+`[^`]*$')
+
 
 def find_ill_formed_block(mdcode):
     """
-    Checks if in a markdown file, every (specified) opening block tag is paired
-    with a closing block tag before a new one is opened.
+    Checks if in a markdown file, every (specified) opening block guard is
+    paired with a closing block guard before a new one is opened.
 
-    Returns the line number of the first offending guard, as well as whether it is identified as a closing or opening guard.
+    Returns the line number of the first offending guard, as well as whether it
+    is identified as a closing or opening guard.
 
     Note: This also disallows unspecified code blocks.
     """
@@ -53,11 +57,39 @@ def find_ill_formed_block(mdcode):
 empty_section_eof = re.compile(
     r'^(.*\n)*#+\s([^\n]*)\n(\s*\n)*$', flags=re.MULTILINE)
 
+
+def check_unclosed_inline_code_guard(mdcode):
+    """
+    Checks if in a markdown file, every opening inline code block guard is
+    paired with a closing guard.
+
+    Returns a list of line numbers.
+    """
+    # Split the content into lines for line number tracking
+    lines = mdcode.split('\n')
+
+    # Check each line that's not in a code block
+    in_code_block = False
+    problematic_lines = []
+
+    for i, line in enumerate(lines, 1):  # Start counting from 1 for line numbers
+        stripped = line.strip()
+        if stripped.startswith('```'):
+            in_code_block = not in_code_block
+            continue
+
+        if not in_code_block and unclosed_backtick_pattern.match(line):
+            problematic_lines.append(i)
+
+    return problematic_lines
+
+
 if __name__ == '__main__':
 
     STATUS_UNSPECIFIED_OR_ILL_FORMED_BLOCK = 1
     STATUS_TOP_LEVEL_HEADER_AFTER_FIRST_LINE = 2
     STATUS_EMPTY_SECTION = 4
+    STATUS_UNCLOSED_BACKTICK = 8
 
     status = 0
 
@@ -80,6 +112,14 @@ def find_ill_formed_block(mdcode):
 
             status |= STATUS_UNSPECIFIED_OR_ILL_FORMED_BLOCK
 
+        # Check for unmatched backticks outside of Agda code blocks
+        backtick_lines = check_unclosed_inline_code_guard(output)
+        if backtick_lines:
+            line_list = ", ".join(str(line) for line in backtick_lines)
+            print(
+                f"Error! File '{fpath}' line(s) {line_list} contain backticks (`) for guarding inline code blocks that don't have matching closing or opening guards. Please add the matching backtick(s).")
+            status |= STATUS_UNCLOSED_BACKTICK
+
         if top_level_header_after_first_line.search(output):
             print(
                 f"Error! File '{fpath}' has a top level header after the first line. Please increase the header's level.")
diff --git a/src/elementary-number-theory/based-induction-natural-numbers.lagda.md b/src/elementary-number-theory/based-induction-natural-numbers.lagda.md
@@ -31,7 +31,7 @@ family `P` of types over `ℕ` and any natural number `k : ℕ`, equipped with
 
 such that
 
-1. `based-ind-ℕ k P p0 pS k K ＝ p0` for any `K : k ≤-ℕ k, and
+1. `based-ind-ℕ k P p0 pS k K ＝ p0` for any `K : k ≤-ℕ k`, and
 2. `based-ind-ℕ k P p0 pS (n + 1) N' ＝ pS n N (based-ind-ℕ k P p0 pS n N` for
    any `N : k ≤-ℕ n` and any `N' : k ≤-ℕ n + 1`.
 
diff --git a/src/foundation/diagonals-of-morphisms-arrows.lagda.md b/src/foundation/diagonals-of-morphisms-arrows.lagda.md
@@ -41,7 +41,7 @@ maps `i` and `j`, which fit in a naturality square
 ```
 
 In other words, the diagonal of a morphism of arrows `h : hom-arrow f g` is a
-morphism of arrows `Δ h : hom-arrow f (functoriality Δ g).
+morphism of arrows `Δ h : hom-arrow f (functoriality Δ g)`.
 
 Note that this operation preserves
 [cartesian squares](foundation.cartesian-morphisms-arrows.md). Furthermore, by a
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
@@ -113,7 +113,7 @@ equivalences are contractible maps, it follows that the
 at `id : A → A` is contractible, i.e., the type `Σ (B → A) (λ h → h ∘ f ＝ id)`
 is contractible. Furthermore, since fiberwise equivalences induce equivalences
 on total spaces, it follows from
-[function extensionality](foundation.function-extensionality.md)` that the type
+[function extensionality](foundation.function-extensionality.md) that the type
 
 ```text
   Σ (B → A) (λ h → h ∘ f ~ id)
diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
@@ -293,11 +293,11 @@ The Regensburg extension of the fundamental theorem is used in the following
 files:
 
 - In
-  [`higher-group-theory.free-higher-group-actions.md`](higher-group-theory.free-higher-group-actions.md)
+  [`higher-group-theory.free-higher-group-actions`](higher-group-theory.free-higher-group-actions.md)
   it is used to show that a higher group action is free if and only its total
   space is a set.
 - In
-  [`higher-group-theory.transitive-higher-group-actions.md`](higher-group-theory.transitive-higher-group-actions.md)
+  [`higher-group-theory.transitive-higher-group-actions`](higher-group-theory.transitive-higher-group-actions.md)
   it is used to show that a higher group action is transitive if and only if its
   total space is connected.
 
diff --git a/src/graph-theory/dependent-reflexive-graphs.lagda.md b/src/graph-theory/dependent-reflexive-graphs.lagda.md
@@ -44,8 +44,8 @@ Alternatively, a dependent reflexive graph `B` over `A` can be defined by
 - A family `B₀ : A₀ → Reflexive-Graph` of reflexive graphs as the type family of
   vertices
 - A family `B₁ : {x y : A₀} → A₁ x y → (B₀ x)₀ → (B₀ y)₀ → 𝒰`.
-- A [family of equivalences](foundation.families-of-equivalences.md) `refl B :
-  (x : A₀) (y y' : B₀ x) → B₁ (refl A x) y y' ≃ (B₀ x)₁ y y'.
+- A [family of equivalences](foundation.families-of-equivalences.md)
+  `refl B : (x : A₀) (y y' : B₀ x) → B₁ (refl A x) y y' ≃ (B₀ x)₁ y y'`.
 
 This definition is more closely related to the concept of morphism into the
 universal reflexive graph.
diff --git a/src/group-theory/conjugation.lagda.md b/src/group-theory/conjugation.lagda.md
@@ -40,7 +40,7 @@ the map `y ↦ (xy)x⁻¹`. This can be seen as a homomorphism `G → G` as well
 group action of `G` onto itself.
 
 The delooping of the conjugation homomorphism is defined in
-[`structured-types.conjugation-pointed-types.md`](structured-types.conjugation-pointed-types.md)`.
+[`structured-types.conjugation-pointed-types`](structured-types.conjugation-pointed-types.md).
 
 ## Definitions
 
diff --git a/src/group-theory/pullbacks-subsemigroups.lagda.md b/src/group-theory/pullbacks-subsemigroups.lagda.md
@@ -81,7 +81,7 @@ module _
     is-closed-under-eq-Subsemigroup' G pullback-Subsemigroup
 ```
 
-### The order preserving operation `pullback-Subsemigroup
+### The order preserving operation `pullback-Subsemigroup`
 
 ```agda
 module _
diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md
@@ -657,8 +657,8 @@ module _
 
 The subset consisting of elements `x : G` such that `(1 ＝ x) ∨ P` holds is
 always a subgroup of `G`. This subgroup consists only of the unit element if `P`
-is false, and it is the [full subgroup](group-theory.full-subgroups.md)`if`P` is
-true.
+is false, and it is the [full subgroup](group-theory.full-subgroups.md) if `P`
+is true.
 
 ```agda
 module _
diff --git a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
@@ -269,7 +269,7 @@ diagram
      f     g
 ```
 
-The composite `g ∘ f` is then an extension of `c` along `a.
+The composite `g ∘ f` is then an extension of `c` along `a`.
 
 ```agda
 module _
diff --git a/src/structured-types/types-equipped-with-automorphisms.lagda.md b/src/structured-types/types-equipped-with-automorphisms.lagda.md
@@ -62,7 +62,7 @@ pr2 (trivial-Type-With-Automorphism X) = id-equiv
 ## See also
 
 - Sets equipped with automorphisms are defined in
-  [`structured-types.sets-equipped-with-automorphisms.md`](structured-types.sets-equipped-with-automorphisms.md)
+  [`structured-types.sets-equipped-with-automorphisms`](structured-types.sets-equipped-with-automorphisms.md)
 - Cyclic types are
   [sets equipped with automorphisms](structured-types.sets-equipped-with-automorphisms.md)
   of which the automorphism acts transitively.
diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md
@@ -64,7 +64,7 @@ we can characterize dependent cocones over a suspension cocone as equivalent to
 the following:
 
 For a suspension structure `(N , S , m)`, a dependent suspension structure in
-`P` over (N , S , m)` is given by points
+`P` over `(N , S , m)` is given by points
 
 ```text
 north : P N
diff --git a/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md
@@ -66,9 +66,9 @@ and the gluing data sending `h : PA (fs) → RA (fs)` to
 **Note:** It is important to differentiate between families of _function types_,
 i.e. a type family that to every `x : X` assigns the _type_ `P x → R x`, and
 families of _functions_, i.e. a family that to every `x : X` assigns a
-_function_ from `P x` to R x`. Descent data plays the role of a family of types,
-so it makes sense to talk about "descent data corresponding to a family of
-function types", but it doesn't make sense to talk about "descent data
+_function_ from `P x` to `R x`. Descent data plays the role of a family of
+types, so it makes sense to talk about "descent data corresponding to a family
+of function types", but it doesn't make sense to talk about "descent data
 corresponding to a family of functions". The kind of data that corresponds to
 families of functions are the _sections_ of the descent data of a family of
 function types.
diff --git a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md
@@ -31,7 +31,7 @@ open import synthetic-homotopy-theory.loop-spaces
 ## Idea
 
 Any [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` induces a
-pointed map `pointed-map-Ω f : Ω A →∗ Ω B`` on
+pointed map `pointed-map-Ω f : Ω A →∗ Ω B` on
 [loop spaces](synthetic-homotopy-theory.loop-spaces.md). Furthermore, this
 operation respects the groupoidal operations on loop spaces.
 
diff --git a/src/synthetic-homotopy-theory/homotopy-groups.lagda.md b/src/synthetic-homotopy-theory/homotopy-groups.lagda.md
@@ -37,8 +37,8 @@ where
 - `π₀ A` is the set of
   [connected components](foundation.connected-components.md) of `A`, and
 - `πᵢ₊₁ A` is the set `πᵢ ΩA` equipped with the
-  [group structure](group-theory.groups.md) obtained from the [loop
-  space](synthetic-homotopy theory.loop-spaces.md).
+  [group structure](group-theory.groups.md) obtained from the
+  [loop space](synthetic-homotopy-theory.loop-spaces.md).
 
 For `i ≥ 2`, the `i`-th homotopy group `πᵢ A` of `A` is
 [abelian](group-theory.abelian-groups.md) by the
diff --git a/src/synthetic-homotopy-theory/morphisms-descent-data-circle.lagda.md b/src/synthetic-homotopy-theory/morphisms-descent-data-circle.lagda.md
@@ -20,9 +20,9 @@ open import synthetic-homotopy-theory.descent-circle
 ## Idea
 
 Given two [descent data](synthetic-homotopy-theory.descent-circle.md) `(A,e)`
-and `(B,f)` over the
-[circle](synthetic-homotopy-theory.circle.md)`, a **morphism** `h`of descent data between`(A,
-e)`and`(B, f)`is a map`h`from`A`to`B` such that the square
+and `(B,f)` over the [circle](synthetic-homotopy-theory.circle.md), a
+**morphism** `h` of descent data between `(A, e)` and `(B, f) `is a map `h` from
+`A` to `B` such that the square
 
 ```text
       h
diff --git a/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md b/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md
@@ -31,7 +31,7 @@ open import trees.polynomial-endofunctors
 ## Idea
 
 A **morphism** of algebras of a polynomial endofunctor `P A B` consists of a map
-`f : X → Y$ between the underlying types, equipped with a homotopy witnessing
+`f : X → Y` between the underlying types, equipped with a homotopy witnessing
 that the square
 
 ```text
diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md
@@ -334,7 +334,7 @@ module _
     leq-is-emb-is-finite (is-emb-is-injective (is-set-is-finite K) I)
 ```
 
-#### There are no embeddings between finite types `A` and `B` such that `|B| < |A|
+#### There are no embeddings between finite types `A` and `B` such that `|B| < |A|`
 
 ```agda
   is-not-emb-le-is-finite :
@@ -353,7 +353,7 @@ module _
             ( E)))
 ```
 
-#### There are no injective maps between finite types `A` and `B` such that `|B| < |A|
+#### There are no injective maps between finite types `A` and `B` such that `|B| < |A|`
 
 ```agda
   is-not-injective-le-is-finite :
diff --git a/tables/loop-spaces-concepts.md b/tables/loop-spaces-concepts.md
@@ -7,6 +7,6 @@
 | Free loops                   | [`synthetic-homotopy-theory.free-loops`](synthetic-homotopy-theory.free-loops.md)                                 |
 | Functoriality of loop spaces | [`synthetic-homotopy-theory.functoriality-loop-spaces`](synthetic-homotopy-theory.functoriality-loop-spaces.md)   |
 | Groups of loops in 1-types   | [`synthetic-homotopy-theory.groups-of-loops-in-1-types`](synthetic-homotopy-theory.groups-of-loops-in-1-types.md) |
-| Iterated loop spaces         | [`synthetic-homotopy-theory.iterated-loop-spaces'](synthetic-homotopy-theory.iterated-loop-spaces.md)             |
+| Iterated loop spaces         | [`synthetic-homotopy-theory.iterated-loop-spaces`](synthetic-homotopy-theory.iterated-loop-spaces.md)             |
 | Powers of loops              | [`synthetic-homotopy-theory.powers-of-loops`](synthetic-homotopy-theory.powers-of-loops.md)                       |
 | Triple loop spaces           | [`synthetic-homotopy-theory.triple-loop-spaces`](synthetic-homotopy-theory.triple-loop-spaces.md)                 |
