Make `Omitted` carry its location

7 files changed, 12 insertions, 11 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index 337c64f..5c1b61e 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -1376,7 +1376,8 @@ checkProof = \case
         locally (checkLemmaWithProof (Lemma [] subclaim) subproof)
         assume [Asm subclaim]
         checkProof continue
-    Omitted -> do
+    Omitted loc -> do
+        setLocation loc
         setGoals []
     Suffices loc reduction by proof -> do
         setLocation loc
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 3c91455..2e49c22 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -607,8 +607,8 @@ glossDefnHead = \case
 
 glossProof :: Raw.Proof -> Gloss Sem.Proof
 glossProof = \case
-    Raw.Omitted ->
-        pure Sem.Omitted
+    Raw.Omitted loc ->
+        pure (Sem.Omitted loc)
     Raw.Qed loc by ->
         pure (Sem.Qed loc by)
     Raw.Contradiction loc by ->
diff --git a/source/Render/Html.hs b/source/Render/Html.hs
index 58a8cde..e393eea 100644
--- a/source/Render/Html.hs
+++ b/source/Render/Html.hs
@@ -960,7 +960,7 @@ collectReferencedMarkers =
 
         collectProof :: Proof -> Set Marker
         collectProof = \case
-            Omitted ->
+            Omitted _loc ->
                 mempty
             Qed _loc justification ->
                 collectJustification justification
@@ -1145,7 +1145,7 @@ collectMissingHints hints = foldMap collectBlock
 
         collectProof :: Proof -> MissingHintMap
         collectProof = \case
-            Omitted ->
+            Omitted _loc ->
                 mempty
             Qed{} ->
                 mempty
@@ -2773,7 +2773,7 @@ referenceTargetsOfBlockRenderInfo (_index, block, blockId) =
 
 renderProof :: HintMap -> ReferenceContext -> Proof -> Html ()
 renderProof hints references = \case
-    Omitted ->
+    Omitted _loc ->
         p_ "Omitted."
     Qed mloc justification ->
         renderProofTerminal mloc justification
@@ -2929,7 +2929,7 @@ isImplicitProofEnd = \case
 
 proofStepCount :: Proof -> Int
 proofStepCount = \case
-    Omitted -> 1
+    Omitted _loc -> 1
     Qed{} -> 1
     Contradiction{} -> 1
     ByCase _loc cases -> 1 + sum (caseStepCount <$> cases)
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index c930bec..dee4076 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -628,7 +628,7 @@ data CalcQuantifier
     deriving (Show, Eq, Ord)
 
 data Proof
-    = Omitted
+    = Omitted Location
     | Qed (Maybe Location) Justification
     -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
     | Contradiction Location Justification
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 3bf5d31..cf010b3 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -385,7 +385,7 @@ grammar lexicon@Lexicon{..} = mdo
     justification <- rule (justificationSet <|> justificationRef <|> justificationLocal <|> pure JustificationEmpty)
 
     trivial          <- rule $ Qed . Just <$> _trivial <* _dot <*> pure JustificationEmpty
-    omitted          <- rule $ Omitted <$ _omitted <* _dot
+    omitted          <- rule $ Omitted <$> _omitted <* _dot
     qedJustified     <- rule $ Qed . Just <$> _follows <*> (justification <* _dot)
     qed              <- rule $ qedJustified <|> trivial <|> omitted <|> pure (Qed Nothing JustificationEmpty)
     contradiction    <- rule $ Contradiction <$> _contradiction <*> justification <* _dot
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 5037e14..5c2fb8d 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -517,7 +517,7 @@ data CalcQuantifier
     deriving (Show, Eq, Ord)
 
 data Proof
-    = Omitted
+    = Omitted Location
     -- ^ Ends a proof without further verification.
     -- This results in a “gap” in the formalization.
     | Qed {mloc :: Maybe Location, by :: Justification}
diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs
index 0bc1ed7..db0e92d 100644
--- a/source/Test/Unit/Checking.hs
+++ b/source/Test/Unit/Checking.hs
@@ -319,7 +319,7 @@ structClaimIntroducesContextBlocks =
     , BlockLemma Nowhere "foo_claim_test" (Lemma [] ((var "A" `eq` var "A") `And` (var "x" `eq` var "x")))
     , BlockProof Nowhere Nowhere $
         Have Nowhere (fooStructPredicate "A") JustificationEmpty $
-            Have Nowhere (var "x" `isElementOf` var "A") JustificationEmpty Omitted
+            Have Nowhere (var "x" `isElementOf` var "A") JustificationEmpty (Omitted Nowhere)
     ]
 
 boundStructLabelBlocks :: [Block]