@@ -83,12 +83,6 @@ type NsItem = (Name, Maybe Docs, Accessibility)
83type NsInfo = [NsItem]
83type NsInfo = [NsItem]
84type NsDict = M.Map NsName NsInfo
84type NsDict = M.Map NsName NsInfo
86−-- Information stored together with IdrisDoc documentation
87−data DocInfo = DocInfo {
88− -- Namespaces already documented
89− namespaces :: S.Set NsName
92-- --------------------------------------------------------------- [ Utility ]
86-- --------------------------------------------------------------- [ Utility ]
94-- | Make an error message
88-- | Make an error message
@@ -291,14 +285,21 @@ extractPTermNames (PUnifyLog p) = extract p
291extractPTermNames (PNoImplicits p) = extract p
285extractPTermNames (PNoImplicits p) = extract p
292extractPTermNames _ = []
286extractPTermNames _ = []
288+-- | Shorter name for extractPTermNames
289+extract :: PTerm -- ^ Where to extract names from
290+ -> [Name] -- ^ Extracted names
294extract = extractPTermNames
291extract = extractPTermNames
293+-- | Helper function for extractPTermNames
294+extractPArg :: PArg -> [Name]
296extractPArg (PImp {pname=n, getTm=p}) = n : extract p
295extractPArg (PImp {pname=n, getTm=p}) = n : extract p
297extractPArg (PExp {getTm=p}) = extract p
296extractPArg (PExp {getTm=p}) = extract p
298extractPArg (PConstraint {getTm=p}) = extract p
297extractPArg (PConstraint {getTm=p}) = extract p
299extractPArg (PTacImplicit {pname=n, getScript=p1, getTm=p2})
298extractPArg (PTacImplicit {pname=n, getScript=p1, getTm=p2})
300 = n : (concatMap extract [p1, p2])
299 = n : (concatMap extract [p1, p2])
301+-- | Helper function for extractPTermNames
302+extractPDo :: PDo -> [Name]
302extractPDo (DoExp _ p) = extract p
303extractPDo (DoExp _ p) = extract p
303extractPDo (DoBind _ n p) = n : extract p
304extractPDo (DoBind _ n p) = n : extract p
304extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
305extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
@@ -307,6 +308,8 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
307extractPDo (DoLet _ n p1 p2) = n : concatMap extract [p1, p2]
308extractPDo (DoLet _ n p1 p2) = n : concatMap extract [p1, p2]
308extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
309extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
311+-- | Helper function for extractPTermNames
312+extractPTactic :: PTactic -> [Name]
310extractPTactic (Intro ns) = ns
313extractPTactic (Intro ns) = ns
311extractPTactic (Focus n) = [n]
314extractPTactic (Focus n) = [n]
312extractPTactic (Refine n _) = [n]
315extractPTactic (Refine n _) = [n]
@@ -345,10 +348,9 @@ createDocs :: IState -- ^ Needed to determine the types of names
345 -- documentation will be written.
348 -- documentation will be written.
346 -> IO (Failable ())
349 -> IO (Failable ())
347createDocs ist nsd out =
350createDocs ist nsd out =
348− do docInfo <- readDocInfo out
351+ do new <- not `fmap` (doesFileExist $ out </> "IdrisDoc")
349− let (new, docInfo') = case docInfo of Nothing -> (True, DocInfo S.empty)
352+ existing_nss <- existingNamespaces out
350− Just di -> (False, di)
351− nss = S.union (M.keysSet nsd) (namespaces docInfo')
353+ let nss = S.union (M.keysSet nsd) existing_nss
352 dExists <- doesDirectoryExist out
354 dExists <- doesDirectoryExist out
353 if new && dExists then err $ "Output directory (" ++ out ++ ") is" ++
355 if new && dExists then err $ "Output directory (" ++ out ++ ") is" ++
354 " already in use for other than IdrisDoc."
356 " already in use for other than IdrisDoc."
@@ -356,7 +358,10 @@ createDocs ist nsd out =
356 createDirectoryIfMissing True out
358 createDirectoryIfMissing True out
357 foldl docGen (return ()) (M.toList nsd)
359 foldl docGen (return ()) (M.toList nsd)
358 createIndex nss out
360 createIndex nss out
359− writeDocInfo out (docInfo' { namespaces = nss })
361+ -- Create an empty IdrisDoc file to signal 'out' is used for IdrisDoc
362+ if new -- But only if it not already existed...
363+ then withFile (out </> "IdrisDoc") WriteMode ((flip hPutStr) "")
360 copyDependencies out
365 copyDependencies out
361 return $ Right ()
366 return $ Right ()
@@ -607,66 +612,32 @@ nbsp :: H.Html
607nbsp = preEscapedToHtml (" " :: String)
612nbsp = preEscapedToHtml (" " :: String)
615+-- | Returns a list of namespaces already documented in a IdrisDoc directory
616+existingNamespaces :: FilePath -- ^ The base directory containing the
617+ -- 'docs' directory with existing
619+ -> IO (S.Set NsName)
620+existingNamespaces out = do
621+ let docs = out </> "docs"
622+ str2Ns s | s == rootNsStr = []
623+ str2Ns s = reverse $ T.splitOn (T.singleton '.') (txt s)
624+ toNs fp = do isFile <- doesFileExist $ docs </> fp
625+ let isHtml = ".html" == takeExtension fp
626+ name = dropExtension fp
628+ return $ if isFile && isHtml then Just ns else Nothing
629+ docsExists <- doesDirectoryExist docs
632+ else do contents <- getDirectoryContents docs
633+ namespaces <- catMaybes `fmap` (sequence $ map toNs contents)
634+ return $ S.fromList namespaces
610-- | Copies IdrisDoc dependencies such as stylesheets to a directory
637-- | Copies IdrisDoc dependencies such as stylesheets to a directory
611−copyDependencies :: FilePath
638+copyDependencies :: FilePath -- ^ The base directory to which
639+ -- dependencies should be written
613copyDependencies dir =
641copyDependencies dir =
614 do styles <- getDataFileName $ "idrisdoc" </> "styles.css"
642 do styles <- getDataFileName $ "idrisdoc" </> "styles.css"
615− copyFile styles (dir </> "styles.css")
643+ copyFile styles (dir </> "styles.css")
617−-- ---------------------------------------------------- [ DocInfo Read/Write ]
619−-- | Name of the DocInfo file
620−docInfoFile :: String
621−docInfoFile = "IdrisDoc"
624−-- | Reads the 'IdrisDoc' file from the given directory, if it is there
625−-- The info within is converted to a DocInfo
626−readDocInfo :: FilePath -- ^ The IdrisDoc directory also containing the info
627− -> IO (Maybe DocInfo)
629− do exists <- doesFileExist (dir </> docInfoFile)
632− -- Filter out namespaces for which documentation no longer exists
633− else do di <- (withFile (dir </> docInfoFile) ReadMode reader)
634− s <- S.fold (onlyValid dir) (return S.empty) (namespaces di)
635− return . Just . DocInfo $ s
637− where reader h = let converter = text2DocInfo . E.decodeUtf8
638− in converter `fmap` BS.hGetContents h
639− onlyValid out ns s = do s' <- s
640− let end = "docs" </> (genRelNsPath ns "html")
641− exists <- doesFileExist $ out </> end
642− if exists then return $ S.insert ns s'
645−-- | Writes a DocInfo to the 'IdrisDoc' file in the given directory
646−writeDocInfo :: FilePath -- ^ The directory to write to
647− -> DocInfo -- ^ The DocInfo to write
649−writeDocInfo dir info = withFile (dir </> docInfoFile) WriteMode writer
651− where writer h = BS.hPut h $ E.encodeUtf8 $ docInfo2Text info
654−-- | Converts a DocInfo to Text for easy writing
655−docInfo2Text :: DocInfo
657−docInfo2Text (DocInfo {namespaces=nss}) = S.fold folder T.empty nss
659− where folder [] res = T.append (txt rootNsStr) (T.cons '\n' res)
660− folder ns res = let base = (T.append (head ns) $ T.cons '\n' res)
661− in foldr joiner base (tail ns)
662− joiner n r = T.append n (T.cons '.' r)
665−-- | Converts an unmodified Text created by 'docInfo2Text' to DocInfo
666−text2DocInfo :: T.Text
668−text2DocInfo text = DocInfo $ foldl nsAdder S.empty (T.lines text)
670− where nsAdder set text = S.insert (txt2Ns text) set
671− txt2Ns t | t == (txt rootNsStr) = []
672− txt2Ns t = reverse $ T.splitOn (T.singleton '.') t