inductive CancelAction : Type

What must be done when stopping the spinner?

• persist (sym : String) (msg : Option String) : CancelAction

  Replace the spinner animation with the symbol sym, optionally changing the message to msg.

• erase : CancelAction

  Completely erase the spinner.

• replace (msg : String) : CancelAction

  Print the given msg in place of the spinner.

structure Spinner : Type

• chan : Std.CloseableChannel Msg
• task : Task (Except IO.Error Unit)
• stream : IO.FS.Stream
• cancelAction : IO.Ref CancelAction

def Spinner.setTitle (spinner : Spinner) (title : String) : IO Unit

Change the title of the spinner.

Equations

• One or more equations did not get rendered due to their size.

def Spinner.log (spinner : Spinner) (line : String) : IO Unit

Print line as its own persisted line above the spinner, without stopping it (unlike Spinner.cancel .persist, which ends the spinner for good).

Equations

• One or more equations did not get rendered due to their size.

def Spinner.logOn (spinner : Spinner) (out : IO.FS.Stream) (line : String) : IO Unit

Like Spinner.log, but puts line on out instead of on the stream the animation is drawn on. For output that belongs on another handle — the compiled file going to standard output while the animation runs on standard error — and so must still be sequenced against the animation rather than written past it.

Equations

• One or more equations did not get rendered due to their size.

def Spinner.cancel (spinner : Spinner) (act : CancelAction := CancelAction.erase) : IO Unit

Stops the spinner, erasing the spinner and its message.

Equations

• One or more equations did not get rendered due to their size.

def Spinner.isCancelled (spinner : Spinner) : IO Bool

Check if a call to Spinner.cancel has already been done or not.

Equations

• spinner.isCancelled = liftM (IO.hasFinished (Spinner.task✝ spinner))

@[reducible, inline]

abbrev Spinner.new (spinner : SpinnerData) (message : Option String) : IO Spinner

Create a new spinner on stdout that will execute endAction when cancelled.

Equations

• Spinner.new spinner message = Spinner.newInner✝ spinner message none

@[reducible, inline]

abbrev Spinner.newOnStream (spinner : SpinnerData) (message : Option String) (stream : IO.FS.Stream) : IO Spinner

Create a new spinner on the provided stream that will execute endAction when cancelled.

Equations

• Spinner.newOnStream spinner message stream = Spinner.newInner✝ spinner message (some stream)