From 59cec853a697a4dd793c216c9bd603bd775d6da2 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Thu, 16 May 2024 15:59:04 +0200 Subject: Attach whitespace info to located token --- source/Syntax/Adapt.hs | 12 ++++++++---- source/Syntax/Token.hs | 50 ++++++++++++++++++++++++++++++++------------------ 2 files changed, 40 insertions(+), 22 deletions(-) (limited to 'source/Syntax') diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index b1237d2..3a8b3d6 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -26,10 +26,14 @@ scanChunk ltoks = let toks = unLocated <$> ltoks matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos) in case ltoks of - Located pos (BeginEnv "definition") : _ -> matchOrErr definition "definition" pos - Located pos (BeginEnv "abbreviation") : _ -> matchOrErr abbreviation "abbreviation" pos - Located pos (BeginEnv "struct") :_ -> matchOrErr struct "struct definition" pos - Located pos (BeginEnv "inductive") :_ -> matchOrErr inductive "inductive definition" pos + Located{startPos = pos, unLocated = BeginEnv "definition"} : _ -> + matchOrErr definition "definition" (pos) + Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ -> + matchOrErr abbreviation "abbreviation" pos + Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ -> + matchOrErr struct "struct definition" pos + Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> + matchOrErr inductive "inductive definition" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index 1d13693..eb0950f 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -164,8 +164,17 @@ instance Pretty Token where data Located a = Located { startPos :: !SourcePos , unLocated :: !a + , postWhitespace :: Whitespace } deriving (Show) +data Whitespace = NoSpace | Space deriving (Show) + +collapseWhitespace :: [Whitespace] -> Whitespace +collapseWhitespace = \case + Space : _ -> Space + NoSpace : ws -> collapseWhitespace ws + [] -> NoSpace + instance Eq a => Eq (Located a) where (==) = (==) `on` unLocated instance Ord a => Ord (Located a) where compare = compare `on` unLocated @@ -178,32 +187,32 @@ toks = whitespace *> goNormal id <* eof r <- optional tok case r of Nothing -> pure (f []) - Just t@(Located _ (BeginEnv "math")) -> goMath (f . (t:)) - Just t@(Located _ (BeginEnv "align*")) -> goMath (f . (t:)) + Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:)) + Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:)) Just t -> goNormal (f . (t:)) goText f = do r <- optional textToken case r of Nothing -> pure (f []) - Just t@(Located _ (BeginEnv "math")) -> goMathInText (f . (t:)) - Just t@(Located _ (EndEnv "text")) -> goMath (f . (t:)) - Just t@(Located _ (EndEnv "explanation")) -> goMath (f . (t:)) + Just t@Located{unLocated = BeginEnv "math"} -> goMathInText (f . (t:)) + Just t@Located{unLocated = EndEnv "text"} -> goMath (f . (t:)) + Just t@Located{unLocated = EndEnv "explanation"} -> goMath (f . (t:)) Just t -> goText (f . (t:)) goMath f = do r <- optional mathToken case r of Nothing -> pure (f []) - Just t@(Located _ (EndEnv "math")) -> goNormal (f . (t:)) - Just t@(Located _ (EndEnv "align*")) -> goNormal (f . (t:)) - Just t@(Located _ (BeginEnv "text")) -> goText (f . (t:)) - Just t@(Located _ (BeginEnv "explanation")) -> goText (f . (t:)) + Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:)) + Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:)) + Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:)) + Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:)) Just t -> goMath (f . (t:)) goMathInText f = do r <- optional mathToken case r of Nothing -> pure (f []) - Just t@(Located _ (EndEnv "math")) -> goText (f . (t:)) - Just t@(Located _ (BeginEnv "text")) -> goText (f . (t:)) + Just t@(Located{unLocated = EndEnv "math"}) -> goText (f . (t:)) + Just t@(Located{unLocated = BeginEnv "text"}) -> goText (f . (t:)) Just t -> goMathInText (f . (t:)) {-# INLINE toks #-} @@ -430,12 +439,17 @@ lexeme :: Lexer a -> Lexer (Located a) lexeme p = do start <- getSourcePos t <- p - whitespace - pure (Located start t) + w <- whitespace + pure (Located start t w) -space :: Lexer () -space = void (Char.char ' ' <|> Char.char '\n' <|> Char.char '\r') - <|> void (Char.string "\\ " <|> Char.string "\\\\" <|> Char.string "\\!" <|> Char.string "\\," <|> Char.string "\\:" <|> Char.string "\\;" <|> Char.string "\\;") +space :: Lexer Whitespace +space = Space <$ (Char.char ' ' <|> Char.char '\n' <|> Char.char '\r') + <|> Space <$ (Char.string "\\ " <|> Char.string "\\\\" <|> Char.string "\\!" <|> Char.string "\\," <|> Char.string "\\:" <|> Char.string "\\;" <|> Char.string "\\;") -whitespace :: Lexer () -whitespace = Lexer.space (void (some space)) (Lexer.skipLineComment "%") empty +whitespace :: Lexer Whitespace +whitespace = do + ws <- many (spaces <|> comment) + pure (collapseWhitespace ws) + where + spaces = collapseWhitespace <$> some space + comment = NoSpace <$ Lexer.skipLineComment "%" -- cgit v1.2.3 From d87aa179ade758a02a9b1609dadc07bf842df635 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Tue, 21 May 2024 19:23:59 +0200 Subject: Allow line breaks via `\textbox`, handle `\left`/`\right` --- latex/naproche.sty | 3 ++- library/topology/basis.tex | 4 ++-- source/Syntax/Concrete/Keywords.hs | 4 ++-- source/Syntax/Token.hs | 6 +++--- 4 files changed, 9 insertions(+), 8 deletions(-) (limited to 'source/Syntax') 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 -- cgit v1.2.3 From 9db5125330d293a9ea5eb09daf8198f7d5e18ca9 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Wed, 22 May 2024 16:56:50 +0200 Subject: Allow `\left` and `\right` everywhere --- source/Syntax/Token.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'source/Syntax') diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index 65c02ca..cb3f4cb 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -417,7 +417,7 @@ end = lexeme do -- | Parses an opening delimiter. opening :: Lexer (Located Token) -opening = lexeme (paren <|> brace <|> group <|> bracket) +opening = lexeme (group <|> optional (Char.string "\\left") *> (paren <|> brace <|> bracket)) where brace = VisibleBraceL <$ lexeme (Char.string "\\{") group = InvisibleBraceL <$ lexeme (Char.char '{') @@ -426,7 +426,7 @@ opening = lexeme (paren <|> brace <|> group <|> bracket) -- | Parses a closing delimiter. closing :: Lexer (Located Token) -closing = lexeme (paren <|> brace <|> group <|> bracket) +closing = lexeme (group <|> optional (Char.string "\\right") *> (paren <|> brace <|> bracket)) where brace = VisibleBraceR <$ lexeme (Char.string "\\}") group = InvisibleBraceR <$ lexeme (Char.char '}') -- cgit v1.2.3