From 56e575e82a98cde697919e0c3faeb0a56b25f940 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 24 Nov 2023 21:45:08 +0100 Subject: [PATCH] Use
instead of \n for right md cblock formatting --- .../Compiler/Backend/Markdown/Data/Types.hs | 2 +- .../Markdown/Translation/FromTyped/Source.hs | 5 ++- tests/positive/Markdown/Test.juvix.md | 31 ++++++++++++++++--- tests/positive/Markdown/markdown/Test.md | 23 ++++++++------ 4 files changed, 46 insertions(+), 15 deletions(-) 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;