Idris2Doc : Qutescript.Request

Qutescript.Request

(source)
Definitions
data QuteError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
UnsetEnvironment : String -> QuteError
  
InvalidMode : String -> String -> QuteError
  
InvalidFile : String -> String -> QuteError
  
InvalidPath : String -> String -> QuteError
  
InvalidNat : String -> String -> QuteError
data QuteMode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Hints : QuteMode
  
Command : QuteMode

  Hints:
  
Eq QuteMode
  
Ord QuteMode
  
Show QuteMode
record CommandData : Type
  Totality: total
  Visibility: public export
  Constructor: 
C : String -> String -> Nat -> Maybe Nat -> Maybe String -> CommandData

  Projections:
  
.count : CommandData -> Maybe Nat
  
.selectedText : CommandData -> Maybe String
  
.tabIndex : CommandData -> Nat
  
.title : CommandData -> String
  
.url : CommandData -> String
.url : CommandData -> String
  Totality: total
  Visibility: public export
url : CommandData -> String
  Totality: total
  Visibility: public export
.title : CommandData -> String
  Totality: total
  Visibility: public export
title : CommandData -> String
  Totality: total
  Visibility: public export
.tabIndex : CommandData -> Nat
  Totality: total
  Visibility: public export
tabIndex : CommandData -> Nat
  Totality: total
  Visibility: public export
.count : CommandData -> Maybe Nat
  Totality: total
  Visibility: public export
count : CommandData -> Maybe Nat
  Totality: total
  Visibility: public export
.selectedText : CommandData -> Maybe String
  Totality: total
  Visibility: public export
selectedText : CommandData -> Maybe String
  Totality: total
  Visibility: public export
record HintData : Type
  Totality: total
  Visibility: public export
  Constructor: 
H : String -> String -> Maybe String -> Maybe String -> HintData

  Projections:
  
.currentUrl : HintData -> String
  
.selectedHtml : HintData -> Maybe String
  
.selectedText : HintData -> Maybe String
  
.url : HintData -> String
.url : HintData -> String
  Totality: total
  Visibility: public export
url : HintData -> String
  Totality: total
  Visibility: public export
.currentUrl : HintData -> String
  Totality: total
  Visibility: public export
currentUrl : HintData -> String
  Totality: total
  Visibility: public export
.selectedText : HintData -> Maybe String
  Totality: total
  Visibility: public export
selectedText : HintData -> Maybe String
  Totality: total
  Visibility: public export
.selectedHtml : HintData -> Maybe String
  Totality: total
  Visibility: public export
selectedHtml : HintData -> Maybe String
  Totality: total
  Visibility: public export
0 ModeData : QuteMode -> Type
  Totality: total
  Visibility: public export
record Request : Type
  Totality: total
  Visibility: public export
  Constructor: 
R : (mode : QuteMode) -> Maybe String -> File Abs -> File Abs -> File Abs -> Path Abs -> Path Abs -> Path Abs -> Maybe String -> String -> ModeData mode -> Request

  Projections:
  
.commandlineText : Request -> Maybe String
  
.configDir : Request -> Path Abs
  
.dataDir : Request -> Path Abs
  
.downloadDir : Request -> Path Abs
  
.fifo : Request -> File Abs
  
.html : Request -> File Abs
  
.mode : Request -> QuteMode
  
.otherData : ({rec:0} : Request) -> ModeData (mode {rec:0})
  
.text : Request -> File Abs
  
.userAgent : Request -> Maybe String
  
.version : Request -> String
.mode : Request -> QuteMode
  Totality: total
  Visibility: public export
mode : Request -> QuteMode
  Totality: total
  Visibility: public export
.userAgent : Request -> Maybe String
  Totality: total
  Visibility: public export
userAgent : Request -> Maybe String
  Totality: total
  Visibility: public export
.fifo : Request -> File Abs
  Totality: total
  Visibility: public export
fifo : Request -> File Abs
  Totality: total
  Visibility: public export
.html : Request -> File Abs
  Totality: total
  Visibility: public export
html : Request -> File Abs
  Totality: total
  Visibility: public export
.text : Request -> File Abs
  Totality: total
  Visibility: public export
text : Request -> File Abs
  Totality: total
  Visibility: public export
.configDir : Request -> Path Abs
  Totality: total
  Visibility: public export
configDir : Request -> Path Abs
  Totality: total
  Visibility: public export
.dataDir : Request -> Path Abs
  Totality: total
  Visibility: public export
dataDir : Request -> Path Abs
  Totality: total
  Visibility: public export
.downloadDir : Request -> Path Abs
  Totality: total
  Visibility: public export
downloadDir : Request -> Path Abs
  Totality: total
  Visibility: public export
.commandlineText : Request -> Maybe String
  Totality: total
  Visibility: public export
commandlineText : Request -> Maybe String
  Totality: total
  Visibility: public export
.version : Request -> String
  Totality: total
  Visibility: public export
version : Request -> String
  Totality: total
  Visibility: public export
.otherData : ({rec:0} : Request) -> ModeData (mode {rec:0})
  Totality: total
  Visibility: public export
otherData : ({rec:0} : Request) -> ModeData (mode {rec:0})
  Totality: total
  Visibility: public export
request : Has QuteError ts => App ts Request
  Totality: total
  Visibility: export
pairs : Request -> List (String, String)
  Totality: total
  Visibility: export
printErr : QuteError -> String
  Totality: total
  Visibility: export
quteRun : All (\x => x -> String) ts -> App ts () -> IO ()
  Totality: total
  Visibility: export