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

Basic citation support #69

Merged
merged 2 commits into from May 9, 2022
Merged

Basic citation support #69

merged 2 commits into from May 9, 2022

Conversation

SquidDev
Copy link
Collaborator

@SquidDev SquidDev commented May 9, 2022

Closes #68. See the notes in the commit message for actual implementation details.

Rendered view:

"A screenshot of the 1Lab.intro page, with a "References" block

CC @plt-amy and @TOTBWF - don't know if you have opinions on citation styles?

It might also be nice to move our :target highlight class to apply to all links, so people know which reference they're looking at.

 - Convert git authors to an oracle cache. When you need to rebuild a
   lot of pages, this can get quite slow, so useful to save between
   runs.
 - Add a bibliography to the source tree (with a single citation in) and
   get Pandoc to read that.
 - Do some massaging to the parsed Markdown/HTML to put the references
   block at the very end of the page (after footnotes). Also patch up
   citation links to include the paper's title:

     [Steele 2017](#ref-Steele2017)

   becomes

     [Steele 2017](#ref-Steele2017 "It’s Time for a New Old Language")

Closes #68
src/1Lab/intro.lagda.md Outdated Show resolved Hide resolved
Copy link
Owner

@plt-amy plt-amy left a comment

Choose a reason for hiding this comment

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

Tiny tiny quibble

support/shake/app/Main.hs Outdated Show resolved Hide resolved
Basically try to parse our references from the tree Pandoc produces
(it's gross, I know, but otherwise we need to copy a lot of Pandoc's
internal logic) and then emit them within the template itself.
Copy link
Owner

@plt-amy plt-amy left a comment

Choose a reason for hiding this comment

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

Nice, but also, yikes.

@plt-amy plt-amy merged commit 8fd4400 into main May 9, 2022
@SquidDev
Copy link
Collaborator Author

SquidDev commented May 9, 2022

yikes

Yikes indeed

@SquidDev SquidDev deleted the feature/citations branch May 9, 2022 18:25
@TOTBWF
Copy link
Collaborator

TOTBWF commented May 9, 2022

Awesome, thank you so much ❤️

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Citations
3 participants