Skip to content

Commit

Permalink
Use <br/> instead of \n for right md cblock formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
@jonaprieto
jonaprieto committed Nov 24, 2023
1 parent 5f1067b commit 56e575e
Show file tree
Hide file tree
Showing 4 changed files with 46 additions and 15 deletions.
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Backend/Markdown/Data/Types.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
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
31 changes: 27 additions & 4 deletions tests/positive/Markdown/Test.juvix.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
```juvix
module example-add;
import Stdlib.Data.Nat open;
add : Nat -> Nat -> Nat
| n zero := n
| n (suc m) := suc (add n m);
end;
```
23 changes: 14 additions & 9 deletions tests/positive/Markdown/markdown/Test.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

<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="Y744"><span class="annot"><a href="X#Y744"><span class="annot"><a href="X#Y744"><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#Y744"><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="Y745"><span class="annot"><a href="X#Y745"><span class="annot"><a href="X#Y745"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="Y746"><span class="annot"><a href="X#Y746"><span class="annot"><a href="X#Y746"><span class="ju-var">x1</span></a></span></a></span></span> <span id="Y747"><span class="annot"><a href="X#Y747"><span class="annot"><a href="X#Y747"><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#Y745"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y747"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#Y746"><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#Y747"><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#Y748"><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#Y748"><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.

Expand Down Expand Up @@ -54,6 +49,16 @@ We also use other markup for documentation such as:
f {n : Nat := 0} {m : Nat := n + 1} ....
```

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">axiom</span> <span id="Y743"><span class="annot"><a href="X#Y743"><span class="annot"><a href="X#Y743"><span class="ju-axiom">AA</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="ju-keyword">Type</span><span class="ju-delimiter">;</span></pre></code></pre>

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,

<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 56e575e

Please sign in to comment.