Skip to content

Commit

Permalink
Fix codeblocks indentation in Markdown output (#2539)
Browse files Browse the repository at this point in the history 
- Closes #2528
- Closes anoma/juvix-docs#95

After this PR is merged, this will fix the misbehaving of code blocks
within !!!/??? Environments spotted in
anoma/juvix-docs#95. The result would be
as expected:

Already deployed, e.g. https://docs.juvix.org/0.5.4/tutorials/learn/

![screencapture-localhost-8000-reference-language-functions-2023-11-24-21_28_39](https://github.com/anoma/juvix/assets/1428088/85877b1a-0428-40b2-b900-147b3f386e8c)
  • Loading branch information
@jonaprieto
jonaprieto authored Nov 27, 2023
1 parent d8027fc commit 628dd23
Show file tree
Hide file tree
Showing 4 changed files with 120 additions and 11 deletions.
4 changes: 2 additions & 2 deletions src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ instance MK.ToPlainText Mk where
builder :: Mk -> [Text]
builder = \case
MkConcat a b -> builder a <> builder b
MkTextBlock t -> [trimText (t ^. textBlock) <> nl]
MkTextBlock t -> [t ^. textBlock]
MkJuvixCodeBlock j -> [textJuvixCodeBlock j]
MkNull -> mempty

Expand Down Expand Up @@ -209,7 +209,7 @@ processCodeBlock info t loc =
_juvixCodeBlockInterval = loc
}
_ ->
let b = "```" <> info <> nl <> t <> "```"
let b = "```" <> info <> t <> "```"
in MkTextBlock TextBlock {_textBlock = b, _textBlockInterval = loc}

instance-- (MK.IsInline TextBlock) =>
Expand Down
5 changes: 4 additions & 1 deletion src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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" "<br/>" $
resHtml,
_textBlockInterval = j ^. juvixCodeBlockInterval
}
let newState =
Expand Down
66 changes: 64 additions & 2 deletions tests/positive/Markdown/Test.juvix.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ module Test;

Certain blocks can be hidden from the output by adding the `hide` attribute, as shown below.


```juvix hide
import Stdlib.Prelude open;
```
Expand All @@ -27,4 +26,67 @@ Commands like `typecheck` and `compile` can be used with Juvix Markdown files.

```juvix
main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
```
```

Other code blocks are not touched, e.g:

```text
This is a text block
```


```haskell
module Test where
```

Blocks indented.

```haskell
module Test where
```

Empty blocks:

```
```
We also use other markup for documentation such as:
!!! note
We use this kind of markup for notes, solutions, and other stuff
1. More text
```text
f {n : Nat := 0} {m : Nat := n + 1} ....
```

2. Second text


??? info "Solution"

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

```juvix
module example-add;
import Stdlib.Data.Nat open;
add : Nat -> Nat -> Nat
| n zero := n
| n (suc m) := suc (add n m);
end;
```
56 changes: 50 additions & 6 deletions tests/positive/Markdown/markdown/Test.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,18 +3,62 @@
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.

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y0"><span class="annot"><a href="X#Y0"><span class="annot"><a href="X#Y0"><span class="ju-var">Test</span></a></span></a></span></span><span class="ju-delimiter">;</span>
</pre></code></pre>
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y0"><span class="annot"><a href="X#Y0"><span class="annot"><a href="X#Y0"><span class="ju-var">Test</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/></pre></code></pre>

Certain blocks can be hidden from the output by adding the `hide` attribute, as shown below.


<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y740"><span class="annot"><a href="X#Y740"><span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span>
<span class="ju-keyword">|</span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span id="Y743"><span class="annot"><a href="X#Y743"><span class="annot"><a href="X#Y743"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y743"><span class="ju-var">x1</span></a></span>
<span class="ju-keyword">|</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y744"><span class="annot"><a href="X#Y744"><span class="annot"><a href="X#Y744"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="Y745"><span class="annot"><a href="X#Y745"><span class="annot"><a href="X#Y745"><span class="ju-var">x1</span></a></span></a></span></span> <span id="Y746"><span class="annot"><a href="X#Y746"><span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y744"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#Y745"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#Y510"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span>

<span id="Y741"><span class="annot"><a href="X#Y741"><span class="annot"><a href="X#Y741"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y747"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y747"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y740"><span class="annot"><a href="X#Y740"><span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span id="Y743"><span class="annot"><a href="X#Y743"><span class="annot"><a href="X#Y743"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y743"><span class="ju-var">x1</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y744"><span class="annot"><a href="X#Y744"><span class="annot"><a href="X#Y744"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="Y745"><span class="annot"><a href="X#Y745"><span class="annot"><a href="X#Y745"><span class="ju-var">x1</span></a></span></a></span></span> <span id="Y746"><span class="annot"><a href="X#Y746"><span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y744"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#Y745"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#Y510"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="Y741"><span class="annot"><a href="X#Y741"><span class="annot"><a href="X#Y741"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y747"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y747"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>

Commands like `typecheck` and `compile` can be used with Juvix Markdown files.

<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y742"><span class="annot"><a href="X#Y742"><span class="annot"><a href="X#Y742"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y714"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y719"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#Y727"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#Y188"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#Y741"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#Y188"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#Y551"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>

Other code blocks are not touched, e.g:

```text
This is a text block
```


```haskell
module Test where
```

Blocks indented.

```haskell
module Test where
```

Empty blocks:

```
```
We also use other markup for documentation such as:
!!! note
We use this kind of markup for notes, solutions, and other stuff
1. More text
```text
f {n : Nat := 0} {m : Nat := n + 1} ....
```

2. Second text


??? info "Solution"

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,

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y751"><span class="annot"><a href="X#Y751"><span class="annot"><a href="X#Y751"><span class="ju-var">move-to-left</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span class="annot"><a href="X#Y506"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="Y748"><span class="annot"><a href="X#Y748"><span class="annot"><a href="X#Y748"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y749"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y749"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y750"><span class="annot"><a href="X#Y750"><span class="annot"><a href="X#Y750"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#Y748"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#Y749"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y750"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>

is equivalent to

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y756"><span class="annot"><a href="X#Y756"><span class="annot"><a href="X#Y756"><span class="ju-var">example-add</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span class="annot"><a href="X#Y506"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="Y752"><span class="annot"><a href="X#Y752"><span class="annot"><a href="X#Y752"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span id="Y753"><span class="annot"><a href="X#Y753"><span class="annot"><a href="X#Y753"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y753"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span id="Y754"><span class="annot"><a href="X#Y754"><span class="annot"><a href="X#Y754"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y755"><span class="annot"><a href="X#Y755"><span class="annot"><a href="X#Y755"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#Y752"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#Y754"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y755"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>

0 comments on commit 628dd23

Please sign in to comment.