From b10bd9aa54c36e2493994b21c0785133cf693bba Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Wed, 13 Dec 2023 21:54:21 +0100
Subject: [PATCH] fix: don't look for closing position of invalid document

Fixes #2
---
 src/leandoc/LeanDoc/Doc/Concrete.lean | 35 +++++++++++++++------------
 1 file changed, 19 insertions(+), 16 deletions(-)

diff --git a/src/leandoc/LeanDoc/Doc/Concrete.lean b/src/leandoc/LeanDoc/Doc/Concrete.lean
index a5813fb..5cfce25 100644
--- a/src/leandoc/LeanDoc/Doc/Concrete.lean
+++ b/src/leandoc/LeanDoc/Doc/Concrete.lean
@@ -143,19 +143,22 @@ def currentDocName [Monad m] [MonadEnv m] : m Name := do
 
 elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : command => open Lean Elab Term Command PartElabM DocElabM in do
   findGenre genre
-  let endPos := eof.raw.getTailPos?.get!
-  let .node _ _ blocks := text.raw
-    | dbg_trace "nope {ppSyntax text.raw}" throwUnsupportedSyntax
-  let ⟨`<low| [~_ ~(titleName@(.node _ _ titleParts))]>⟩ := title
-    | dbg_trace "nope {ppSyntax title}" throwUnsupportedSyntax
-  let titleString := inlinesToString (← getEnv) titleParts
-  let ((), st, st') ← liftTermElabM <| PartElabM.run {} (.init titleName) <| do
-    setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
-    for b in blocks do partCommand b
-    closePartsUntil 0 endPos
-    pure ()
-  let finished := st'.partContext.toPartFrame.close endPos
-  pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
-  saveRefs st st'
-  let docName ← mkIdentFrom title <$> currentDocName
-  elabCommand (← `(def $docName : Part $genre := $(← finished.toSyntax st'.linkDefs st'.footnoteDefs)))
+  if eof.raw.isMissing then
+    throwError "Syntax error prevents processing document"
+  else
+    let endPos := eof.raw.getTailPos?.get!
+    let .node _ _ blocks := text.raw
+      | dbg_trace "nope {ppSyntax text.raw}" throwUnsupportedSyntax
+    let ⟨`<low| [~_ ~(titleName@(.node _ _ titleParts))]>⟩ := title
+      | dbg_trace "nope {ppSyntax title}" throwUnsupportedSyntax
+    let titleString := inlinesToString (← getEnv) titleParts
+    let ((), st, st') ← liftTermElabM <| PartElabM.run {} (.init titleName) <| do
+      setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
+      for b in blocks do partCommand b
+      closePartsUntil 0 endPos
+      pure ()
+    let finished := st'.partContext.toPartFrame.close endPos
+    pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
+    saveRefs st st'
+    let docName ← mkIdentFrom title <$> currentDocName
+    elabCommand (← `(def $docName : Part $genre := $(← finished.toSyntax st'.linkDefs st'.footnoteDefs)))