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

Support extract-module-statements attribute in juvix code blocks #2734

Merged
merged 7 commits into from
Apr 18, 2024

Conversation

paulcadman
Copy link
Collaborator

@paulcadman paulcadman commented Apr 17, 2024

This PR adds support for the extract-module-statements attribute for Juvix code blocks:

So if you write something like the following block in a Juvix markdown file:

```juvix extract-module-statements
module Foo;
   type T := t;
end;
```

The statement type T := t; from the body of the module is rendered in the output. The module Foo; , and end; lines are not rendered in the output.

A block with the extract-module-statements must contain a single local module statement and nothing else. An error is reported if this is not the case.

The extract-module-statements attribute also takes an optional argument. It sets the number of statements from the module body to drop from the output.

In the following example, the output will contain the single line a : T := t;.

```juvix extract-module-statements 1
module Foo;
   type T := t;
   a : T  := t;
end;
```

@paulcadman paulcadman added this to the 0.6.2 milestone Apr 17, 2024
@paulcadman paulcadman self-assigned this Apr 17, 2024
@paulcadman paulcadman marked this pull request as draft April 17, 2024 14:20
@paulcadman paulcadman force-pushed the md-extract-module-statements branch from 737712c to 1b88f30 Compare April 17, 2024 18:19
@paulcadman paulcadman marked this pull request as ready for review April 17, 2024 18:51
@paulcadman paulcadman force-pushed the md-extract-module-statements branch from bf49657 to b21d592 Compare April 17, 2024 18:52
@janmasrovira janmasrovira self-requested a review April 18, 2024 09:02
@janmasrovira janmasrovira force-pushed the md-extract-module-statements branch from 119f780 to 39e0e48 Compare April 18, 2024 13:01
@paulcadman paulcadman merged commit 52a3eed into main Apr 18, 2024
4 checks passed
@paulcadman paulcadman deleted the md-extract-module-statements branch April 18, 2024 16:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants