Physlib.Meta.Notes.ToHTML
11 declarations
Ordering of `HTMLNote` by file index and line number
#sortLEThe function `Physlib.NoteFile.sortLE` defines a "less than or equal to" comparison between two `HTMLNote` objects, and . The comparison first checks the indices of the file names of the notes within a list . If the file names are different, the result is true if the index of the file name of is less than or equal to the index of the file name of . If the file names are the same, the function returns true if the line number of is less than or equal to the line number of .
Sorted list of objects for files in
#getNodeInfoThis function, operating within the `CoreM` monad, retrieves and aggregates a list of `HTMLNote` objects from the environment. It collects data from three sources: standard notes (from `noteExtension`), formal declarations (from `noteDeclExtension`), and informal declarations (from `noteInformalDeclExtension`), converting them into `HTMLNote` structures using `ofNodeInfo`, `ofFormal`, and `ofInformal` respectively. The resulting list is filtered to include only those notes whose file path is contained in the list . Finally, the function returns this list sorted according to the ordering relation , which compares notes based on their file index and line number.
HTML code for Lean syntax highlighting
#codeBlockHTMLThe constant `Physlib.NoteFile.codeBlockHTML` is a string containing the HTML header elements and JavaScript configuration required to enable syntax highlighting for code blocks in generated documentation. It includes metadata for character encoding and responsive design, imports the `highlight.js` library and its default CSS, and registers a custom language definition for Lean. This custom definition identifies specific keywords such as `def`, `theorem`, `axiomatic`, `structure`, and `lemma`, and provides regex-based rules for identifying comments and mathematical operators.
CSS styling for informal definitions
#informalDefStyleThe constant `Physlib.NoteFile.informalDefStyle` is a string containing the CSS (Cascading Style Sheets) code used to define the visual styling for informal definitions in HTML documentation. It specifies properties for the `.informal-def` class, including a light red background (), a solid dark red border (), and relative positioning. It also defines the appearance of buttons within these blocks, including their absolute positioning, transparency (), and a hover state that changes the background color to blue ().
CSS styling for HTML code buttons
#codeButtonThe constant `Physlib.NoteFile.codeButton` is a string containing the CSS (Cascading Style Sheets) code used to define the visual appearance and layout of buttons within code blocks in HTML documentation. It specifies properties for the `.code-button` class, such as its absolute positioning, a semi-transparent red background (), white text color, and a blue background transition upon hovering.
HTML script for MathJax configuration and loading
#mathJaxScriptThe constant `Physlib.NoteFile.mathJaxScript` is a string containing the HTML `<script>` tags used to configure and load the MathJax library. It specifies that LaTeX mathematical expressions should be delimited by `$` for display math, and it loads the MathJax 3 engine from a content delivery network (CDN) to ensure proper rendering of mathematical notation in HTML documents.
HTML header for documentation files
#headerHTMLThe constant `Physlib.NoteFile.headerHTML` is a string that defines the initial HTML structure and metadata for generated documentation files. It contains a YAML front matter block specifying a default layout, followed by the opening `<html>` and `<head>` tags. The header section includes concatenated strings for Lean syntax highlighting (`codeBlockHTML`), MathJax configuration for rendering mathematical expressions (`mathJaxScript`), and CSS styles for informal definitions (`informalDefStyle`) and interactive buttons (`codeButton`). The string concludes by closing the `<head>` section and opening the `<body>` tag.
HTML snippet for title, authors, and abstract
#titleHTMLThe function `Physlib.NoteFile.titleHTML` generates an HTML string to display the metadata of a note . It formats the title within a centered level-1 heading with a font size of , followed by a centered list of authors separated by commas, and a centered block containing the abstract .
HTML snippet for the Lean and Physlib informational note
#leanNoteThe constant `leanNote` is a string containing HTML code intended to display a standardized informational notice. This notice informs the reader that the document was created using the Lean interactive theorem prover to formally verify mathematical and physical content. It further identifies the work as part of the Physlib project for the digitalization of high energy physics and provides hyperlinks for community contribution and feedback via GitHub.
HTML string generation for a `NoteFile`
#toHTMLStringThis function, operating within the `MetaM` monad, constructs a complete HTML document as a string for a given `NoteFile` . It retrieves a list of `HTMLNote` objects associated with using `getNodeInfo`, extracts their content strings, and joins them together with newline characters. The final output is formed by concatenating the following components in order: the standard HTML header `headerHTML`, the formatted title and metadata , the project-specific `leanNote` snippet, the joined content strings from the retrieved notes, and the HTML footer `footerHTML`.