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

more elegant this way

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-03-10 16:37:04 +01:00
parent 481f2b5cbb
commit 66f506c5b2
1 changed files with 7 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/leanserver/GameServer/StrInterpolation.lean
+7 -3
View File
@@ -23,9 +23,10 @@ partial def interpolatedStrNoIndentFn (p : ParserFn) : ParserFn := fun c s =>
let s := mkNodeToken interpolatedStrLitKind startPos c s let s := mkNodeToken interpolatedStrLitKind startPos c s
s.mkNode interpolatedStrKind stackSize s.mkNode interpolatedStrKind stackSize
else if curr == '\n' then else if curr == '\n' then
-- Ignore initial spaces on a new line
let s := mkNodeToken interpolatedStrLitKind startPos c s let s := mkNodeToken interpolatedStrLitKind startPos c s
let s := takeWhileFn (fun curr => curr == ' ') c s let s := takeWhileFn (fun curr => curr == ' ') c s
parse (input.prev s.pos) c s parse s.pos c s
else if curr == '\\' then else if curr == '\\' then
andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant) (parse startPos) c s andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant) (parse startPos) c s
else if curr == '{' then else if curr == '{' then
@@ -103,8 +104,11 @@ private partial def decodeInterpStrLit (s : String) : Option String :=
loop i (acc.push c) loop i (acc.push c)
else else
loop i (acc.push c) loop i (acc.push c)
loop ⟨1⟩ "" let c := s.get 0
if c == '\"' || c == '{' then
loop ⟨1⟩ ""
else
loop ⟨0⟩ ""
partial def isInterpolatedStrLit? (stx : Syntax) : Option String := partial def isInterpolatedStrLit? (stx : Syntax) : Option String :=
match Syntax.isLit? interpolatedStrLitKind stx with match Syntax.isLit? interpolatedStrLitKind stx with
| none => none | none => none