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.

Sign up for GitHub

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

Jump to bottom

Improve section nesting and ToC display #17

Merged
merged 2 commits into from
Aug 9, 2024
Merged

Improve section nesting and ToC display #17

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
de2c2a5
fix: Implement Kyle's suggested CSS fixes
david-christiansen Aug 9, 2024
2775551
fix: duplicate header nesting
david-christiansen Aug 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 3 additions & 5 deletions Manual/BuiltInTypes/String/Literals.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,9 @@ set_option pp.rawOnError true
tag := "string-syntax"
%%%

# Syntax

Lean has two kinds of string literals: ordinary string literals and raw string literals.

## String Literals
# String Literals

String literals begin and end with a double-quote character `"`. {index subterm:="string"}[literal]
Between these characters, they may contain any other character, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as `'\n'`, regardless of file encoding and platform).
Expand Down Expand Up @@ -64,7 +62,7 @@ The parser error is:
```


## Raw String Literals
# Raw String Literals

In {deftech}[raw string literals], {index subterm:="raw string"}[literal] there are no escape sequences or gaps, and each character denotes itself exactly.
Raw string literals are preceded by `r`, followed by zero or more hash characters (`#`) and a double quote `"`.
Expand Down Expand Up @@ -92,7 +90,7 @@ example : r##"This is r#"literally"# quoted"## = "This is r#\"literally\"# quote
```


## Interpolated Strings
# Interpolated Strings

Preceding a string literal with `s!` causes it to be processed as an {deftech}[_interpolated string_], in which regions of the string surrounded by `{` and `}` characters are parsed and interpreted as Lean expressions.
Interpolated strings are interpreted by appending the string that precedes the interpolation, the expression (with an added call to {name ToString.toString}`toString` surrounding it), and the string that follows the interpolation.
Expand Down
4 changes: 2 additions & 2 deletions lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "38b2cee26a96d1e9fb63f310b8f3251d83c5e7f6",
"rev": "1336f04b07cb29286fd1776b6b7e3564454c71dc",
"name": "subverso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -25,7 +25,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "e223cfcc12428144130fd2b20e5801675d29de6b",
"rev": "d0855a766c98af34f1ffaacd1858a8cca6c5e71c",
"name": "verso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
11 changes: 8 additions & 3 deletions static/theme.css
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,33 +111,38 @@ figcaption {
position: absolute;
left: -1.5em;
box-sizing: border-box;
font-variant-numeric: tabular-nums;
}

#toc > ol > li {
margin-left: 1.5em;
position: relative;
margin-bottom: 1ex;
}

#toc > ol > li > ol > li::before {
width: 2.25em;
position: absolute;
left: -2.25em;
box-sizing: border-box;
font-variant-numeric: tabular-nums;
}

#toc > ol > li > ol > li {
margin-left: 2.25em;
position: relative;
margin-bottom: 0.5ex;
}

#toc > ol > li > ol > li > ol > li::before {
width: 2.75em;
width: 3em;
position: absolute;
left: -2.75em;
left: -3em;
box-sizing: border-box;
font-variant-numeric: tabular-nums;
}

#toc > ol > li > ol > li > ol > li {
margin-left: 2.75em;
margin-left: 3em;
position: relative;
}
Loading