Idris2Doc : Text.HTML.File

Text.HTML.File

(source)
Reexports
import public Data.FilePath
import public Web.Internal.FileTypes
Definitions
data FileEv : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NameChanged : String -> FileEv
  
FileChanged : File -> String -> FileEv
record FileEnv : Type -> Type
  Environment for editing files plus their paths

  Totality: total
  Visibility: public export
  Constructor: 
FE : (i -> i) -> (String -> Either String Body) -> String -> Class -> Class -> Class -> FileEnv i

  Projections:
  
.browse : FileEnv i -> String
  
.fileCls : FileEnv i -> Class
  
.fileID : FileEnv i -> i -> i
  
.inputCls : FileEnv i -> Class
  
.labelCls : FileEnv i -> Class
  
.readBody : FileEnv i -> String -> Either String Body
.fileID : FileEnv i -> i -> i
  Totality: total
  Visibility: public export
fileID : FileEnv i -> i -> i
  Totality: total
  Visibility: public export
.readBody : FileEnv i -> String -> Either String Body
  Totality: total
  Visibility: public export
readBody : FileEnv i -> String -> Either String Body
  Totality: total
  Visibility: public export
.browse : FileEnv i -> String
  Totality: total
  Visibility: public export
browse : FileEnv i -> String
  Totality: total
  Visibility: public export
.fileCls : FileEnv i -> Class
  Totality: total
  Visibility: public export
fileCls : FileEnv i -> Class
  Totality: total
  Visibility: public export
.inputCls : FileEnv i -> Class
  Totality: total
  Visibility: public export
inputCls : FileEnv i -> Class
  Totality: total
  Visibility: public export
.labelCls : FileEnv i -> Class
  Totality: total
  Visibility: public export
labelCls : FileEnv i -> Class
  Totality: total
  Visibility: public export
file : Cast i DomID => ValEnv i => FileEnv i => FileEnv i => i -> Maybe Body -> Node FileEv
  Totality: total
  Visibility: export