Support Literate Markdown Agda?

[drcicero]

I noticed literate-agda files also use markdown sometimes (for example: https://raw.githubusercontent.com/plfa/plfa.github.io/dev/src/plfa/part1/Naturals.lagda.md).

Would supporting that look somewhat like the following? (I am new to atom, it's just a guess, based on the other file)

fileTypes: [
  'lagda.md'
]
name: 'Literate Markdown Agda'
scopeName: 'text.md.agda'
patterns: [
  {
    begin: '^```(\\s*\\n)?'
    end: '^```(\\s*\\n)?'
    contentName: 'source.agda.embedded.md.agda'
    name: 'meta.embedded.block.agda.md.agda'
    patterns: [
      {
        'include': 'source.agda'
      }
    ]
  }
  {
    include: 'text.markdown'
  }
]

[banacorn]

Sorry I'm have no idea how that TextMate grammar would look like. I've forgotten where this TextMate grammar came from.

However it is possible to parse and highlight literate-agda files with tree-sitter.

The default parser is now tree-sitter instead of TextMate grammar anyway. But regardless of which way of parsing, all PRs are welcome.

[freeman42x]

@banacorn are there any plans to implement .lagda.md support? If it is not very difficult, I might give it a try since I am currently going through PLFA, and they use that file format there. I renamed Naturals.lagda.md to Naturals.lagda and it gives the following error:

1,1-9
The name of the top level module does not match the file name. The
module Naturals should be defined in one of the following files:
  D:\Sources\agda-stdlib-1.3\src\Naturals.agda
  D:\Sources\agda-stdlib-1.3\src\Naturals.lagda
  D:\Projects\plfa.github.io\src\Naturals.agda
  D:\Projects\plfa.github.io\src\Naturals.lagda
  C:\Users\razva\AppData\Roaming\cabal\store\ghc-8.6.5\Agda-2.6.1-4e8308a0fb502e0931da3367eabd80ac5657a424\share\lib\prim\Naturals.agda
  C:\Users\razva\AppData\Roaming\cabal\store\ghc-8.6.5\Agda-2.6.1-4e8308a0fb502e0931da3367eabd80ac5657a424\share\lib\prim\Naturals.lagda

[lclem]

same here! it would be great to have literate markdown support :)