diff --git a/server/leanserver/GameServer/StrInterpolation.lean b/server/leanserver/GameServer/StrInterpolation.lean index 643a608..935e941 100644 --- a/server/leanserver/GameServer/StrInterpolation.lean +++ b/server/leanserver/GameServer/StrInterpolation.lean @@ -7,6 +7,19 @@ as quotes. import Lean namespace Lean.Parser +/-- Push `(Syntax.node tk )` onto syntax stack if parse was successful. -/ +def mkNodeTokenNoWs (n : SyntaxNodeKind) (startPos : String.Pos) : ParserFn := fun c s => Id.run do + if s.hasError then + return s + let input := c.input + let stopPos := s.pos + let leading := mkEmptySubstringAt input startPos + let val := input.extract startPos stopPos + let wsStopPos := s.pos + let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring } + let info := SourceInfo.original leading startPos trailing stopPos + s.pushSyntax (Syntax.mkLit n val info) + partial def interpolatedStrNoIndentFn (p : ParserFn) : ParserFn := fun c s => let input := c.input let stackSize := s.stackSize @@ -24,7 +37,7 @@ partial def interpolatedStrNoIndentFn (p : ParserFn) : ParserFn := fun c s => s.mkNode interpolatedStrKind stackSize else if curr == '\n' then -- Ignore initial spaces on a new line - let s := mkNodeToken interpolatedStrLitKind startPos c s + let s := mkNodeTokenNoWs interpolatedStrLitKind startPos c s let s := takeWhileFn (fun curr => curr == ' ') c s parse s.pos c s else if curr == '\\' then @@ -98,7 +111,7 @@ private partial def decodeInterpStrLit (s : String) : Option String := else if c == '\n' then pure (acc.push c) else if s.atEnd i then - none + pure acc else if c == '\\' then do let (c, i) ← decodeInterpStrQuotedChar s i loop i (acc.push c) diff --git a/server/testgame/TestGame/Levels/Function/L11_Inverse.lean b/server/testgame/TestGame/Levels/Function/L11_Inverse.lean index 5ee50f3..14ac036 100644 --- a/server/testgame/TestGame/Levels/Function/L11_Inverse.lean +++ b/server/testgame/TestGame/Levels/Function/L11_Inverse.lean @@ -18,12 +18,16 @@ aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst. " open Function - +set_option pp.rawOnError true Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by Branch exfalso - Hint "Das war eine blöde Idee" + Hint "Das war eine blöde Idee + dd + + ddds + " Hint (hidden := true) "constructor" constructor Hint "intro h" -- does not show