Idris.Doc.String

Reexports

Definitions

addDocString : Ref Ctxt Defs => Ref Syn SyntaxInfo => Name -> String -> Core ()

Visibility: export

addDocStringNS : Ref Ctxt Defs => Ref Syn SyntaxInfo => Namespace -> Name -> String -> Core ()

Visibility: export

prettyType : Ref Ctxt Defs => Ref Syn SyntaxInfo => (IdrisSyntax -> ann) -> ClosedTerm -> Core (Doc ann)

Visibility: export

getDocsForPrimitive : Ref Ctxt Defs => Ref Syn SyntaxInfo => Constant -> Core (Doc IdrisDocAnn)

Visibility: export

data Config : Type

Totality: total
Visibility: public export
Constructor: 

MkConfig : {default True _ : Bool} -> {default True _ : Bool} -> {default False _ : Bool} -> {default True _ : Bool} -> Config

  Configuration of the printer for a name
  @ showType    Do we show the type?
  @ longNames   Do we print qualified names?
  @ dropFirst   Do we drop the first argument in the type?
  @ getTotality Do we print the totality status of the function?

methodsConfig : Config

  Printer configuration for interface methods
  * longNames turned off for interface methods because the namespace is
              already spelt out for the interface itself
  * dropFirst turned on for interface methods because the first argument
              is always the interface constraint
  * totality  turned off for interface methods because the methods themselves
              are just projections out of a record and so are total

Visibility: export

shortNamesConfig : Config

Visibility: export

justUserDoc : Config

Visibility: export

getDocsForName : Ref ROpts REPLOpts => Ref Ctxt Defs => Ref Syn SyntaxInfo => FC -> Name -> Config -> Core (Doc IdrisDocAnn)

Visibility: export

getDocsForImplementation : Ref Syn SyntaxInfo => Ref Ctxt Defs => PTerm -> Core (Maybe (Doc IdrisSyntax))

Visibility: export

getDocsForPTerm : Ref ROpts REPLOpts => Ref Ctxt Defs => Ref Syn SyntaxInfo => PTerm -> Core (Doc IdrisDocAnn)

Visibility: export

getDocs : Ref ROpts REPLOpts => Ref Ctxt Defs => Ref Syn SyntaxInfo => DocDirective -> Core (Doc IdrisDocAnn)

Visibility: export

getContents : Ref ROpts REPLOpts => Ref Ctxt Defs => Ref Syn SyntaxInfo => Namespace -> Core (Doc IdrisDocAnn)

Visibility: export