diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2024-05-21 19:23:59 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2024-05-21 19:23:59 +0200 |
| commit | d87aa179ade758a02a9b1609dadc07bf842df635 (patch) | |
| tree | dcdf232039309ac3eb66fad112be06928d26f503 | |
| parent | 1ea35d4861f29faa5d7eab25c7773c0d9b638b38 (diff) | |
Allow line breaks via `\textbox`, handle `\left`/`\right`
| -rw-r--r-- | latex/naproche.sty | 3 | ||||
| -rw-r--r-- | library/topology/basis.tex | 4 | ||||
| -rw-r--r-- | source/Syntax/Concrete/Keywords.hs | 4 | ||||
| -rw-r--r-- | source/Syntax/Token.hs | 6 |
4 files changed, 9 insertions, 8 deletions
diff --git a/latex/naproche.sty b/latex/naproche.sty index 4bbefea..00ddf9a 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -11,7 +11,8 @@ % command for importing theories, no visible rendering \newcommand{\import}[1]{} \newcommand{\explanation}[1]{\quad\text{[#1]}} - +\usepackage{pbox} +\newcommand{\textbox}[1]{\pbox{28em}{#1}} diff --git a/library/topology/basis.tex b/library/topology/basis.tex index ecdd0f7..e33909f 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -45,6 +45,6 @@ \end{definition} \begin{definition}\label{genOpens} - $\genOpens{B}{X} = \{ U\in\pow{X} \mid \text{for all $x\in U$ there exists $V\in B$ - such that $x\in V\subseteq U$}\}$. + $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$ + \\ such that $x\in V\subseteq U$}\right\}$. \end{definition} diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs index e0f577e..135cdac 100644 --- a/source/Syntax/Concrete/Keywords.hs +++ b/source/Syntax/Concrete/Keywords.hs @@ -203,7 +203,7 @@ _haveIntro = _thus <|> _particularly <|> _have _colon :: Prod r Text (Located Token) SourcePos _colon = symbol ":" ? ":" _pipe :: Prod r Text (Located Token) SourcePos -_pipe = symbol "|" <|> command "mid" ? "\\mid" +_pipe = (optional (command "middle") *> symbol "|") <|> command "mid" ? "\\mid" _comma :: Prod r Text (Located Token) SourcePos _comma = symbol "," ? "," _commaAnd :: Prod r Text (Located Token) SourcePos @@ -219,4 +219,4 @@ _eq = symbol "=" ? "=" _in :: Prod r Text (Located Token) SourcePos _in = symbol "∈" <|> command "in" ? "\\in" _subseteq :: Prod r Text (Located Token) SourcePos -_subseteq = command "subseteq" ? ":" +_subseteq = command "subseteq" ? "\\subseteq" diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index eb0950f..65c02ca 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -228,7 +228,7 @@ mathToken = beginText :: Lexer (Located Token) beginText = lexeme do - Char.string "\\text{" + Char.string "\\text{" <|> Char.string "\\textbox{" setTextMode pure (BeginEnv "text") @@ -249,14 +249,14 @@ textToken = word <|> symbol <|> begin <|> end <|> textEnd <|> mathBegin <|> alig setMathMode pure (EndEnv "text") - opening' = lexeme (brace <|> group <|> paren <|> bracket) + opening' = lexeme (group <|> optional (Char.string "\\left") *> (brace <|> paren <|> bracket)) where brace = VisibleBraceL <$ lexeme (Char.string "\\{") group = InvisibleBraceL <$ lexeme (Char.char '{') <* modify' incrNesting paren = ParenL <$ lexeme (Char.char '(') bracket = BracketL <$ lexeme (Char.char '[') - closing' = lexeme (brace <|> group <|> paren <|> bracket) + closing' = lexeme (group <|> optional (Char.string "\\right") *> (brace <|> paren <|> bracket)) where brace = VisibleBraceR <$ lexeme (Char.string "\\}") group = InvisibleBraceR <$ lexeme (Char.char '}') <* modify' decrNesting |