Katla.Config

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