diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index f0fb594a8..87d595171 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -31,7 +31,7 @@ import public Libraries.Utils.Binary ||| (Increment this when changing anything in the data format) export ttcVersion : Int -ttcVersion = 59 +ttcVersion = 60 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Name/Namespace.idr b/src/Core/Name/Namespace.idr index 3acdbf677..1857cb50e 100644 --- a/src/Core/Name/Namespace.idr +++ b/src/Core/Name/Namespace.idr @@ -182,6 +182,10 @@ export Ord Namespace where compare (MkNS ms) (MkNS ns) = compare ms ns +export +Ord ModuleIdent where + compare (MkMI ms) (MkMI ns) = compare ms ns + mkNSInjective : MkNS ms === MkNS ns -> ms === ns mkNSInjective Refl = Refl diff --git a/src/Core/Options/Log.idr b/src/Core/Options/Log.idr index 3cb71b586..221c0d5fe 100644 --- a/src/Core/Options/Log.idr +++ b/src/Core/Options/Log.idr @@ -81,6 +81,7 @@ knownTopics = [ ("declare.type", Nothing), ("desugar.idiom", Nothing), ("doc.record", Nothing), + ("doc.module", Nothing), ("elab", Nothing), ("elab.ambiguous", Nothing), ("elab.app.var", Nothing), diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 6c75d9531..91b64ee81 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -2,6 +2,7 @@ module Idris.Desugar import Core.Binary import Core.Context +import Core.Context.Log import Core.Core import Core.Env import Core.Metadata @@ -15,6 +16,7 @@ import Libraries.Data.List.Extra import Libraries.Data.StringMap import Libraries.Data.String.Extra import Libraries.Data.ANameMap +import Libraries.Data.SortedMap import Idris.Doc.String import Idris.Syntax @@ -77,13 +79,21 @@ Eq Side where export extendSyn : {auto s : Ref Syn SyntaxInfo} -> + {auto c : Ref Ctxt Defs} -> SyntaxInfo -> Core () extendSyn newsyn = do syn <- get Syn + log "doc.module" 20 $ unlines + [ "Old (" ++ unwords (map show $ saveMod syn) ++ "): " + ++ show (modDocstrings syn) + , "New (" ++ unwords (map show $ saveMod newsyn) ++ "): " + ++ show (modDocstrings newsyn) + ] put Syn (record { infixes $= mergeLeft (infixes newsyn), prefixes $= mergeLeft (prefixes newsyn), ifaces $= merge (ifaces newsyn), - docstrings $= merge (docstrings newsyn), + modDocstrings $= merge (modDocstrings newsyn), + defDocstrings $= merge (defDocstrings newsyn), bracketholes $= ((bracketholes newsyn) ++) } syn) diff --git a/src/Idris/Doc/HTML.idr b/src/Idris/Doc/HTML.idr index 612a27aa8..b9847c629 100644 --- a/src/Idris/Doc/HTML.idr +++ b/src/Idris/Doc/HTML.idr @@ -144,11 +144,15 @@ renderDocIndex pkg = fastConcat $ export renderModuleDoc : {auto c : Ref Ctxt Defs} -> ModuleIdent -> + Maybe String -> Doc IdrisDocAnn -> Core String -renderModuleDoc mod allModuleDocs = pure $ fastConcat +renderModuleDoc mod modDoc allModuleDocs = pure $ fastConcat [ htmlPreamble (show mod) "../" "namespace" + , "
" , "

", show mod, "

" + , maybe "" (\ mDoc => "

" ++ mDoc ++ "

") modDoc + , "
" , !(docDocToHtml allModuleDocs) , htmlFooter ] diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index 14b9f0c87..fb3cde8d0 100644 --- a/src/Idris/Doc/String.idr +++ b/src/Idris/Doc/String.idr @@ -24,6 +24,7 @@ import Data.String import Libraries.Data.ANameMap import Libraries.Data.NameMap +import Libraries.Data.SortedMap import Libraries.Data.StringMap as S import Libraries.Data.String.Extra @@ -68,6 +69,16 @@ header : Doc IdrisDocAnn -> Doc IdrisDocAnn header d = annotate Header d <+> colon +-- Add a doc string for a module name +export +addModDocString : {auto s : Ref Syn SyntaxInfo} -> + ModuleIdent -> String -> + Core () +addModDocString mi doc + = do syn <- get Syn + put Syn (record { saveMod $= (mi ::) + , modDocstrings $= insert mi doc } syn) + -- Add a doc string for a name in the current namespace export addDocString : {auto c : Ref Ctxt Defs} -> @@ -79,7 +90,7 @@ addDocString n_in doc log "doc.record" 50 $ "Adding doc for " ++ show n_in ++ " (aka " ++ show n ++ " in current NS)" syn <- get Syn - put Syn (record { docstrings $= addName n doc, + put Syn (record { defDocstrings $= addName n doc, saveDocstrings $= insert n () } syn) -- Add a doc string for a name, in an extended namespace (e.g. for @@ -95,7 +106,7 @@ addDocStringNS ns n_in doc NS old root => NS (old <.> ns) root root => NS ns root syn <- get Syn - put Syn (record { docstrings $= addName n' doc, + put Syn (record { defDocstrings $= addName n' doc, saveDocstrings $= insert n' () } syn) prettyTerm : IPTerm -> Doc IdrisDocAnn @@ -167,7 +178,7 @@ getDocsForName fc n config resolved <- lookupCtxtName n (gamma defs) let all@(_ :: _) = extra ++ map fst resolved | _ => undefinedName fc n - let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn)) all + let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn)) all | [] => pure $ pretty ("No documentation for " ++ show n) docs <- traverse (showDoc config) ns pure $ vcat (punctuate Line docs) @@ -195,7 +206,7 @@ getDocsForName fc n config syn <- get Syn ty <- resugar [] =<< normaliseHoles defs [] (type def) let conWithTypeDoc = annotate (Decl con) (hsep [dCon con (prettyName con), colon, prettyTerm ty]) - case lookupName con (docstrings syn) of + case lookupName con (defDocstrings syn) of [(n, "")] => pure conWithTypeDoc [(n, str)] => pure $ vcat [ conWithTypeDoc @@ -214,7 +225,7 @@ getDocsForName fc n config getMethDoc : Method -> Core (List (Doc IdrisDocAnn)) getMethDoc meth = do syn <- get Syn - let [nstr] = lookupName meth.name (docstrings syn) + let [nstr] = lookupName meth.name (defDocstrings syn) | _ => pure [] pure <$> showDoc methodsConfig nstr @@ -281,7 +292,7 @@ getDocsForName fc n config ty <- resugar [] =<< normaliseHoles defs [] (type def) let prettyName = prettyName nm let projDecl = annotate (Decl nm) $ hsep [ fun nm prettyName, colon, prettyTerm ty ] - case lookupName nm (docstrings syn) of + case lookupName nm (defDocstrings syn) of [(_, "")] => pure projDecl [(_, str)] => pure $ vcat [ projDecl diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index a6e630c7d..324ffd165 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -3,6 +3,7 @@ module Idris.Package import Compiler.Common import Core.Context +import Core.Context.Log import Core.Core import Core.Directory import Core.Env @@ -22,6 +23,7 @@ import System.Directory import Libraries.System.Directory.Tree import System.File +import Libraries.Data.SortedMap import Libraries.Data.StringMap import Libraries.Data.StringTrie import Libraries.Text.Parser @@ -496,8 +498,11 @@ makeDoc pkg opts = setPPrint (MkPPOpts False False False) [] <- concat <$> for (modules pkg) (\(mod, filename) => do + -- load dependencies let ns = miAsNamespace mod addImport (MkImport emptyFC False mod ns) + + -- generate docs for all visible names defs <- get Ctxt names <- allNames (gamma defs) let allInNamespace = filter (inNS ns) names @@ -507,7 +512,20 @@ makeDoc pkg opts = allDocs <- for (sort visibleNames) $ \ nm => getDocsForName emptyFC nm shortNamesConfig let allDecls = annotate Declarations $ vcat allDocs - Right () <- coreLift $ writeFile outputFilePath !(renderModuleDoc mod allDecls) + + -- grab module header doc + syn <- get Syn + let modDoc = lookup mod (modDocstrings syn) + log "doc.module" 10 $ unwords + [ "Looked up doc for" + , show mod + , "and got:" + , show modDoc + ] + log "doc.module" 15 $ "from: " ++ show (modDocstrings syn) + + Right () <- do doc <- renderModuleDoc mod modDoc allDecls + coreLift $ writeFile outputFilePath doc | Left err => fileError (docBase "index.html") err pure $ the (List Error) [] diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index dc9ab0456..b5b0b8150 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -35,9 +35,11 @@ import Idris.REPL.Common import Idris.REPL.Opts import Idris.Syntax import Idris.Pretty +import Idris.Doc.String import Data.List import Libraries.Data.NameMap +import Libraries.Data.SortedMap import Libraries.Utils.Path import System @@ -322,6 +324,14 @@ processMod sourceFileName ttcFileName msg sourcecode origin (do p <- prog (PhysicalIdrSrc origin); eoi; pure p) | Left err => pure (Just [err]) traverse_ recordWarning ws + -- save the doc string for the current module + log "doc.module" 10 $ unlines + [ "Recording doc" + , documentation mod + , "for module " ++ show (moduleNS mod) + ] + addModDocString (moduleNS mod) (documentation mod) + addSemanticDecorations decor initHash traverse_ addPublicHash (sort importMetas) @@ -383,7 +393,6 @@ process buildmsg sourceFileName ident do defs <- get Ctxt ns <- ctxtPathToNS sourceFileName makeBuildDirectory ns - traverse_ (\cg => do Just cgdata <- getCG cg diff --git a/src/Idris/REPL/Common.idr b/src/Idris/REPL/Common.idr index 287369e94..8f82d0d3d 100644 --- a/src/Idris/REPL/Common.idr +++ b/src/Idris/REPL/Common.idr @@ -226,7 +226,7 @@ docsOrSignature fc n defs <- get Ctxt all@(_ :: _) <- lookupCtxtName n (gamma defs) | _ => undefinedName fc n - let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn)) + let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn)) (map fst all) | [] => typeSummary defs pure [!(render styleAnn !(getDocsForName fc n MkConfig))] diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 0647532ee..5c2a95dcf 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -2,6 +2,7 @@ module Idris.Syntax import public Core.Binary import public Core.Context +import public Core.Context.Log import public Core.Core import public Core.FC import public Core.Normalise @@ -16,6 +17,7 @@ import Data.List import Data.Maybe import Data.String import Libraries.Data.NameMap +import Libraries.Data.SortedMap import Libraries.Data.String.Extra import Libraries.Data.StringMap import Libraries.Text.PrettyPrint.Prettyprinter @@ -872,11 +874,16 @@ record SyntaxInfo where -- (most obviously, -) infixes : StringMap (Fixity, Nat) prefixes : StringMap Nat - ifaces : ANameMap IFaceInfo + -- info about modules + saveMod : List ModuleIdent -- current module name + modDocstrings : SortedMap ModuleIdent String + -- info about interfaces saveIFaces : List Name -- interfaces defined in current session, to save -- to ttc - docstrings : ANameMap String + ifaces : ANameMap IFaceInfo + -- info about definitions saveDocstrings : NameMap () -- names defined in current session + defDocstrings : ANameMap String bracketholes : List Name -- hole names in argument position (so need -- to be bracketed when solved) usingImpl : List (Maybe Name, RawImp) @@ -902,24 +909,29 @@ TTC SyntaxInfo where toBuf b syn = do toBuf b (StringMap.toList (infixes syn)) toBuf b (StringMap.toList (prefixes syn)) + toBuf b (filter (\n => elemBy (==) (fst n) (saveMod syn)) + (SortedMap.toList $ modDocstrings syn)) toBuf b (filter (\n => fst n `elem` saveIFaces syn) (ANameMap.toList (ifaces syn))) - toBuf b (filter (\n => case lookup (fst n) (saveDocstrings syn) of - Nothing => False - _ => True) - (ANameMap.toList (docstrings syn))) + toBuf b (filter (\n => isJust (lookup (fst n) (saveDocstrings syn))) + (ANameMap.toList (defDocstrings syn))) toBuf b (bracketholes syn) toBuf b (startExpr syn) fromBuf b = do inf <- fromBuf b pre <- fromBuf b + moddstr <- fromBuf b ifs <- fromBuf b - dstrs <- fromBuf b + defdstrs <- fromBuf b bhs <- fromBuf b start <- fromBuf b - pure (MkSyntax (fromList inf) (fromList pre) (fromList ifs) - [] (fromList dstrs) empty bhs [] start) + pure $ MkSyntax (fromList inf) (fromList pre) + [] (fromList moddstr) + [] (fromList ifs) + empty (fromList defdstrs) + bhs + [] start HasNames IFaceInfo where full gam iface @@ -962,10 +974,12 @@ initSyntax : SyntaxInfo initSyntax = MkSyntax initInfix initPrefix + [] empty [] - initDocStrings + empty initSaveDocStrings + initDocStrings [] [] (IVar EmptyFC (UN "main")) diff --git a/support/docs/styles.css b/support/docs/styles.css index f1a911f01..916ca7c0f 100644 --- a/support/docs/styles.css +++ b/support/docs/styles.css @@ -65,7 +65,7 @@ h1 { font-family: "Trebuchet MS", Helvetica, sans-serif; } -body.namespace h1 { +#moduleHeader { border-bottom: 1px solid #bbb; padding-bottom: 2px; }