0558972 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix parsing of indented blocks

If there is no indentation, the block should be considered empty. This means empty parameters or using blocks are no longer allowed, which was always the intention, and empty data/instance/class declarations are allowed without needing an explicit {}. Fixes #437

commit0558972df13d7c28947560bead4aefc5d4a716b7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 3 Aug 2013, 17:43 (13 years ago) parente410ab3

1 file changed+9−1

compare with master

unifiedsplit

src/Idris/Parser.hs+9−1

src/Idris/Parser.hs+9−1

@@ -211,7 +211,15 @@ openBlock = do lchar '{'

211211 ist <- getState

212212 setState (ist { brace_stack = Nothing : brace_stack ist })

213213 <|> do ist <- getState

214− lvl <- indent

214+ lvl' <- indent

215+ -- if we're not indented further, it's an empty block, so

216+ -- increment lvl to ensure we get to the end

217+ let lvl = case brace_stack ist of

218+ Just lvl_old : _ ->

219+ if lvl' <= lvl_old then lvl_old+1

220+ else lvl'

221+ [] -> if lvl' == 1 then 2 else lvl'

222+ _ -> lvl'

215223 setState (ist { brace_stack = Just lvl : brace_stack ist })

216224

217225closeBlock :: IParser ()