blob: 33082f1a961630c51e9ecb4578eb1d83e968b31d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ApplicativeDo #-}
module Syntax.Import where
import Base
import Text.Regex.Applicative.Text
import Data.CharSet qualified as CharSet
import Data.Char (isAlphaNum)
gatherImports :: Text -> [FilePath]
gatherImports s = case findFirstPrefix imps s of
Nothing -> []
Just (paths, _) -> paths
imps :: RE Char [FilePath]
imps = do
mpath <- optional imp
paths <- many (few anySym *> string "\n" *> imp)
few anySym
begin
pure case mpath of
Nothing -> paths
Just path -> path : paths
imp :: RE Char FilePath
imp = do
-- Requiring a newline makes it possible to comment imports out.
string "\\import{"
path <- few (psym isTheoryNameChar)
sym '}'
pure path
isTheoryNameChar :: Char -> Bool
isTheoryNameChar c = isAlphaNum c || c `CharSet.member` CharSet.fromList ".-_/"
begin :: RE Char Text
begin = string "\\begin{"
|
