From ecae7e224aec567f04dc8e0398af79f55d1d6464 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 24 Nov 2023 19:52:04 +0100 Subject: [PATCH 1/4] Fix --- .../Compiler/Backend/Markdown/Data/Types.hs | 7 +-- tests/positive/Markdown/Test.juvix.md | 43 +++++++++++++++++- tests/positive/Markdown/markdown/Test.md | 45 +++++++++++++++++-- 3 files changed, 87 insertions(+), 8 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs index 2e3341641b..77d4a943f2 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs @@ -1,6 +1,7 @@ module Juvix.Compiler.Backend.Markdown.Data.Types where import Commonmark qualified as MK +import Data.List.NonEmpty qualified as NonEmpty import Data.Text qualified as T import Juvix.Data.Loc import Juvix.Prelude hiding (Raw) @@ -123,7 +124,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 @@ -209,12 +210,12 @@ 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) => MK.IsBlock TextBlock Mk where - paragraph a = MkTextBlock a + paragraph a = MkTextBlock a <> nl' plain a = MkTextBlock a thematicBreak = toMK "---" blockQuote p = toMK "> " <> p diff --git a/tests/positive/Markdown/Test.juvix.md b/tests/positive/Markdown/Test.juvix.md index 138b11f0e4..06cdbf1ef8 100644 --- a/tests/positive/Markdown/Test.juvix.md +++ b/tests/positive/Markdown/Test.juvix.md @@ -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; ``` @@ -27,4 +26,44 @@ Commands like `typecheck` and `compile` can be used with Juvix Markdown files. ```juvix main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat); -``` \ No newline at end of file +``` + +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} .... + ``` + + ```juvix + axiom AA : Type + ``` + + 2. Second text \ No newline at end of file diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md index c9728e9475..07e8e24ec5 100644 --- a/tests/positive/Markdown/markdown/Test.md +++ b/tests/positive/Markdown/markdown/Test.md @@ -9,12 +9,51 @@ a module declaration at the top, as shown below ---in the first code block. 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);
+  | zero x1 _ := x1
+  | (suc n) x1 x2 := fib n x2 (x1 + x2);
 
-fibonacci (n : Nat) : Nat := fib n 0 1;
+fibonacci (n : Nat) : Nat := fib n 0 1; Commands like `typecheck` and `compile` can be used with Juvix Markdown files. 
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} .... + ``` + + 
axiom AA : Type;
+ + 2. Second text From cb879464610650302229994fd58a1b0329d547fe Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 24 Nov 2023 20:01:12 +0100 Subject: [PATCH 2/4] remove unnecessary import --- src/Juvix/Compiler/Backend/Markdown/Data/Types.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs index 77d4a943f2..e7523d0036 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs @@ -1,7 +1,6 @@ module Juvix.Compiler.Backend.Markdown.Data.Types where import Commonmark qualified as MK -import Data.List.NonEmpty qualified as NonEmpty import Data.Text qualified as T import Juvix.Data.Loc import Juvix.Prelude hiding (Raw) From c469f89c0fd749a256dc35ab9fa6659c94d2533e Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 24 Nov 2023 21:45:08 +0100 Subject: [PATCH 3/4] 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;
From ae7d12a02e83e0f1ace34c6e86795334f35b6e04 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Fri, 24 Nov 2023 21:52:58 +0100 Subject: [PATCH 4/4] Use ??? info sol in the test.md --- tests/positive/Markdown/Test.juvix.md | 2 +- tests/positive/Markdown/markdown/Test.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/positive/Markdown/Test.juvix.md b/tests/positive/Markdown/Test.juvix.md index 0e9b7de7ac..d9d76cb7c7 100644 --- a/tests/positive/Markdown/Test.juvix.md +++ b/tests/positive/Markdown/Test.juvix.md @@ -65,7 +65,7 @@ We also use other markup for documentation such as: 2. Second text -!!! info +??? 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, diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md index ecf693589b..a803ebfec1 100644 --- a/tests/positive/Markdown/markdown/Test.md +++ b/tests/positive/Markdown/markdown/Test.md @@ -52,7 +52,7 @@ We also use other markup for documentation such as: 2. Second text -!!! info +??? 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,