pyk.kcfg.tui module

class BehaviorView(kcfg: KCFG, kprint: KPrint, minimize: bool = True, node_printer: NodePrinter | None = None, id: str = '')

Bases: ScrollableContainer

class Selected

Bases: Message

bubble: ClassVar[bool] = True

handler_name: ClassVar[str] = 'on_behavior_view_selected'

Name of the default message handler.

no_dispatch: ClassVar[bool] = False

time

verbose: ClassVar[bool] = False

can_focus: bool = True

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

compose() → ComposeResult

on_click(click: Click) → None

class Constraint

Bases: NavWidget

can_focus: bool = True

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

on_click(click: Click) → None

class Custom

Bases: NavWidget

can_focus: bool = True

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

on_click(click: Click) → None

class GraphChunk(id: str, node_text: Iterable[str] = ())

Bases: Static

class Selected(chunk_id: str)

Bases: Message

bubble: ClassVar[bool] = True

chunk_id: str

handler_name: ClassVar[str] = 'on_graph_chunk_selected'

Name of the default message handler.

no_dispatch: ClassVar[bool] = False

time

verbose: ClassVar[bool] = False

can_focus: bool = False

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

on_click(click: Click) → None

on_enter() → None

on_leave() → None

class Info

Bases: Widget

can_focus: bool = False

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

compose() → ComposeResult

text: reactive[str]

Create a reactive attribute.

Args:

default: A default value or callable that returns a default. layout: Perform a layout on change. repaint: Perform a repaint on change. init: Call watchers on initialize (post mount). always_update: Call watchers even when the new value equals the old value.

update(text: str) → None

watch_text() → None

class KCFGViewer(kcfg: KCFG, kprint: KPrint, node_printer: NodePrinter | None = None, custom_view: Callable[[KCFGElem], Iterable[str]] | None = None, minimize: bool = True)

Bases: App

BINDINGS: ClassVar[list[BindingType]] = [('h', 'keystroke("h")', 'Hide selected node.'), ('H', 'keystroke("H")', 'Unhide all nodes.'), ('t', 'keystroke("term")', 'Toggle term.'), ('c', 'keystroke("constraint")', 'Toggle constraint.'), ('m', 'keystroke("minimize")', 'Toggle minimization.'), ('s', 'keystroke("status")', 'Toggle status.'), Binding(key='q', action='quit', description='', show=True, key_display=None, priority=True)]

CSS_PATH: ClassVar[CSSPathType | None] = PosixPath('/home/runner/work/pyk/pyk/src/pyk/kcfg/style.css')

File paths to load CSS from.

action_keystroke(key: str) → None

compose() → ComposeResult

on_graph_chunk_selected(message: Selected) → None

class NavWidget(id: str)

Bases: ScrollableContainer

BINDINGS: ClassVar[list[BindingType]] = [('g', 'scroll_home', 'Go to vert start'), ('G', 'scroll_end', 'Go to vert end')]

Keyboard bindings for scrollable containers.

Key(s) | Description |

:- | :- |

up | Scroll up, if vertical scrolling is available. |

down | Scroll down, if vertical scrolling is available. |

left | Scroll left, if horizontal scrolling is available. |

right | Scroll right, if horizontal scrolling is available. |

home | Scroll to the home position, if scrolling is available. |

end | Scroll to the end position, if scrolling is available. |

pageup | Scroll up one page, if vertical scrolling is available. |

pagedown | Scroll down one page, if vertical scrolling is available. |

class Selected

Bases: Message

bubble: ClassVar[bool] = True

handler_name: ClassVar[str] = 'on_nav_widget_selected'

Name of the default message handler.

no_dispatch: ClassVar[bool] = False

time

verbose: ClassVar[bool] = False

can_focus: bool = True

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

compose() → ComposeResult

text: reactive[str]

Create a reactive attribute.

Args:

default: A default value or callable that returns a default. layout: Perform a layout on change. repaint: Perform a repaint on change. init: Call watchers on initialize (post mount). always_update: Call watchers even when the new value equals the old value.

update(text: str) → None

watch_text() → None

class NodeView(kprint: KPrint, id: str = '', minimize: bool = True, term_on: bool = True, constraint_on: bool = True, custom_on: bool = False, status_on: bool = True, custom_view: Callable[[KCFGElem], Iterable[str]] | None = None, proof_status: str = '', proof_id: str = '', exec_time: float = 0)

Bases: Widget

can_focus: bool = False

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

compose() → ComposeResult

on_behavior_view_selected() → None

on_constraint_selected() → None

on_custom_selected() → None

on_mount() → None

on_status_selected() → None

on_term_selected() → None

toggle_option(field: str) → bool

toggle_view(field: str) → None

update(element: Node | Successor) → None

class Status

Bases: NavWidget

can_focus: bool = True

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

on_click(click: Click) → None

class Term

Bases: NavWidget

can_focus: bool = True

Widget may receive focus.

can_focus_children: bool = True

Widget’s children may receive focus.

on_click(click: Click) → None