diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs b/src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs
new file mode 100644
index 000000000..b4953f8ae
--- /dev/null
+++ b/src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs
@@ -0,0 +1,66 @@
+module Juvix.Compiler.Backend.Markdown.Data.MkJuvixBlockOptions where
+
+import Juvix.Parser.Error.Base
+import Juvix.Prelude.Base
+import Juvix.Prelude.Parsing hiding (runParser)
+import Juvix.Prelude.Path
+import Text.Megaparsec qualified as P
+import Text.Megaparsec.Char.Lexer qualified as L
+
+data MkJuvixBlockOptions
+ = MkJuvixBlockOptionsHide
+ | MkJuvixBlockOptionsShow
+ | MkJuvixBlockOptionsExtractModule JuvixBlockOptionsExtractModule
+ deriving stock (Eq, Show)
+
+newtype JuvixBlockOptionsExtractModule = JuvixBlockOptionsExtractModule
+ { _juvixBlockOptionsExtractModuleDrop :: Int
+ }
+ deriving stock (Eq, Show)
+
+makeLenses ''JuvixBlockOptionsExtractModule
+
+optionExtractModuleStatements :: (IsString s) => s
+optionExtractModuleStatements = "extract-module-statements"
+
+optionHide :: (IsString s) => s
+optionHide = "hide"
+
+parseJuvixBlockOptions :: Path Abs File -> Text -> Either MegaparsecError MkJuvixBlockOptions
+parseJuvixBlockOptions p = mapLeft MegaparsecError . P.runParser parseOptions (toFilePath p)
+
+type Parser = P.Parsec Void Text
+
+spaceConsumer :: Parser ()
+spaceConsumer = L.space space1 empty empty
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme spaceConsumer
+
+symbol :: Text -> Parser ()
+symbol = void . L.symbol spaceConsumer
+
+decimal :: Parser Int
+decimal = lexeme L.decimal
+
+parseOptions :: Parser MkJuvixBlockOptions
+parseOptions = do
+ spaceConsumer
+ opts <-
+ parseHide
+ <|> parseExtractModule
+ <|> parseShow
+ eof
+ return opts
+
+parseShow :: Parser MkJuvixBlockOptions
+parseShow = return MkJuvixBlockOptionsShow
+
+parseHide :: Parser MkJuvixBlockOptions
+parseHide = symbol optionHide $> MkJuvixBlockOptionsHide
+
+parseExtractModule :: Parser MkJuvixBlockOptions
+parseExtractModule = do
+ symbol optionExtractModuleStatements
+ dropNum <- fromMaybe 0 <$> optional decimal
+ return (MkJuvixBlockOptionsExtractModule (JuvixBlockOptionsExtractModule dropNum))
diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
index 6ed14f423..f9e3fc8b9 100644
--- a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
+++ b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
@@ -1,20 +1,20 @@
-module Juvix.Compiler.Backend.Markdown.Data.Types where
+module Juvix.Compiler.Backend.Markdown.Data.Types
+ ( module Juvix.Compiler.Backend.Markdown.Data.Types,
+ module Juvix.Compiler.Backend.Markdown.Data.MkJuvixBlockOptions,
+ )
+where
import Commonmark qualified as MK
import Data.Text qualified as T
+import Juvix.Compiler.Backend.Markdown.Data.MkJuvixBlockOptions
import Juvix.Data.Loc
import Juvix.Prelude hiding (Raw)
import Juvix.Prelude.Pretty
import Text.Show qualified as Show
-newtype MkJuvixBlockOptions = MkJuvixBlockOptions
- { _mkJuvixBlockOptionsHide :: Bool
- }
- deriving stock (Eq, Ord)
-
data JuvixCodeBlock = JuvixCodeBlock
{ _juvixCodeBlock :: Text,
- _juvixCodeBlockOptions :: MkJuvixBlockOptions,
+ _juvixCodeBlockOptions :: Text,
_juvixCodeBlockInterval :: Maybe Interval
}
deriving stock (Eq, Ord)
@@ -26,33 +26,16 @@ data TextBlock = TextBlock
deriving stock (Eq, Ord)
makeLenses ''JuvixCodeBlock
-makeLenses ''MkJuvixBlockOptions
makeLenses ''TextBlock
-defaultMkJuvixBlockOptions :: MkJuvixBlockOptions
-defaultMkJuvixBlockOptions =
- MkJuvixBlockOptions
- { _mkJuvixBlockOptionsHide = False
- }
-
instance Show TextBlock where
show t = T.unpack (t ^. textBlock)
-textJuvixBlockOptions :: MkJuvixBlockOptions -> Text
-textJuvixBlockOptions opt =
- T.intercalate " " $
- catMaybes
- [ if opt ^. mkJuvixBlockOptionsHide then Just "hide" else Nothing
- ]
-
-instance Show MkJuvixBlockOptions where
- show opt = T.unpack (textJuvixBlockOptions opt)
-
textJuvixCodeBlock :: JuvixCodeBlock -> Text
textJuvixCodeBlock cb =
mconcat
[ "```juvix",
- textJuvixBlockOptions (cb ^. juvixCodeBlockOptions),
+ cb ^. juvixCodeBlockOptions,
nl,
cb ^. juvixCodeBlock,
"```"
@@ -83,19 +66,6 @@ instance Monoid TextBlock where
}
mappend = (<>)
-instance Semigroup MkJuvixBlockOptions where
- a <> b =
- MkJuvixBlockOptions
- { _mkJuvixBlockOptionsHide = a ^. mkJuvixBlockOptionsHide || b ^. mkJuvixBlockOptionsHide
- }
-
-instance Monoid MkJuvixBlockOptions where
- mempty =
- MkJuvixBlockOptions
- { _mkJuvixBlockOptionsHide = False
- }
- mappend = (<>)
-
instance Semigroup Mk where
a <> MkNull = a
MkNull <> a = a
@@ -190,25 +160,20 @@ instance MK.IsInline TextBlock where
toTextBlock t
| otherwise = mempty
-getJuvixBlockOptions :: Text -> MkJuvixBlockOptions
-getJuvixBlockOptions = \case
- "hide" -> mempty {_mkJuvixBlockOptionsHide = True}
- _ -> mempty
-
nl' :: Mk
nl' = toMK nl
processCodeBlock :: Text -> Text -> Maybe Interval -> Mk
processCodeBlock info t loc =
- case T.splitOn " " (T.strip info) of
- ("juvix" : opts) ->
+ case T.stripPrefix "juvix" (T.strip info) of
+ Just opts ->
MkJuvixCodeBlock
JuvixCodeBlock
{ _juvixCodeBlock = t,
- _juvixCodeBlockOptions = foldMap getJuvixBlockOptions opts,
+ _juvixCodeBlockOptions = opts,
_juvixCodeBlockInterval = loc
}
- _ ->
+ Nothing ->
let b = "```" <> info <> t <> "```"
in MkTextBlock TextBlock {_textBlock = b, _textBlockInterval = loc}
diff --git a/src/Juvix/Compiler/Backend/Markdown/Error.hs b/src/Juvix/Compiler/Backend/Markdown/Error.hs
index ad1ec48b4..a9cc15541 100644
--- a/src/Juvix/Compiler/Backend/Markdown/Error.hs
+++ b/src/Juvix/Compiler/Backend/Markdown/Error.hs
@@ -1,18 +1,24 @@
module Juvix.Compiler.Backend.Markdown.Error where
+import Juvix.Compiler.Backend.Markdown.Data.Types
import Juvix.Compiler.Concrete.Language
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
+import Juvix.Parser.Error.Base
import Juvix.Prelude
data MarkdownBackendError
= ErrInternalNoMarkdownInfo NoMarkdownInfoError
| ErrNoJuvixCodeBlocks NoJuvixCodeBlocksError
+ | ErrInvalidExtractModuleBlock InvalidExtractModuleBlockError
+ | ErrInvalidCodeBlockAttribtues InvalidCodeBlockAttributesError
deriving stock (Show)
instance ToGenericError MarkdownBackendError where
genericError = \case
ErrInternalNoMarkdownInfo e -> genericError e
ErrNoJuvixCodeBlocks e -> genericError e
+ ErrInvalidExtractModuleBlock e -> genericError e
+ ErrInvalidCodeBlockAttribtues e -> genericError e
newtype NoMarkdownInfoError = NoMarkdownInfoError
{ _noMarkdownInfoFilepath :: Path Abs File
@@ -49,3 +55,35 @@ instance ToGenericError NoJuvixCodeBlocksError where
where
i :: Interval
i = singletonInterval . mkInitialLoc $ _noJuvixCodeBlocksErrorFilepath
+
+data InvalidExtractModuleBlockError = InvalidExtractModuleBlockError
+ { _invalidExtractModuleBlockErrorInterval :: Maybe Interval,
+ _invalidExtractModuleBlockErrorPath :: Path Abs File
+ }
+ deriving stock (Show)
+
+instance ToGenericError InvalidExtractModuleBlockError where
+ genericError InvalidExtractModuleBlockError {..} = do
+ let msg :: Doc Ann
+ msg = "Juvix code blocks with attribute" <+> optionExtractModuleStatements <+> "must contain a single local module"
+ return
+ GenericError
+ { _genericErrorLoc = i,
+ _genericErrorMessage = prettyError msg,
+ _genericErrorIntervals = [i]
+ }
+ where
+ i :: Interval
+ i =
+ fromMaybe
+ (singletonInterval (mkInitialLoc (_invalidExtractModuleBlockErrorPath)))
+ _invalidExtractModuleBlockErrorInterval
+
+newtype InvalidCodeBlockAttributesError = InvalidCodeBlockAttributesError
+ { _invalidCodeBlockAttributesErrorMegaparsecError :: MegaparsecError
+ }
+ deriving stock (Show)
+
+instance ToGenericError InvalidCodeBlockAttributesError where
+ genericError InvalidCodeBlockAttributesError {..} =
+ genericError _invalidCodeBlockAttributesErrorMegaparsecError
diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
index 80fe7851d..7e652651d 100644
--- a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
+++ b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
@@ -86,7 +86,7 @@ fromJuvixMarkdown opts = do
_processingStateStmtsSeparation = sepr,
_processingStateStmts = indModuleFilter $ m ^. Concrete.moduleBody
}
- (_, r) <- runState st . runReader htmlOptions . runReader opts $ go
+ (_, r) <- runState st . runReader htmlOptions . runReader opts $ go fname
return $ MK.toPlainText r
Nothing ->
throw
@@ -104,34 +104,49 @@ go ::
( Members
'[ Reader HtmlRender.HtmlOptions,
Reader ProcessJuvixBlocksArgs,
- State ProcessingState
+ State ProcessingState,
+ Error MarkdownBackendError
]
r
) =>
+ Path Abs File ->
Sem r Mk
-go = do
+go fname = do
stmts <- gets @ProcessingState (^. processingStateStmts)
sepr <- gets @ProcessingState (^. processingStateStmtsSeparation)
mk <- gets @ProcessingState (^. processingStateMk)
- case (sepr, stmts) of
- ([], _) -> return mk
- ((n : ns), _) -> do
+ case sepr of
+ [] -> return mk
+ (n : ns) -> do
case mk of
MkNull -> return mk
MkTextBlock _ -> return mk
MkConcat l r -> do
modify (set processingStateMk l)
- lS <- go
+ lS <- go fname
modify (set processingStateMk r)
- MkConcat lS <$> go
+ MkConcat lS <$> go fname
MkJuvixCodeBlock j -> do
+ opts <- case parseJuvixBlockOptions fname (j ^. juvixCodeBlockOptions) of
+ Left e ->
+ throw
+ ( ErrInvalidCodeBlockAttribtues
+ (InvalidCodeBlockAttributesError e)
+ )
+ Right o -> return o
+
m <-
asks @ProcessJuvixBlocksArgs
(^. processJuvixBlocksArgsModule)
isFirstBlock <- gets @ProcessingState (^. processingStateFirstBlock)
- let stmts' = take n stmts
+ stmts' <-
+ let blockStmts = take n stmts
+ in case opts of
+ MkJuvixBlockOptionsExtractModule o ->
+ checkExtractModule j (o ^. juvixBlockOptionsExtractModuleDrop) blockStmts
+ _ -> return blockStmts
htmlStatements :: [Html] <-
mapM (\s -> goRender s <> pure htmlSemicolon) stmts'
@@ -153,15 +168,14 @@ go = do
Text.intercalate "\n\n" $
map (toStrict . Html.renderHtml) htmlStatements
- let _processingStateMk =
- if j ^. juvixCodeBlockOptions . mkJuvixBlockOptionsHide
- then MkNull
- else
- MkTextBlock
- TextBlock
- { _textBlock = Text.replace "\n" "
" resHtml,
- _textBlockInterval = j ^. juvixCodeBlockInterval
- }
+ let _processingStateMk = case opts of
+ MkJuvixBlockOptionsHide -> MkNull
+ _ ->
+ MkTextBlock
+ TextBlock
+ { _textBlock = Text.replace "\n" "
" resHtml,
+ _textBlockInterval = j ^. juvixCodeBlockInterval
+ }
let newState =
ProcessingState
{ _processingStateFirstBlock = False,
@@ -171,6 +185,20 @@ go = do
}
modify @ProcessingState $ const newState
return _processingStateMk
+ where
+ checkExtractModule :: JuvixCodeBlock -> Int -> [Concrete.Statement 'Concrete.Scoped] -> Sem r [Concrete.Statement 'Concrete.Scoped]
+ checkExtractModule j dropNum xs = case xs of
+ [Concrete.StatementModule m] -> do
+ return (drop dropNum (indModuleFilter (m ^. Concrete.moduleBody)))
+ _ ->
+ throw
+ ( ErrInvalidExtractModuleBlock
+ ( InvalidExtractModuleBlockError
+ { _invalidExtractModuleBlockErrorPath = fname,
+ _invalidExtractModuleBlockErrorInterval = j ^. juvixCodeBlockInterval
+ }
+ )
+ )
goRender ::
(Concrete.PrettyPrint c, Members '[Reader HtmlRender.HtmlOptions, Reader ProcessJuvixBlocksArgs] r) =>
diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs
index bd2267020..8e2fa0f1f 100644
--- a/src/Juvix/Parser/Error.hs
+++ b/src/Juvix/Parser/Error.hs
@@ -1,4 +1,8 @@
-module Juvix.Parser.Error where
+module Juvix.Parser.Error
+ ( module Juvix.Parser.Error,
+ module Juvix.Parser.Error.Base,
+ )
+where
import Commonmark qualified as MK
import Juvix.Compiler.Backend.Markdown.Error
@@ -7,9 +11,9 @@ import Juvix.Compiler.Concrete.Pretty.Options (fromGenericOptions)
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
import Juvix.Compiler.Pipeline.Loader.PathResolver.Error
import Juvix.Extra.Paths
+import Juvix.Parser.Error.Base
import Juvix.Prelude
import Text.Megaparsec qualified as M
-import Text.Megaparsec.Error (errorOffset)
import Text.Parsec.Error qualified as P
import Text.Parsec.Pos qualified as P
@@ -33,43 +37,6 @@ instance ToGenericError ParserError where
ErrDanglingJudoc e -> genericError e
ErrMarkdownBackend e -> genericError e
-instance Pretty MegaparsecError where
- pretty (MegaparsecError b) = pretty (M.errorBundlePretty b)
-
-instance HasLoc MegaparsecError where
- getLoc (MegaparsecError b) = singletonInterval (mkLoc offset sourcePos)
- where
- state :: M.PosState Text
- state = M.bundlePosState b
- offset = errorOffset (head (M.bundleErrors b))
-
- sourcePos :: M.SourcePos
- sourcePos =
- (snd . head . fst)
- (M.attachSourcePos errorOffset (M.bundleErrors b) state)
-
-newtype MegaparsecError = MegaparsecError
- { _megaParsecError :: M.ParseErrorBundle Text Void
- }
- deriving stock (Show)
-
-instance ToGenericError MegaparsecError where
- genericError e =
- return
- GenericError
- { _genericErrorLoc = i,
- _genericErrorMessage = mkAnsiText $ pretty @_ @AnsiStyle e,
- _genericErrorIntervals = [i]
- }
- where
- i = getLoc e
-
--- | Use only for debugging
-fromMegaParsecError :: Either MegaparsecError a -> a
-fromMegaParsecError = \case
- Left e -> error (prettyText e)
- Right a -> a
-
newtype CommonmarkError = CommonmarkError
{ _commonMarkError :: MK.ParseError
}
diff --git a/src/Juvix/Parser/Error/Base.hs b/src/Juvix/Parser/Error/Base.hs
new file mode 100644
index 000000000..1232dc2a2
--- /dev/null
+++ b/src/Juvix/Parser/Error/Base.hs
@@ -0,0 +1,43 @@
+module Juvix.Parser.Error.Base where
+
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+import Text.Megaparsec qualified as M
+import Text.Megaparsec.Error (errorOffset)
+
+instance Pretty MegaparsecError where
+ pretty (MegaparsecError b) = pretty (M.errorBundlePretty b)
+
+instance HasLoc MegaparsecError where
+ getLoc (MegaparsecError b) = singletonInterval (mkLoc offset sourcePos)
+ where
+ state :: M.PosState Text
+ state = M.bundlePosState b
+ offset = errorOffset (head (M.bundleErrors b))
+
+ sourcePos :: M.SourcePos
+ sourcePos =
+ (snd . head . fst)
+ (M.attachSourcePos errorOffset (M.bundleErrors b) state)
+
+newtype MegaparsecError = MegaparsecError
+ { _megaParsecError :: M.ParseErrorBundle Text Void
+ }
+ deriving stock (Show)
+
+instance ToGenericError MegaparsecError where
+ genericError e =
+ return
+ GenericError
+ { _genericErrorLoc = i,
+ _genericErrorMessage = mkAnsiText $ pretty @_ @AnsiStyle e,
+ _genericErrorIntervals = [i]
+ }
+ where
+ i = getLoc e
+
+-- | Use only for debugging
+fromMegaParsecError :: Either MegaparsecError a -> a
+fromMegaParsecError = \case
+ Left e -> error (prettyText e)
+ Right a -> a
diff --git a/test/BackendMarkdown/Negative.hs b/test/BackendMarkdown/Negative.hs
index 2617fb9d4..0cb4b9a47 100644
--- a/test/BackendMarkdown/Negative.hs
+++ b/test/BackendMarkdown/Negative.hs
@@ -2,6 +2,9 @@ module BackendMarkdown.Negative where
import Base
import Juvix.Compiler.Backend.Markdown.Error
+import Juvix.Compiler.Backend.Markdown.Translation.FromTyped.Source
+import Juvix.Compiler.Concrete qualified as Concrete
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
import Juvix.Parser.Error
type FailMsg = String
@@ -10,7 +13,7 @@ data NegTest = NegTest
{ _name :: String,
_relDir :: Path Rel Dir,
_file :: Path Rel File,
- _checkErr :: ParserError -> Maybe FailMsg
+ _checkErr :: JuvixError -> Maybe FailMsg
}
testDescr :: NegTest -> TestDescr
@@ -22,12 +25,33 @@ testDescr NegTest {..} =
_testRoot = tRoot,
_testAssertion = Single $ do
entryPoint <- testDefaultEntryPointIO tRoot file'
- result <- testTaggedLockedToIO (runIOEither entryPoint upToParsing)
- case mapLeft fromJuvixError result of
- Left (Just err) -> whenJust (_checkErr err) assertFailure
- Right _ -> assertFailure "Unexpected success."
- Left Nothing -> assertFailure "Unexpected error."
+ result <- testTaggedLockedToIO (runIOEither entryPoint upToScoping)
+ case result of
+ Left err -> whenJust (_checkErr err) assertFailure
+ Right (_, pipelineRes) -> checkResult pipelineRes
}
+ where
+ checkResult :: PipelineResult Scoper.ScoperResult -> IO ()
+ checkResult PipelineResult {..} = do
+ let m = _pipelineResult ^. Scoper.resultModule
+ opts =
+ ProcessJuvixBlocksArgs
+ { _processJuvixBlocksArgsConcreteOpts = Concrete.defaultOptions,
+ _processJuvixBlocksArgsUrlPrefix = "",
+ _processJuvixBlocksArgsIdPrefix = "",
+ _processJuvixBlocksArgsNoPath = True,
+ _processJuvixBlocksArgsExt = ".html",
+ _processJuvixBlocksArgsStripPrefix = "",
+ _processJuvixBlocksArgsComments = Comments mempty,
+ _processJuvixBlocksArgsFolderStructure = False,
+ _processJuvixBlocksArgsModule = m,
+ _processJuvixBlocksArgsOutputDir =
+ root $(mkRelDir "markdown")
+ }
+ res = fromJuvixMarkdown' opts
+ case res of
+ Left err -> whenJust (_checkErr (JuvixError err)) assertFailure
+ Right _ -> assertFailure "Unexpected success"
allTests :: TestTree
allTests =
@@ -38,8 +62,8 @@ allTests =
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/negative")
-wrongError :: Maybe FailMsg
-wrongError = Just "Incorrect error"
+wrongError :: JuvixError -> Maybe FailMsg
+wrongError e = Just ("unexpected error: " <> unpack (renderTextDefault e))
tests :: [NegTest]
tests =
@@ -47,14 +71,35 @@ tests =
"Empty file"
$(mkRelDir "Markdown")
$(mkRelFile "Empty.juvix.md")
- $ \case
- ErrMarkdownBackend (ErrNoJuvixCodeBlocks _) -> Nothing
- _ -> wrongError,
+ $ \e -> case fromJuvixError e of
+ Just (ErrMarkdownBackend (ErrNoJuvixCodeBlocks _)) -> Nothing
+ _ -> wrongError e,
NegTest
"No Juvix code blocks"
$(mkRelDir "Markdown")
$(mkRelFile "NoJuvixCodeBlocks.juvix.md")
- $ \case
- ErrMarkdownBackend (ErrNoJuvixCodeBlocks _) -> Nothing
- _ -> wrongError
+ $ \e -> case fromJuvixError e of
+ Just (ErrMarkdownBackend (ErrNoJuvixCodeBlocks _)) -> Nothing
+ _ -> wrongError e,
+ NegTest
+ "extract-module-statements with no local module"
+ $(mkRelDir "Markdown")
+ $(mkRelFile "InvalidExtractModuleBlockNoModule.juvix.md")
+ $ \e -> case fromJuvixError e of
+ Just (ErrInvalidExtractModuleBlock _) -> Nothing
+ _ -> wrongError e,
+ NegTest
+ "extract-module-statements with no local module"
+ $(mkRelDir "Markdown")
+ $(mkRelFile "InvalidExtractModuleBlockNotJustModule.juvix.md")
+ $ \e -> case fromJuvixError e of
+ Just (ErrInvalidExtractModuleBlock _) -> Nothing
+ _ -> wrongError e,
+ NegTest
+ "code block with both hide and extract-module-statements"
+ $(mkRelDir "Markdown")
+ $(mkRelFile "InvalidCodeBlockExtraAttribute.juvix.md")
+ $ \e -> case fromJuvixError e of
+ Just (ErrInvalidCodeBlockAttribtues _) -> Nothing
+ _ -> wrongError e
]
diff --git a/tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md b/tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md
new file mode 100644
index 000000000..056f7a359
--- /dev/null
+++ b/tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md
@@ -0,0 +1,9 @@
+# Title
+
+```juvix
+module InvalidExtractModuleBlockExtraAttribute;
+```
+
+```juvix hide extract-module-statements
+type T := t;
+```
diff --git a/tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md b/tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md
new file mode 100644
index 000000000..e091b3d25
--- /dev/null
+++ b/tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md
@@ -0,0 +1,9 @@
+# Title
+
+```juvix
+module InvalidExtractModuleBlockUnknownAttribute;
+```
+
+```juvix invalid-attribute
+type T := t;
+```
diff --git a/tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md b/tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md
new file mode 100644
index 000000000..bcb6b4142
--- /dev/null
+++ b/tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md
@@ -0,0 +1,9 @@
+# Title
+
+```juvix
+module InvalidExtractModuleBlockNoModule;
+```
+
+```juvix extract-module-statements
+type T := t;
+```
diff --git a/tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md b/tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md
new file mode 100644
index 000000000..a54edf9da
--- /dev/null
+++ b/tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md
@@ -0,0 +1,12 @@
+# Title
+
+```juvix
+module InvalidExtractModuleBlockNotJustModule;
+```
+
+```juvix extract-module-statements
+module Inner;
+ type T1 := t1;
+end;
+type T2 := t2;
+```
diff --git a/tests/positive/Markdown/Test.juvix.md b/tests/positive/Markdown/Test.juvix.md
index d9d76cb7c..7146c7971 100644
--- a/tests/positive/Markdown/Test.juvix.md
+++ b/tests/positive/Markdown/Test.juvix.md
@@ -22,6 +22,23 @@ fib : Nat → Nat → Nat → Nat
fibonacci (n : Nat) : Nat := fib n 0 1;
```
+The `extract-module-statements` attribute can be used to display only the statements contained in a module in the output.
+
+```juvix extract-module-statements
+module Foo1;
+ type T := t;
+end;
+```
+
+You can pass a number to the `extract-module-statements` attribute to drop that number of statements from the start of the module.
+
+```juvix extract-module-statements 1
+module Foo2;
+ type T := t;
+ a : T := t;
+end;
+```
+
Commands like `typecheck` and `compile` can be used with Juvix Markdown files.
```juvix
@@ -89,4 +106,4 @@ We also use other markup for documentation such as:
| n zero := n
| n (suc m) := suc (add n m);
end;
- ```
\ No newline at end of file
+ ```
diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md
index 0a45d0a79..50f1e7793 100644
--- a/tests/positive/Markdown/markdown/Test.md
+++ b/tests/positive/Markdown/markdown/Test.md
@@ -9,11 +9,19 @@ Certain blocks can be hidden from the output by adding the `hide` attribute, as
-fib : Nat → Nat → Nat → Nat
| zero x1 _ := x1
| (suc n) x1 x2 := fib n x2 (x1 + x2);
fibonacci (n : Nat) : Nat := fib n 0 1;
+fib : Nat → Nat → Nat → Nat
| zero x1 _ := x1
| (suc n) x1 x2 := fib n x2 (x1 + x2);
fibonacci (n : Nat) : Nat := fib n 0 1;
+
+The `extract-module-statements` attribute can be used to display only the statements contained in a module in the output.
+
+type T := t;
+
+You can pass a number to the `extract-module-statements` attribute to drop that number of statements from the start of the module.
+
+a : T := t;
Commands like `typecheck` and `compile` can be used with Juvix Markdown files.
-main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
+main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
Other code blocks are not touched, e.g:
@@ -57,8 +65,8 @@ We also use other markup for documentation such as:
Initial function arguments that match variables or wildcards in all clauses can
be moved to the left of the colon in the function definition. For example,
- module move-to-left;
import Stdlib.Data.Nat open;
add (n : Nat) : Nat -> Nat
| zero := n
| (suc m) := suc (add n m);
end;
+ module move-to-left;
import Stdlib.Data.Nat open;
add (n : Nat) : Nat -> Nat
| zero := n
| (suc m) := suc (add n m);
end;
is equivalent to
- module example-add;
import Stdlib.Data.Nat open;
add : Nat -> Nat -> Nat
| n zero := n
| n (suc m) := suc (add n m);
end;
+ module example-add;
import Stdlib.Data.Nat open;
add : Nat -> Nat -> Nat
| n zero := n
| n (suc m) := suc (add n m);
end;