A "copy to clipboard" infoview widget

copyToClipboard creates a MessageData widget that copies a string to the clipboard when clicked. This may be rendered as some combination of a clickable "copy" codicon and clickable text. See copyToClipboard and CopyDisplay for details.

Note: we use CopyDisplay instead of e.g. an Option String for text and a top-level hasIcon := Bool for readability and to avoid situations where the user may remove both the icon and the text accidentally.

structure ImportGraph.Widget.CopyProps : Type

Props for the copy widget.

• display: if some s, render s as the label of a clickable link; if none, render just a copy icon.
• copyText: the string written to the clipboard on click.
• hasIcon: whether to show the copy/check codicon. Only consulted when display is some.

• display : Option String
• copyText : String
• hasIcon : Bool

@[instance_reducible]

instance ImportGraph.Widget.instRpcEncodableCopyProps : Lean.Server.RpcEncodable CopyProps

Equations

• ImportGraph.Widget.instRpcEncodableCopyProps = { rpcEncode := ImportGraph.Widget.instRpcEncodableCopyProps.enc✝, rpcDecode := ImportGraph.Widget.instRpcEncodableCopyProps.dec✝ }

def ImportGraph.Widget.Copy : Lean.Widget.Module

The copy-to-clipboard widget. Renders a blue link (if display := some s) and/or a clickable codicon button. Clicking either the text or the icon copies copyText.

Equations

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

inductive ImportGraph.Widget.CopyDisplay : Type

How copyToClipboard is displayed in the infoview. May be:

• .iconOnly to just display the "copy" codicon
• .text s (hasIcon := true) to display s : String (with or without a preceding codicon)
• .copiedText (hasIcon := true) to display the copied text (with or without a preceding codicon)

Everything displayed is clickable.

• text (s : String) (hasIcon : Bool := true) : CopyDisplay

  Displays some string with or without a preceding codicon.

  Note that this only needs to be used if hasIcon := false. Otherwise, you may take advantage of the coercion from String to CopyDisplay.

• iconOnly : CopyDisplay

  Displays just a "copy" codicon. This turns into a check when clicked.

• copiedText (hasIcon : Bool := true) : CopyDisplay

  Displays whatever text is to be copied, with or without a preceding codicon.

@[instance_reducible]

instance ImportGraph.Widget.instCoeStringCopyDisplay : Coe String CopyDisplay

Equations

• ImportGraph.Widget.instCoeStringCopyDisplay = { coe := fun (s : String) => ImportGraph.Widget.CopyDisplay.text s }

def ImportGraph.Widget.copyToClipboard (copyText : String) (display : CopyDisplay := CopyDisplay.iconOnly) : Lean.CoreM Lean.MessageData

Build a MessageData widget that, when clicked, copies copyText to the clipboard.

By default, this is simply a clickable "copy" codicon, but text may be provided through the display argument. Specifically:

• display := .iconOnly (the default) renders just a clickable "copy" codicon.
• display := .text s (hasIcon := true) or equivalently display := (s : String) (in the hasIcon := true case) displays s : String (with or without a preceding codicon)
• display := .copiedText (hasIcon := true) displays the copied text (with or without a preceding codicon)

Use as e.g. let msg ← copyToClipboard "text to be copied" (display := "(click to copy!)").

Equations

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