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

Add TopDef property for specs #3223

Merged
merged 2 commits into from
Dec 6, 2024
Merged

Add TopDef property for specs #3223

merged 2 commits into from
Dec 6, 2024

Conversation

janmasrovira
Copy link
Collaborator

@janmasrovira janmasrovira commented Dec 3, 2024

This pr implements a request for the Specs team by @jonaprieto.

juvix dev highlight --format json now also outputs an additional field topDef that contains a list of pairs containing a file interval (with the usual encoding) and an identifier.
e.g

[["/home/jan/projects/juvix/juvix-stdlib/Stdlib/Extra/Gcd.juvix",10,1,4,10,4],"gcd"]

@janmasrovira janmasrovira self-assigned this Dec 3, 2024
@janmasrovira janmasrovira changed the title Add TopDef property for vscode Add TopDef property for specs Dec 4, 2024
@jonaprieto
Copy link
Collaborator

In the specs, we are writing textual documents that require referencing Juvix terms. However, there is no way to easily link these terms, as the anchors generated by compiler are numbers.
After this PR, I plan to implement another case for the WikiLinks preprocessor for the mkdocs juvix plugin, so it can replace automatically these references. The candidate syntax may just prefix the term identifier with juvix: [[juvix:MyTerm]].

@jonaprieto jonaprieto added enhancement New feature or request CLI dev-tools labels Dec 4, 2024
@jonaprieto jonaprieto added this to the 0.6.9 milestone Dec 4, 2024
Copy link
Collaborator

@jonaprieto jonaprieto left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Although, you may want to add a smoke test of a minimal example and check that some expected term identifier appears in the JSON file.

@janmasrovira janmasrovira marked this pull request as ready for review December 4, 2024 10:51
@lukaszcz lukaszcz force-pushed the add-topdef-property branch from 80a3643 to 83e7657 Compare December 5, 2024 08:10
@janmasrovira janmasrovira force-pushed the add-topdef-property branch 2 times, most recently from 97e0817 to 15f1d16 Compare December 6, 2024 08:30
@lukaszcz lukaszcz force-pushed the add-topdef-property branch from ba58b62 to 012548e Compare December 6, 2024 11:27
@lukaszcz lukaszcz merged commit 69c629b into main Dec 6, 2024
4 checks passed
@lukaszcz lukaszcz deleted the add-topdef-property branch December 6, 2024 14:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CLI dev-tools enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants