@leanprover/infoview
Preparing search index...
index
Module index
Namespaces
DocumentPosition
GoalLocation
GoalsLocation
RpcPtr
Enumerations
LeanFileProgressKind
LeanTag
RpcErrorCode
Classes
EditorConnection
RpcSessions
ServerVersion
Interfaces
ClientRequestOptions
ContextMenuAction
DocumentPosition
DynamicComponentProps
EditorApi
GoalsLocation
HighlightedTraceEmbed
InfoPopup
InfoviewApi
InfoviewConfig
InfoviewTacticStateFilter
InteractiveGoal
InteractiveGoalCore
InteractiveGoals
InteractiveHypothesisBundle
InteractiveTermGoal
LeanDiagnostic
LeanFileProgressParams
LeanFileProgressProcessingInfo
LeanPublishDiagnosticsParams
LeanServerCapabilities
LineRange
PanelWidgetProps
PlainGoal
PlainTermGoal
RpcCallParams
RpcConnected
RpcConnectParams
RpcError
RpcKeepAliveParams
RpcOptions
RpcReleaseParams
RpcServerIface
RpcSessionAtPos
RpcSessionForFile
ServerStoppedReason
SubexprInfo
TraceEmbed
UserWidget
UserWidgetInstance
UserWidgets
WidgetSource
Type Aliases
CodeWithInfos
ContextInfo
ContextMenuEntry
DiffTag
ExpectedTypeVisibility
FVarId
GoalLocation
GoToKind
HighlightedCodeWithInfos
HighlightedMsgEmbed
HighlightedSubexprInfo
HighlightMatchesOptions
InfoviewAction
InfoviewActionKind
InfoWithCtx
InteractiveCodeProps
InteractiveDiagnostic
LazyTraceChildren
MessageData
MessageOrder
ModuleHierarchyOptions
MsgEmbed
MVarId
Name
RpcPtr
RpcWireFormat
StrictOrLazy
SubexprPos
TaggedText
TermInfo
TextInsertKind
Variables
defaultInfoviewConfig
EditorContext
EnvPosContext
LocationsContext
RpcContext
VersionContext
Functions
DynamicComponent
getGoToLocation
getInteractiveDiagnostics
getInteractiveGoals
getInteractiveTermGoal
highlightMatches
importWidgetModule
InteractiveCode
InteractiveDiagnostics_infoToInteractive
InteractiveDiagnostics_msgToInteractive
InteractiveHypothesisBundle_nonAnonymousNames
InteractiveMessageData
isRpcError
lazyTraceChildrenToInteractive
mapRpcError
Markdown
renderInfoview
TaggedText_stripTags
useAsync
useAsyncPersistent
useAsyncWithTrigger
useClientNotificationEffect
useClientNotificationState
useEvent
useEventResult
useRpcSession
useServerNotificationEffect
useServerNotificationState
Widget_getWidgets
Widget_getWidgetSource
Settings
Member Visibility
Protected
Inherited
External
Theme
OS
Light
Dark
On This Page
Namespaces
Document
Position
Goal
Location
Goals
Location
Rpc
Ptr
Enumerations
Lean
File
Progress
Kind
Lean
Tag
Rpc
Error
Code
Classes
Editor
Connection
Rpc
Sessions
Server
Version
Interfaces
Client
Request
Options
Context
Menu
Action
Document
Position
Dynamic
Component
Props
Editor
Api
Goals
Location
Highlighted
Trace
Embed
Info
Popup
Infoview
Api
Infoview
Config
Infoview
Tactic
State
Filter
Interactive
Goal
Interactive
Goal
Core
Interactive
Goals
Interactive
Hypothesis
Bundle
Interactive
Term
Goal
Lean
Diagnostic
Lean
File
Progress
Params
Lean
File
Progress
Processing
Info
Lean
Publish
Diagnostics
Params
Lean
Server
Capabilities
Line
Range
Panel
Widget
Props
Plain
Goal
Plain
Term
Goal
Rpc
Call
Params
Rpc
Connected
Rpc
Connect
Params
Rpc
Error
Rpc
Keep
Alive
Params
Rpc
Options
Rpc
Release
Params
Rpc
Server
Iface
Rpc
Session
At
Pos
Rpc
Session
For
File
Server
Stopped
Reason
Subexpr
Info
Trace
Embed
User
Widget
User
Widget
Instance
User
Widgets
Widget
Source
Type Aliases
Code
With
Infos
Context
Info
Context
Menu
Entry
Diff
Tag
Expected
Type
Visibility
F
Var
Id
Goal
Location
Go
To
Kind
Highlighted
Code
With
Infos
Highlighted
Msg
Embed
Highlighted
Subexpr
Info
Highlight
Matches
Options
Infoview
Action
Infoview
Action
Kind
Info
With
Ctx
Interactive
Code
Props
Interactive
Diagnostic
Lazy
Trace
Children
Message
Data
Message
Order
Module
Hierarchy
Options
Msg
Embed
M
Var
Id
Name
Rpc
Ptr
Rpc
Wire
Format
Strict
Or
Lazy
Subexpr
Pos
Tagged
Text
Term
Info
Text
Insert
Kind
Variables
default
Infoview
Config
Editor
Context
Env
Pos
Context
Locations
Context
Rpc
Context
Version
Context
Functions
Dynamic
Component
get
Go
To
Location
get
Interactive
Diagnostics
get
Interactive
Goals
get
Interactive
Term
Goal
highlight
Matches
import
Widget
Module
Interactive
Code
Interactive
Diagnostics_
info
To
Interactive
Interactive
Diagnostics_
msg
To
Interactive
Interactive
Hypothesis
Bundle_
non
Anonymous
Names
Interactive
Message
Data
is
Rpc
Error
lazy
Trace
Children
To
Interactive
map
Rpc
Error
Markdown
render
Infoview
Tagged
Text_
strip
Tags
use
Async
use
Async
Persistent
use
Async
With
Trigger
use
Client
Notification
Effect
use
Client
Notification
State
use
Event
use
Event
Result
use
Rpc
Session
use
Server
Notification
Effect
use
Server
Notification
State
Widget_
get
Widgets
Widget_
get
Widget
Source
@leanprover/infoview
Loading...