@@ -83,12 +83,6 @@ type NsItem = (Name, Maybe Docs, Accessibility)
8383type NsInfo = [NsItem]
8484type NsDict = M.Map NsName NsInfo
8585
86−-- Information stored together with IdrisDoc documentation
87−data DocInfo = DocInfo {
88− -- Namespaces already documented
89− namespaces :: S.Set NsName
90− }
91−
9286-- --------------------------------------------------------------- [ Utility ]
9387
9488-- | Make an error message
@@ -291,14 +285,21 @@ extractPTermNames (PUnifyLog p) = extract p
291285extractPTermNames (PNoImplicits p) = extract p
292286extractPTermNames _ = []
293287
288+-- | Shorter name for extractPTermNames
289+extract :: PTerm -- ^ Where to extract names from
290+ -> [Name] -- ^ Extracted names
294291extract = extractPTermNames
295292
293+-- | Helper function for extractPTermNames
294+extractPArg :: PArg -> [Name]
296295extractPArg (PImp {pname=n, getTm=p}) = n : extract p
297296extractPArg (PExp {getTm=p}) = extract p
298297extractPArg (PConstraint {getTm=p}) = extract p
299298extractPArg (PTacImplicit {pname=n, getScript=p1, getTm=p2})
300299 = n : (concatMap extract [p1, p2])
301300
301+-- | Helper function for extractPTermNames
302+extractPDo :: PDo -> [Name]
302303extractPDo (DoExp _ p) = extract p
303304extractPDo (DoBind _ n p) = n : extract p
304305extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
@@ -307,6 +308,8 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
307308extractPDo (DoLet _ n p1 p2) = n : concatMap extract [p1, p2]
308309extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
309310
311+-- | Helper function for extractPTermNames
312+extractPTactic :: PTactic -> [Name]
310313extractPTactic (Intro ns) = ns
311314extractPTactic (Focus n) = [n]
312315extractPTactic (Refine n _) = [n]
@@ -345,10 +348,9 @@ createDocs :: IState -- ^ Needed to determine the types of names
345348 -- documentation will be written.
346349 -> IO (Failable ())
347350createDocs ist nsd out =
348− do docInfo <- readDocInfo out
349− let (new, docInfo') = case docInfo of Nothing -> (True, DocInfo S.empty)
350− Just di -> (False, di)
351− nss = S.union (M.keysSet nsd) (namespaces docInfo')
351+ do new <- not `fmap` (doesFileExist $ out </> "IdrisDoc")
352+ existing_nss <- existingNamespaces out
353+ let nss = S.union (M.keysSet nsd) existing_nss
352354 dExists <- doesDirectoryExist out
353355 if new && dExists then err $ "Output directory (" ++ out ++ ") is" ++
354356 " already in use for other than IdrisDoc."
@@ -356,7 +358,10 @@ createDocs ist nsd out =
356358 createDirectoryIfMissing True out
357359 foldl docGen (return ()) (M.toList nsd)
358360 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) "")
364+ else return ()
360365 copyDependencies out
361366 return $ Right ()
362367
@@ -607,66 +612,32 @@ nbsp :: H.Html
607612nbsp = preEscapedToHtml (" " :: String)
608613
609614
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
618+ -- namespace pages
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
627+ ns = str2Ns name
628+ return $ if isFile && isHtml then Just ns else Nothing
629+ docsExists <- doesDirectoryExist docs
630+ if not docsExists
631+ then return S.empty
632+ else do contents <- getDirectoryContents docs
633+ namespaces <- catMaybes `fmap` (sequence $ map toNs contents)
634+ return $ S.fromList namespaces
635+
636+
610637-- | 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
612640 -> IO ()
613641copyDependencies dir =
614642 do styles <- getDataFileName $ "idrisdoc" </> "styles.css"
615− copyFile styles (dir </> "styles.css")
616−
617−-- ---------------------------------------------------- [ DocInfo Read/Write ]
618−
619−-- | Name of the DocInfo file
620−docInfoFile :: String
621−docInfoFile = "IdrisDoc"
622−
623−
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)
628−readDocInfo dir =
629− do exists <- doesFileExist (dir </> docInfoFile)
630− if not exists
631− then return Nothing
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
636−
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'
643− else s
644−
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
648− -> IO ()
649−writeDocInfo dir info = withFile (dir </> docInfoFile) WriteMode writer
650−
651− where writer h = BS.hPut h $ E.encodeUtf8 $ docInfo2Text info
652−
653−
654−-- | Converts a DocInfo to Text for easy writing
655−docInfo2Text :: DocInfo
656− -> T.Text
657−docInfo2Text (DocInfo {namespaces=nss}) = S.fold folder T.empty nss
658−
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)
663−
664−
665−-- | Converts an unmodified Text created by 'docInfo2Text' to DocInfo
666−text2DocInfo :: T.Text
667− -> DocInfo
668−text2DocInfo text = DocInfo $ foldl nsAdder S.empty (T.lines text)
669−
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
643+ copyFile styles (dir </> "styles.css")