Skip to content
This repository has been archived by the owner on Feb 26, 2021. It is now read-only.

.lagda.md support #65

Open
jonaprieto opened this issue Aug 2, 2018 · 2 comments
Open

.lagda.md support #65

jonaprieto opened this issue Aug 2, 2018 · 2 comments

Comments

@jonaprieto
Copy link

I was wondering if you could please support markdown files,
I would like to take advantage of the previewer for images and other stuff
of markdown. What I have now is files (.lagda) with markdown syntax inside except for
the agda blocks. (\begin{code}\end{code}).

@banacorn
Copy link
Owner

banacorn commented Aug 3, 2018

atom/atom#17551 is working on mixing different grammars in a single file.

So far as I'm aware of there are 3 kinds of markup languages Agda supports:

agda-mode/src/type.ts

Lines 8 to 13 in dec2fb3

const enum FileType {
Agda,
LiterateTeX,
LiterateReStructuredText,
LiterateMarkdown
}

@jonaprieto
Copy link
Author

I see

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

No branches or pull requests

2 participants