idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-03 00:55:00 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #1635 ] Show module docstring in HTML backend

Browse Source
This commit is contained in:
Guillaume ALLAIS 2021-08-20 12:46:28 +01:00 committed by G. Allais
parent e1bfaa7ae0
commit 1df84e8b5c
11 changed files with 94 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Binary.idr
View File

@ -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 ()

4
src/Core/Name/Namespace.idr
View File

@ -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

1
src/Core/Options/Log.idr
View File

@ -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),

12
src/Idris/Desugar.idr
View File

@ -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)

6
src/Idris/Doc/HTML.idr
View File

@ -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"
, "<div id=\"moduleHeader\">"
, "<h1>", show mod, "</h1>"
, maybe "" (\ mDoc => "<p>" ++ mDoc ++ "</p>") modDoc
, "</div>"
, !(docDocToHtml allModuleDocs)
, htmlFooter
]

23
src/Idris/Doc/String.idr
View File

@ -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

20
src/Idris/Package.idr
View File

@ -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) []

11
src/Idris/ProcessIdr.idr
View File

@ -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

2
src/Idris/REPL/Common.idr
View File

@ -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))]

34
src/Idris/Syntax.idr
View File

@ -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"))

2
support/docs/styles.css
View File

@ -65,7 +65,7 @@ h1 {
font-family: "Trebuchet MS", Helvetica, sans-serif;
}
body.namespace h1 {
#moduleHeader {
border-bottom: 1px solid #bbb;
padding-bottom: 2px;
}