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.

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

Export Juvix source code to latex #2917

Merged
merged 22 commits into from
Aug 5, 2024
Merged

Export Juvix source code to latex #2917

merged 22 commits into from
Aug 5, 2024

Conversation

janmasrovira
Copy link
Collaborator

@janmasrovira janmasrovira commented Jul 26, 2024

This pr adds two new commands related to latex.

  1. juvix dev latex getJuvixSty. This command prints the contents of the juvix.sty latex package to stdout. It has no options and the expected usage is juvix dev latex getJuvixSty > juvix.sty.
  2. juvix dev latex export. Expects a .juvix file as an argument and outputs to stdout the highlighted module in latex format. Optional flags --from LINE, --to LINE to output only the specified line range. There is a --mode flag to choose how you want the output.
    • standalone: Output a ready to compile LaTeX file
    • wrap: Wrap the code in a Verbatim environment
    • raw: Output only the code (default: standalone)
    
  3. As shown in the standalone output, one is allowed to choose the theme when importing the juvix package like this: \usepackage[theme = latte]{juvix}. Available themes are latte, frappe, macchiato, mocha.

Examples:
To generate the following output I ran these commands:

cd examples/milestones/HelloWorld
mkdir latex
juvix dev latex getJuvixSty > latex/juvix.sty
juvix dev latex export HelloWorld.juvix > latex/main.tex
cd latex
xelatex main.tex
open main.pdf
  1. with \usepackage[theme = latte]{juvix}:
    image
  2. with \usepackage[theme = frappe]{juvix}:
    image
  3. with \usepackage[theme = macchiato]{juvix}:
    image
  4. with \usepackage[theme = mocha]{juvix}:
    image

@janmasrovira janmasrovira added enhancement New feature or request backend:latex labels Jul 26, 2024
@janmasrovira janmasrovira self-assigned this Jul 26, 2024
@janmasrovira janmasrovira force-pushed the latex branch 8 times, most recently from c38392a to f81fd01 Compare August 2, 2024 10:35
@janmasrovira janmasrovira marked this pull request as ready for review August 2, 2024 10:35
@janmasrovira janmasrovira requested a review from paulcadman August 2, 2024 11:15
@paulcadman paulcadman added this to the 0.6.5 milestone Aug 2, 2024
paulcadman
paulcadman previously approved these changes Aug 2, 2024
@janmasrovira janmasrovira merged commit bad61a7 into main Aug 5, 2024
4 checks passed
@janmasrovira janmasrovira deleted the latex branch August 5, 2024 09:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend:latex enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants