This repository was archived by the owner on Nov 2, 2023. It is now read-only.
-
-
Notifications
You must be signed in to change notification settings - Fork 214
Add a Glossary page with 2 initial entries. #461
Merged
Changes from all commits
Commits
Show all changes
5 commits
Select commit
Hold shift + click to select a range
d19bf52
Add a Glossary page with 2 initial entries.
Julian fee524d
Add the proper header for the glossary markdown file.
Julian 4e0d93b
Add a solicitation for further glossary entries.
Julian 77d5a40
Try including anchor headings via allejo/jekyll-anchor-headings.
Julian 7f57b0f
H4 for see also, as our H5 is smaller than Lean's.
Julian File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,172 @@ | ||
{% capture headingsWorkspace %} | ||
{% comment %} | ||
Copyright (c) 2018 Vladimir "allejo" Jimenez | ||
|
||
Permission is hereby granted, free of charge, to any person | ||
obtaining a copy of this software and associated documentation | ||
files (the "Software"), to deal in the Software without | ||
restriction, including without limitation the rights to use, | ||
copy, modify, merge, publish, distribute, sublicense, and/or sell | ||
copies of the Software, and to permit persons to whom the | ||
Software is furnished to do so, subject to the following | ||
conditions: | ||
|
||
The above copyright notice and this permission notice shall be | ||
included in all copies or substantial portions of the Software. | ||
|
||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, | ||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES | ||
OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND | ||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT | ||
HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, | ||
WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING | ||
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR | ||
OTHER DEALINGS IN THE SOFTWARE. | ||
{% endcomment %} | ||
{% comment %} | ||
Version 1.0.11 | ||
https://github.com/allejo/jekyll-anchor-headings | ||
|
||
"Be the pull request you wish to see in the world." ~Ben Balter | ||
|
||
Usage: | ||
{% include anchor_headings.html html=content anchorBody="#" %} | ||
|
||
Parameters: | ||
* html (string) - the HTML of compiled markdown generated by kramdown in Jekyll | ||
|
||
Optional Parameters: | ||
* beforeHeading (bool) : false - Set to true if the anchor should be placed _before_ the heading's content | ||
* headerAttrs (string) : '' - Any custom HTML attributes that will be added to the heading tag; you may NOT use `id`; | ||
the `%heading%` and `%html_id%` placeholders are available | ||
* anchorAttrs (string) : '' - Any custom HTML attributes that will be added to the `<a>` tag; you may NOT use `href`, `class` or `title`; | ||
the `%heading%` and `%html_id%` placeholders are available | ||
* anchorBody (string) : '' - The content that will be placed inside the anchor; the `%heading%` placeholder is available | ||
* anchorClass (string) : '' - The class(es) that will be used for each anchor. Separate multiple classes with a space | ||
* anchorTitle (string) : '' - The `title` attribute that will be used for anchors | ||
* h_min (int) : 1 - The minimum header level to build an anchor for; any header lower than this value will be ignored | ||
* h_max (int) : 6 - The maximum header level to build an anchor for; any header greater than this value will be ignored | ||
* bodyPrefix (string) : '' - Anything that should be inserted inside of the heading tag _before_ its anchor and content | ||
* bodySuffix (string) : '' - Anything that should be inserted inside of the heading tag _after_ its anchor and content | ||
* generateId (true) : false - Set to true if a header without id should generate an id to use. | ||
|
||
Output: | ||
The original HTML with the addition of anchors inside of all of the h1-h6 headings. | ||
{% endcomment %} | ||
|
||
{% assign minHeader = include.h_min | default: 1 %} | ||
{% assign maxHeader = include.h_max | default: 6 %} | ||
{% assign beforeHeading = include.beforeHeading %} | ||
{% assign headerAttrs = include.headerAttrs %} | ||
{% assign nodes = include.html | split: '<h' %} | ||
|
||
{% capture edited_headings %}{% endcapture %} | ||
|
||
{% for _node in nodes %} | ||
{% capture node %}{{ _node | strip }}{% endcapture %} | ||
|
||
{% if node == "" %} | ||
{% continue %} | ||
{% endif %} | ||
|
||
{% assign nextChar = node | replace: '"', '' | strip | slice: 0, 1 %} | ||
{% assign headerLevel = nextChar | times: 1 %} | ||
|
||
<!-- If the level is cast to 0, it means it's not a h1-h6 tag, so let's see if we need to fix it --> | ||
{% if headerLevel == 0 %} | ||
<!-- Split up the node based on closing angle brackets and get the first one. --> | ||
{% assign firstChunk = node | split: '>' | first %} | ||
|
||
<!-- If the first chunk does NOT contain a '<', that means we've broken another HTML tag that starts with 'h' --> | ||
{% unless firstChunk contains '<' %} | ||
{% capture node %}<h{{ node }}{% endcapture %} | ||
{% endunless %} | ||
|
||
{% capture edited_headings %}{{ edited_headings }}{{ node }}{% endcapture %} | ||
{% continue %} | ||
{% endif %} | ||
|
||
{% capture _closingTag %}</h{{ headerLevel }}>{% endcapture %} | ||
{% assign _workspace = node | split: _closingTag %} | ||
{% capture _hAttrToStrip %}{{ _workspace[0] | split: '>' | first }}>{% endcapture %} | ||
{% assign header = _workspace[0] | replace: _hAttrToStrip, '' %} | ||
{% assign escaped_header = header | strip_html | strip %} | ||
|
||
{% assign _classWorkspace = _workspace[0] | split: 'class="' %} | ||
{% assign _classWorkspace = _classWorkspace[1] | split: '"' %} | ||
{% assign _html_class = _classWorkspace[0] %} | ||
|
||
{% if _html_class contains "no_anchor" %} | ||
{% assign skip_anchor = true %} | ||
{% else %} | ||
{% assign skip_anchor = false %} | ||
{% endif %} | ||
|
||
{% assign _idWorkspace = _workspace[0] | split: 'id="' %} | ||
{% if _idWorkspace[1] %} | ||
{% assign _idWorkspace = _idWorkspace[1] | split: '"' %} | ||
{% assign html_id = _idWorkspace[0] %} | ||
{% elsif include.generateId %} | ||
<!-- If the header did not have an id we create one. --> | ||
{% assign html_id = escaped_header | slugify %} | ||
{% if html_id == "" %} | ||
{% assign html_id = false %} | ||
{% endif %} | ||
{% capture headerAttrs %}{{ headerAttrs }} id="%html_id%"{% endcapture %} | ||
{% endif %} | ||
|
||
<!-- Build the anchor to inject for our heading --> | ||
{% capture anchor %}{% endcapture %} | ||
|
||
{% if skip_anchor == false and html_id and headerLevel >= minHeader and headerLevel <= maxHeader %} | ||
{% if headerAttrs %} | ||
{% capture _hAttrToStrip %}{{ _hAttrToStrip | split: '>' | first }} {{ headerAttrs | replace: '%heading%', escaped_header | replace: '%html_id%', html_id }}>{% endcapture %} | ||
{% endif %} | ||
|
||
{% capture anchor %}href="#{{ html_id }}"{% endcapture %} | ||
|
||
{% if include.anchorClass %} | ||
{% capture anchor %}{{ anchor }} class="{{ include.anchorClass }}"{% endcapture %} | ||
{% endif %} | ||
|
||
{% if include.anchorTitle %} | ||
{% capture anchor %}{{ anchor }} title="{{ include.anchorTitle | replace: '%heading%', escaped_header }}"{% endcapture %} | ||
{% endif %} | ||
|
||
{% if include.anchorAttrs %} | ||
{% capture anchor %}{{ anchor }} {{ include.anchorAttrs | replace: '%heading%', escaped_header | replace: '%html_id%', html_id }}{% endcapture %} | ||
{% endif %} | ||
|
||
{% capture anchor %}<a {{ anchor }}>{{ include.anchorBody | replace: '%heading%', escaped_header | default: '' }}</a>{% endcapture %} | ||
|
||
<!-- In order to prevent adding extra space after a heading, we'll let the 'anchor' value contain it --> | ||
{% if beforeHeading %} | ||
{% capture anchor %}{{ anchor }} {% endcapture %} | ||
{% else %} | ||
{% capture anchor %} {{ anchor }}{% endcapture %} | ||
{% endif %} | ||
{% endif %} | ||
|
||
{% capture new_heading %} | ||
<h{{ _hAttrToStrip }} | ||
{{ include.bodyPrefix }} | ||
{% if beforeHeading %} | ||
{{ anchor }}{{ header }} | ||
{% else %} | ||
{{ header }}{{ anchor }} | ||
{% endif %} | ||
{{ include.bodySuffix }} | ||
</h{{ headerLevel }}> | ||
{% endcapture %} | ||
|
||
<!-- | ||
If we have content after the `</hX>` tag, then we'll want to append that here so we don't lost any content. | ||
--> | ||
{% assign chunkCount = _workspace | size %} | ||
{% if chunkCount > 1 %} | ||
{% capture new_heading %}{{ new_heading }}{{ _workspace | last }}{% endcapture %} | ||
{% endif %} | ||
|
||
{% capture edited_headings %}{{ edited_headings }}{{ new_heading }}{% endcapture %} | ||
{% endfor %} | ||
{% endcapture %}{% assign headingsWorkspace = '' %}{{ edited_headings | strip }} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
--- | ||
layout: page | ||
title: JSON Schema Glossary | ||
--- | ||
|
||
This document collects short explanations of terminology one may encounter within the JSON Schema community. | ||
|
||
Whilst many of the entries below have precise technical definitions, preference is given to explanations of their conversational use, with additional references linked for further information. | ||
This page is not meant to be [normative](#normative), nor is it meant to contain fully original research or explanation. | ||
It is meant to aid the understanding of those less familiar with formal language used within JSON Schema, or within specifications more broadly. | ||
(In fact, entries below make effort to avoid terminology like "normative" itself for reasons just mentioned.) | ||
|
||
If you encounter a term you wish were defined here, please feel free to [file an issue requesting it](https://github.com/json-schema-org/json-schema-org.github.io/issues/new?title=Add%20a%20glossary%20entry%20for%20). | ||
|
||
The entries on this page can be linked to via anchor links (e.g. `https://json-schema.org/learn/glossary.html#vocabulary`) when sharing a definition with others. | ||
|
||
### draft | ||
|
||
An individual release of the JSON Schema specification. | ||
|
||
JSON Schema drafts are not intended to be provisional documents, as the layman's use of the word "draft" might indicate. | ||
|
||
While future drafts may introduce new behavior or changes to existing behavior, each draft is a completed, released document, batching together changes to the specification, and intended for implementation and use. | ||
|
||
The current list of drafts can be found [here](https://json-schema.org/specification-links.html#published-drafts). | ||
|
||
### normative | ||
|
||
In the context of JSON Schema, and formal specifications more broadly, a document which outlines standardized behavior. | ||
This is as distinct from *non*-normative or informational documents, meant to explain, simplify or offer opinions. | ||
|
||
Distinguishing between whether a document is normative or not is intended to clarify to those using the document whether its contents are allowed to contradict or augment behavior described in other normative documents. | ||
JSON Schema's normative documents notably include its [specification](https://json-schema.org/specification.html). | ||
This page for instance, not being a normative document, is not able to proscribe new JSON Schema behavior not already covered by the specification. | ||
|
||
#### See also | ||
|
||
* [normative](https://developer.mozilla.org/en-US/docs/Glossary/Normative) and [non-normative](https://developer.mozilla.org/en-US/docs/Glossary/non-normative) in the Mozilla Glossary, and its links |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.