Add \dots commands
Add all of the \dots commands, and import their metrics from the ttf files. Fixes #23 Auditors: alpert
This commit is contained in:
parent
71da6aa50f
commit
6ee2ecf47e
File diff suppressed because one or more lines are too long
|
@ -10,6 +10,10 @@ metrics_to_extract = {
|
|||
u"\u2245",
|
||||
u"\u0020",
|
||||
u"\u00a0",
|
||||
u"\u2026",
|
||||
u"\u22ef",
|
||||
u"\u22f1",
|
||||
u"\u22ee",
|
||||
]
|
||||
}
|
||||
|
||||
|
|
50
symbols.js
50
symbols.js
|
@ -763,6 +763,56 @@ var symbols = {
|
|||
font: "math",
|
||||
group: "op",
|
||||
replace: "\u222b"
|
||||
},
|
||||
"\\ldots": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u2026"
|
||||
},
|
||||
"\\dotsc": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u2026"
|
||||
},
|
||||
"\\dotso": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u2026"
|
||||
},
|
||||
"\\dots": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u2026"
|
||||
},
|
||||
"\\cdots": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u22ef"
|
||||
},
|
||||
"\\dotsb": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u22ef"
|
||||
},
|
||||
"\\dotsm": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u22ef"
|
||||
},
|
||||
"\\dotsi": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u22ef"
|
||||
},
|
||||
"\\ddots": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u22f1"
|
||||
},
|
||||
"\\vdots": {
|
||||
font: "main",
|
||||
group: "punct",
|
||||
replace: "\u22ee"
|
||||
}
|
||||
},
|
||||
"text": {
|
||||
|
|
Loading…
Reference in New Issue
Block a user