Add support for literat Cryptol with RST #1443
Conversation
src/Cryptol/Parser/Unlit.hs
Outdated
| {-# LANGUAGE OverloadedStrings, Safe, PatternGuards #-} | ||
| {-# LANGUAGE OverloadedStrings, PatternGuards #-} |
There was a problem hiding this comment.
Is the code in this module no longer Safe?
There was a problem hiding this comment.
It is still Safe. I think we've been using Safe incorrectly, probably due to a historical misunderstanding on my part about what the pragma means, so I thought I might as well start fixing things slowly. In particular, GHC can already infer which modules are safe and which are not, without the pragma. Instead, the pragma explicitly asks GHC to check if a module is safe, and complain if it is not. So I don't think we need to annotate every single module with Safe, but rather we should add it to modules where we want this checked. We currently don't really have a use case for this feature, so I am not sure which modules should have the annotation...
There was a problem hiding this comment.
Ah, I see. I don't have too strong of an opinion about Safe myself (if anything, I am slightly biased against it), so I'm happy to defer to your judgment about whether they should be kept or removed.
src/Cryptol/Parser/Unlit.hs
Outdated
| rst :: [Text] -> [Block] | ||
| rst = comment [] | ||
| where | ||
| isBeginCode l = case filter (not . Text.null) (Text.splitOn " " l) of |
There was a problem hiding this comment.
I wonder if this should use Text.split isSpace instead, both for consistency with isEmpty/isCode and to catch other whitespace characters.
src/Cryptol/Parser/Unlit.hs
Outdated
| l : ls1 | isBeginCode l -> codeOptoins (l : acc) ls1 | ||
| | otherwise -> comment (l : acc) ls1 | ||
|
|
||
| codeOptoins acc ls = |
There was a problem hiding this comment.
| codeOptoins acc ls = | |
| codeOptions acc ls = |
src/Cryptol/Parser/Unlit.hs
Outdated
| comment acc ls = | ||
| case ls of | ||
| [] -> mk Comment acc | ||
| l : ls1 | isBeginCode l -> codeOptoins (l : acc) ls1 |
There was a problem hiding this comment.
| l : ls1 | isBeginCode l -> codeOptoins (l : acc) ls1 | |
| l : ls1 | isBeginCode l -> codeOptions (l : acc) ls1 |
src/Cryptol/Parser/Unlit.hs
Outdated
| case ls of | ||
| [] -> mk Comment acc | ||
| l : ls1 | isEmpty l -> mk Comment (l : acc) ++ code [] ls1 | ||
| | otherwise -> codeOptoins (l : acc) ls1 |
There was a problem hiding this comment.
| | otherwise -> codeOptoins (l : acc) ls1 | |
| | otherwise -> codeOptions (l : acc) ls1 |
src/Cryptol/Parser/Unlit.hs
Outdated
| rst = comment [] | ||
| where | ||
| isBeginCode l = case filter (not . Text.null) (Text.splitOn " " l) of | ||
| ["..", "code::", "cryptol"] -> True |
There was a problem hiding this comment.
I wonder if we should recognize code-block:: and sourcecode:: in addition to code::? The first two are officially recognized directives in Sphinx.
In fact, code is technically a different thing altogether, although I don't know if strict adherence to Sphinx's rules is a goal for Cryptol.
There was a problem hiding this comment.
You are quite right, I was reading the docs for code-block and I guess auto-corrected it code :)
|
@yav I tested it and it correctly parses all rst examples I have available. Thanks for putting it together! |
This implements supports for literate Cryptol with RST, see #1441