Skip to content

Conversation

mgritter
Copy link

@mgritter mgritter commented Nov 7, 2021

This PR refreshes the standard library documentation using fstardoc.

Instead of using pandoc (and writing a syntax highlighting grammar in the format it understands) my revised script uses the GitHub service to render markdown -> html, so we get the syntax highlighting that GitHub performs.

The script used to generate this is a work in progress at
https://github.com/mgritter/FStar/blob/mgritter/script_html_conversion/.scripts/fstardoc/generate-ulib.py

Additions:

  • Index page includes the first sentence in the module documentation, if it can be found.
  • Instead of showing the code for open or module X = Y or include, the document translates those dependencies into a bulleted list with hyperlinks.
  • Language annotation on code blocks is FStar not fstar

Diffs to fstardoc can be seen here: FStarLang/FStar@master...mgritter:mgritter/script_html_conversion

@ghost
Copy link

ghost commented Nov 7, 2021

CLA assistant check
All CLA requirements met.

@mgritter
Copy link
Author

mgritter commented Nov 7, 2021

I broke the CSS for syntax highlighting... will fix.

@mgritter mgritter marked this pull request as draft November 7, 2021 23:18
@mgritter mgritter marked this pull request as ready for review November 8, 2021 00:11
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.

1 participant