package gui
GUIPanel and [GUIFrame]] maintain a swing-based graphical interface to the frontend.Controller and its children.
- Source
- package.scala
- Alphabetic
- By Inheritance
- gui
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- class BackendPane extends JScrollPane
- class ConfigPane extends JScrollPane
- class ControllerNode extends MMTNode
- class ExtManPane extends JScrollPane
- class GUIFrame extends JFrame
- class GUIPanel extends JPanel
-
case class
Item(label: String, id: String) extends Product with Serializable
a label-id pair, used e.g., to label and identify a GUI item
-
trait
MMTAsset extends AnyRef
node in the sidekick outline tree: common ancestor class
-
trait
MMTAuxAsset extends AnyRef
a dummy asset for structuring the tree
-
trait
MMTElemAsset extends MMTAsset
node for structural elements
- abstract class MMTNode extends AnyRef
- trait MMTNotAsset extends MMTAsset
-
trait
MMTObjAsset extends MMTAsset
node for objects
- class MMTTree extends JTree
- class MMTTreeModel extends TreeModel
-
trait
MMTURIAsset extends AnyRef
a node for URIs
-
trait
NavigationTree extends AnyRef
an abstraction for the classes used by UI-specific tree implementations
- abstract class NavigationTreeBuilder extends AnyRef
-
trait
NavigationTreeElement extends AnyRef
an abstraction for the classes used by UI-specific tree implementations
-
abstract
class
NavigationTreeElementInfo extends AnyRef
the semantic information to be stored in the nodes of a NavigationTreeElement
- trait NavigationTreeElements extends AnyRef
-
abstract
class
NavigationTreeImplementation[T <: NavigationTree, N <: NavigationTreeElement] extends AnyRef
abstraction for rendering trees in different UIs
-
case class
NavigationTreeInfo(src: File) extends Product with Serializable
global information about a NavigationTree
- class ObjNode extends MMTNode
- class PathNode extends MMTNode
- class SearchPane extends JPanel
- class StructuralElementNode extends MMTNode
- class TreePane extends JPanel
- class Window extends JWindow
- class WindowManager extends AnyRef
-
class
WrapLayout extends FlowLayout
Modified FlowLayout that wraps lines properly
Modified FlowLayout that wraps lines properly
This follows the ideas of WrapLayout.java but adds a defaultWidth