Idris2Doc : Katla.Config

Katla.Config

(source)
Definitions
convert : Decoration -> String
  Visibility: export
record Category : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCategory : String -> String -> Category

  Projections:
  
.colour : Category -> String
  
.style : Category -> String

  Hint: 
FromDhall Category
.style : Category -> String
  Visibility: public export
style : Category -> String
  Visibility: public export
.colour : Category -> String
  Visibility: public export
colour : Category -> String
  Visibility: public export
record Config : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkConfig : String -> String -> Category -> Category -> Category -> Category -> Category -> Category -> Category -> Category -> Category -> Category -> Config

  Projections:
  
.aModule : Config -> Category
  
.bound : Config -> Category
  
.comment : Config -> Category
  
.datacons : Config -> Category
  
.font : Config -> String
  
.function : Config -> Category
  
.hole : Config -> Category
  
.keyword : Config -> Category
  
.namespce : Config -> Category
  
.postulte : Config -> Category
  
.space : Config -> String
  
.typecons : Config -> Category

  Hint: 
FromDhall Config
.space : Config -> String
  Visibility: public export
.font : Config -> String
  Visibility: public export
space : Config -> String
  Visibility: public export
font : Config -> String
  Visibility: public export
.datacons : Config -> Category
  Visibility: public export
datacons : Config -> Category
  Visibility: public export
.typecons : Config -> Category
  Visibility: public export
typecons : Config -> Category
  Visibility: public export
.bound : Config -> Category
  Visibility: public export
bound : Config -> Category
  Visibility: public export
.function : Config -> Category
  Visibility: public export
function : Config -> Category
  Visibility: public export
.keyword : Config -> Category
  Visibility: public export
keyword : Config -> Category
  Visibility: public export
.comment : Config -> Category
  Visibility: public export
comment : Config -> Category
  Visibility: public export
.hole : Config -> Category
  Visibility: public export
hole : Config -> Category
  Visibility: public export
.namespce : Config -> Category
  Visibility: public export
namespce : Config -> Category
  Visibility: public export
.postulte : Config -> Category
  Visibility: public export
postulte : Config -> Category
  Visibility: public export
.aModule : Config -> Category
  Visibility: public export
aModule : Config -> Category
  Visibility: public export
.toString : Category -> String -> {default (length prefixString) _ : Nat} -> String
  Visibility: export
.toString : Config -> String
  Visibility: export
defaultHTMLConfig : Config
  Visibility: export
defaultLatexConfig : Config
  Visibility: export
data Backend : Type
  Totality: total
  Visibility: public export
  Constructors:
  
LaTeX : Backend
  
HTML : Backend
  
Markdown : Backend
  
Literate : Backend
defaultConfig : Backend -> Config
  Visibility: export
getConfiguration : Backend -> Maybe String -> IO Config
  Visibility: export
record Driver : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDriver : (Nat -> Nat -> String, String) -> (Char -> List Char) -> (Maybe Decoration -> String -> String) -> (String, String) -> (String -> String, String) -> (String -> String, String) -> Driver

  Projections:
  
.annotate : Driver -> Maybe Decoration -> String -> String
  
.blockMacro : Driver -> (String -> String, String)
  
.escape : Driver -> Char -> List Char
  
.inlineMacro : Driver -> (String -> String, String)
  
.line : Driver -> (Nat -> Nat -> String, String)
  
.standalone : Driver -> (String, String)
.line : Driver -> (Nat -> Nat -> String, String)
  Visibility: public export
line : Driver -> (Nat -> Nat -> String, String)
  Visibility: public export
.escape : Driver -> Char -> List Char
  Visibility: public export
escape : Driver -> Char -> List Char
  Visibility: public export
.annotate : Driver -> Maybe Decoration -> String -> String
  Visibility: public export
annotate : Driver -> Maybe Decoration -> String -> String
  Visibility: public export
.standalone : Driver -> (String, String)
  Visibility: public export
standalone : Driver -> (String, String)
  Visibility: public export
.inlineMacro : Driver -> (String -> String, String)
  Visibility: public export
inlineMacro : Driver -> (String -> String, String)
  Visibility: public export
.blockMacro : Driver -> (String -> String, String)
  Visibility: public export
blockMacro : Driver -> (String -> String, String)
  Visibility: public export
initExec : Backend -> Maybe String -> IO ()
  Visibility: export