phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix #8

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-01-20 13:57:04 +01:00
parent 7c66d6c7de
commit edc49184a6
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/leanserver/GameServer/FileWorker.lean
+1 -1
View File
@@ -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 pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
let (tacticStx, cmdParserState, msgLog, endOfWhitespace) := let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap 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 if Parser.isEOI tacticStx then
let endSnap : Snapshot := { let endSnap : Snapshot := {
beginPos := cmdPos beginPos := cmdPos