console

本頁內容尚未翻譯。

machine.Console

record Console

The standard streams: unread input, written output and error output, and the flags of the last reads.

def Console.ofInput (text : String) : Console

A console that will read the given text, with nothing written yet.

def Console.write (text : String) (c : Console) : Console

Writes text to the standard output of c.

def Console.writeError (text : String) (c : Console) : Console

Writes text to the standard error of c.

def Console.feed (more : List Char) (c : Console) : Console

Appends more input after what c has not read yet.

def Console.consumed (rest : List Char) (c : Console) : Console

Records that a read left rest of the input of c.

def Console.markFailed (c : Console) : Console

Records in c that a read failed.

def Console.markAtEnd (c : Console) : Console

Records in c that a read reached the end of the input.

def Console.writeOutput (text : String) (c : Console) : (Console.write text c).output = String.append c.output text

Writing text to c appends it to the output.

def Console.feedInput (more : List Char) (c : Console) : (Console.feed more c).input = append c.input more

Feeding more to c adds it after the unread input.