idris-lang/Idris2

Nested code blocks are ignored in literate markdown

joelberkeley opened this issue · 1 comments

Steps to Reproduce

Type check the following markdown

```idris
x : Nat
x = ""
```

* some text
  ```idris
  y : Nat
  y = ""
  ```

Expected Behavior

Both code blocks fail type-checking

Observed Behavior

Only the first fails

jfdm commented

This is expected behaviour, but not really desired behaviour.

The parser behind the literate mode is rather naive for blocks, and expects the blocks to be delineated by markers that occur at the start of the line, content too.

When fixing this 'issue' the parser would need to keep track of indentation.