mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
Added some modest improvements to code.
This commit is contained in:
parent
ef85348de8
commit
49b4f97c5d
@ -62,28 +62,28 @@ rawTokens delims ls =
|
||||
++ [(notCodeLine, Any)]
|
||||
|
||||
||| Merge the tokens into a single source file.
|
||||
reduce : List (TokenData Token) -> String -> String
|
||||
reduce [] acc = acc
|
||||
reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (acc ++ blank_content)
|
||||
reduce : List (TokenData Token) -> List String -> String
|
||||
reduce [] acc = fastAppend (reverse acc)
|
||||
reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc)
|
||||
where
|
||||
-- Preserve the original document's line count.
|
||||
blank_content : String
|
||||
blank_content = if elem '\n' (unpack x)
|
||||
then concat $ replicate (length (lines x)) "\n"
|
||||
else ""
|
||||
blank_content = fastAppend (replicate (length (lines x)) "\n")
|
||||
|
||||
reduce (MkToken _ _ (CodeLine m src) :: rest) acc =
|
||||
if m == trim src
|
||||
then reduce rest (acc ++ "\n")
|
||||
else reduce rest (acc ++ (substr (length m + 1) -- remove space to right of marker.
|
||||
(length src)
|
||||
src))
|
||||
then reduce rest ("\n"::acc)
|
||||
else reduce rest ((substr (length m + 1) -- remove space to right of marker.
|
||||
(length src)
|
||||
src
|
||||
)::acc)
|
||||
|
||||
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
|
||||
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
|
||||
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
|
||||
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
|
||||
reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
|
||||
reduce rest (acc ++ "\n" ++ unlines srcs)
|
||||
reduce rest ("\n" :: unlines srcs :: acc)
|
||||
|
||||
-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
|
||||
|
||||
@ -164,7 +164,7 @@ extractCode : (specification : LiterateStyle)
|
||||
-> Either LiterateError String
|
||||
extractCode (MkLitStyle delims markers exts) str =
|
||||
case lex (rawTokens delims markers) str of
|
||||
(toks, (_,_,"")) => Right $ reduce toks ""
|
||||
(toks, (_,_,"")) => Right (reduce toks Nil)
|
||||
(_, (l,c,i)) => Left (MkLitErr l c i)
|
||||
|
||||
||| Synonym for `extractCode`.
|
||||
|
Loading…
Reference in New Issue
Block a user