From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 10 Feb 2024 02:22:14 +0100
Subject: Initial commit

---
 source/Syntax/Import.hs | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 source/Syntax/Import.hs

(limited to 'source/Syntax/Import.hs')

diff --git a/source/Syntax/Import.hs b/source/Syntax/Import.hs
new file mode 100644
index 0000000..33082f1
--- /dev/null
+++ b/source/Syntax/Import.hs
@@ -0,0 +1,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{"
-- 
cgit v1.2.3