Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Syntax coloring in the documentation #1719

Closed
lukaszcz opened this issue Jan 12, 2023 · 0 comments · Fixed by #2448
Closed

Syntax coloring in the documentation #1719

lukaszcz opened this issue Jan 12, 2023 · 0 comments · Fixed by #2448
Assignees
@janmasrovira
Labels
documentation Improvements or additions to documentation enhancement New feature or request judoc Juvix documentation generation priority:low
Milestone
0.5.4

Comments

@lukaszcz
Copy link
Collaborator

It should be possible to configure mdbook somehow so that Juvix code can be written in the documentation and correctly highlighted
@lukaszcz lukaszcz added enhancement New feature or request documentation Improvements or additions to documentation pending-review labels Jan 12, 2023
@janmasrovira janmasrovira added the judoc Juvix documentation generation label Jan 12, 2023
@lukaszcz lukaszcz added this to the 0.5 milestone Jan 24, 2023
@janmasrovira janmasrovira mentioned this issue Feb 27, 2023
Closed
@lukaszcz lukaszcz modified the milestones: 0.5.0, 0.5.2 Sep 15, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.2, 0.5.3 Oct 2, 2023
@jonaprieto jonaprieto modified the milestones: 0.5.3, 0.5.4 Oct 31, 2023
@jonaprieto jonaprieto mentioned this issue Nov 3, 2023
Merged
jonaprieto added a commit that referenced this issue Nov 10, 2023
@jonaprieto
Add support for Literate Juvix Markdown (#2448)
bd16d3e 
This PR adds an initial support for Literate Juvix Markdown files, files
with the extension `.juvix.md`.

Here is a small example of such a file: `Test.juvix.md`.

<pre>
# This is a heading
Lorem ...

```juvix
module Test;

type A := a;

fun : A -> A 
 | _ := a;
```
Other text
</pre>


This initial support enables users to execute common commands such as
typechecking, compilation, and HTML generation. Additionally, a new
command called `markdown` has been introduced. This command replaces
code blocks marked with the juvix attribute with their respective HTML
output, much like the output we obtain when running `juvix html`. In
this version, comments are ignored in the output, including judoc
blocks.

- We intend to use this new feature in combination with this Python
plugin (https://github.com/anoma/juvix-mkdocs) to enhance our
documentation site.



https://github.com/anoma/juvix/assets/1428088/a0c17f36-3d76-42cc-a571-91f885866874


## Future work

Open as issues once this PR is merged, we can work on the following:

- Support imports of Juvix Markdown modules (update the path resolver to
support imports of Literate Markdown files)
- Support (Judoc) comments in md Juvix blocks
- Support Markdown in Judoc blocks
- Update Text editor support, vscode extension and emacs mode (the
highlighting info is a few characters off in the current state)



- Closes #1839 
- Closes #1719
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@janmasrovira janmasrovira

Labels
documentation Improvements or additions to documentation enhancement New feature or request judoc Juvix documentation generation priority:low
Projects
None yet
Milestone
0.5.4
Development

Successfully merging a pull request may close this issue.

Add support for Literate Juvix Markdown anoma/juvix
Add juvix org command anoma/juvix
3 participants
@lukaszcz @jonaprieto @janmasrovira