From edc49184a66bacdb728b90d1f2b5d36554df508d Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 20 Jan 2023 13:56:49 +0100
Subject: [PATCH] fix #8

---
 server/leanserver/GameServer/FileWorker.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index 1029f62..9bed1eb 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -71,7 +71,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
     MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
-  let cmdPos := tacticStx.getPos?.get!
+  let cmdPos := tacticStx.getPos?.getD 0
   if Parser.isEOI tacticStx then
     let endSnap : Snapshot := {
       beginPos := cmdPos