diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
index e7523d0036..6ed14f4237 100644
--- a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
+++ b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
@@ -214,7 +214,7 @@ processCodeBlock info t loc =
instance-- (MK.IsInline TextBlock) =>
MK.IsBlock TextBlock Mk where
- paragraph a = MkTextBlock a <> nl'
+ paragraph a = MkTextBlock a
plain a = MkTextBlock a
thematicBreak = toMK "---"
blockQuote p = toMK "> " <> p
diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
index d8c1d9af41..d7c4d05d7b 100644
--- a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
+++ b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
@@ -146,13 +146,16 @@ go = do
Html.preEscapedText $
Text.intercalate "\n\n" $
map (toStrict . Html.renderHtml) htmlStatements
+
let _processingStateMk =
if j ^. juvixCodeBlockOptions . mkJuvixBlockOptionsHide
then MkNull
else
MkTextBlock
TextBlock
- { _textBlock = resHtml,
+ { _textBlock =
+ Text.replace "\n" "
" $
+ resHtml,
_textBlockInterval = j ^. juvixCodeBlockInterval
}
let newState =
diff --git a/tests/positive/Markdown/Test.juvix.md b/tests/positive/Markdown/Test.juvix.md
index 06cdbf1ef8..0e9b7de7ac 100644
--- a/tests/positive/Markdown/Test.juvix.md
+++ b/tests/positive/Markdown/Test.juvix.md
@@ -62,8 +62,31 @@ We also use other markup for documentation such as:
f {n : Nat := 0} {m : Nat := n + 1} ....
```
- ```juvix
- axiom AA : Type
- ```
+ 2. Second text
+
+
+!!! info
+
+ 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,
+
+ ```juvix
+ 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
- 2. Second text
\ No newline at end of file
+ ```juvix
+ module example-add;
+ import Stdlib.Data.Nat open;
+ add : Nat -> Nat -> Nat
+ | 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 07e8e24ec5..ecf693589b 100644
--- a/tests/positive/Markdown/markdown/Test.md
+++ b/tests/positive/Markdown/markdown/Test.md
@@ -3,18 +3,13 @@
A Juvix Markdown file name ends with `.juvix.md`. This kind of file must contain
a module declaration at the top, as shown below ---in the first code block.
-module Test;
-
+module Test;
Certain blocks can be hidden from the output by adding the `hide` attribute, as shown below.
-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;
Commands like `typecheck` and `compile` can be used with Juvix Markdown files.
@@ -54,6 +49,16 @@ We also use other markup for documentation such as:
f {n : Nat := 0} {m : Nat := n + 1} ....
```
- axiom AA : Type;
-
2. Second text
+
+
+!!! info
+
+ 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;
+
+ 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;