gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.prooftool/DrawSequentInProof

DrawSequentInProof

gapt.prooftool.DrawSequentInProof
class DrawSequentInProof[F, T <: SequentProof[F, T]](val parent: DrawSequentProof[F, T], sequent: Sequent[F], val mainAuxIndices: Set[SequentIndex], val cutAncestorIndices: Set[SequentIndex], sequentElementRenderer: F => String) extends DrawSequent[F, SequentProofViewer[F, T]]

Draws a sequent that is part of a sequent proof.

Unlike the general DrawSequent class, this contains logic relating to main/aux formulas and cut ancestors.

Type parameters

F

The type of elements of the sequent.

Value parameters

cutAncestorIndices

The indices of cut ancestors.

mainAuxIndices

The indices of main and aux formulas. Relevant for hiding contexts.

parent

The DrawSequentProof object that this belongs to.

sequent

The sequent to be displayed.

sequentElementRenderer

The function that turns elements of the sequent into strings.

Attributes

Source
DrawSequent.scala
Graph
Supertypes
class BoxPanel
trait Wrapper
trait SequentialContainer
class Panel
trait Wrapper
trait Container
class Component
trait UIElement
trait Publisher
trait Reactor
trait Proxy
class Object
trait Matchable
class Any
Show all

Members list

Type members

Inherited classlikes

protected class Content extends BufferWrapper[Component]

Attributes

Inherited from:
Wrapper
Source
Container.scala
Supertypes
class BufferWrapper[Component]
trait Buffer[Component]
trait Shrinkable[Component]
trait Growable[Component]
trait Clearable
trait Seq[Component]
trait SeqOps[Component, Buffer, Buffer[Component]]
trait Cloneable[Buffer[Component]]
trait Cloneable
trait Seq[Component]
trait Equals
trait SeqOps[Component, Buffer, Buffer[Component]]
trait PartialFunction[Int, Component]
trait Int => Component
trait Iterable[Component]
trait Iterable[Component]
trait IterableFactoryDefaults[Component, Buffer]
trait IterableOps[Component, Buffer, Buffer[Component]]
trait IterableOnceOps[Component, Buffer, Buffer[Component]]
trait IterableOnce[Component]
class Object
trait Matchable
class Any
Show all
object keys extends Publisher

Attributes

Inherited from:
Component
Source
Component.scala
Supertypes
trait Publisher
trait Reactor
class Object
trait Matchable
class Any
object mouse

Contains publishers for various mouse events. They are separated for efficiency reasons.

Contains publishers for various mouse events. They are separated for efficiency reasons.

Attributes

Inherited from:
Component
Source
Component.scala
Supertypes
class Object
trait Matchable
class Any

Value members

Inherited methods

def background: Color

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def background_=(c: Color): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def border: Border

Attributes

Inherited from:
Component
Source
Component.scala
def border_=(b: Border): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def bounds: Rectangle

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def componentOrientation: ComponentOrientation

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def componentOrientation_=(x: ComponentOrientation): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def cursor: Cursor

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def cursor_=(c: Cursor): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def deafTo(ps: Publisher*): Unit

Installed reaction won't receive events from the given publisher anylonger.

Installed reaction won't receive events from the given publisher anylonger.

Attributes

Inherited from:
Reactor
Source
Reactor.scala
def displayable: Boolean

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def enabled: Boolean

Attributes

Inherited from:
Component
Source
Component.scala
def enabled_=(b: Boolean): Unit

Attributes

Inherited from:
Component
Source
Component.scala
override def equals(that: Any): Boolean

Compares the receiver object (this) with the argument object (that) for equivalence.

Compares the receiver object (this) with the argument object (that) for equivalence.

Any implementation of this method should be an equivalence relation:

  • It is reflexive: for any instance x of type Any, x.equals(x) should return true.
  • It is symmetric: for any instances x and y of type Any, x.equals(y) should return true if and only if y.equals(x) returns true.
  • It is transitive: for any instances x, y, and z of type Any if x.equals(y) returns true and y.equals(z) returns true, then x.equals(z) should return true.

If you override this method, you should verify that your implementation remains an equivalence relation. Additionally, when overriding this method it is usually necessary to override hashCode to ensure that objects which are "equal" (o1.equals(o2) returns true) hash to the same scala.Int. (o1.hashCode.equals(o2.hashCode)).

Value parameters

that

the object to compare against this object for equality.

Attributes

Returns

true if the receiver object is equivalent to the argument; false otherwise.

Definition Classes
Proxy -> Any
Inherited from:
Proxy
def focusable: Boolean

Attributes

Inherited from:
Component
Source
Component.scala
def focusable_=(b: Boolean): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def font: Font

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def font_=(f: Font): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def foreground: Color

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def foreground_=(c: Color): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def hasFocus: Boolean

Attributes

Inherited from:
Component
Source
Component.scala
override def hashCode(): Int

Calculate a hash code value for the object.

Calculate a hash code value for the object.

The default hashing algorithm is platform dependent.

Note that it is allowed for two objects to have identical hash codes (o1.hashCode.equals(o2.hashCode)) yet not be equal (o1.equals(o2) returns false). A degenerate implementation could always return 0. However, it is required that if two objects are equal (o1.equals(o2) returns true) that they have identical hash codes (o1.hashCode.equals(o2.hashCode)). Therefore, when overriding this method, be sure to verify that the behavior is consistent with the equals method.

Attributes

Returns

the hash code value for this object.

Definition Classes
Proxy -> Any
Inherited from:
Proxy
def ignoreRepaint: Boolean

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def ignoreRepaint_=(b: Boolean): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def inputVerifier: Component => Boolean

Attributes

Inherited from:
Component
Source
Component.scala
def inputVerifier_=(v: Component => Boolean): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def listenTo(ps: Publisher*): Unit

Listen to the given publisher as long as deafTo isn't called for them.

Listen to the given publisher as long as deafTo isn't called for them.

Attributes

Inherited from:
Reactor
Source
Reactor.scala
def locale: Locale

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def location: Point

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def locationOnScreen: Point

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def maximumSize: Dimension

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def maximumSize_=(x: Dimension): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def minimumSize: Dimension

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def minimumSize_=(x: Dimension): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def name: String

Attributes

Inherited from:
Component
Source
Component.scala
def name_=(s: String): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def opaque: Boolean

Attributes

Inherited from:
Component
Source
Component.scala
def opaque_=(b: Boolean): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def paint(g: Graphics2D): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def preferredSize: Dimension

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def preferredSize_=(x: Dimension): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def publish(e: Event): Unit

Notify all registered reactions.

Notify all registered reactions.

Attributes

Inherited from:
Publisher
Source
Publisher.scala
def repaint(rect: Rectangle): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def repaint(): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def requestFocus(): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def requestFocusInWindow(): Boolean

Attributes

Inherited from:
Component
Source
Component.scala
def revalidate(): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def self: Any

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def showing: Boolean

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def size: Dimension

Attributes

Inherited from:
UIElement
Source
UIElement.scala
override def subscribe(listener: Reaction): Unit

Attributes

Definition Classes
LazyPublisher -> Publisher
Inherited from:
LazyPublisher (hidden)
Source
Publisher.scala
override def toString: String

Returns a string representation of the object.

Returns a string representation of the object.

The default representation is platform dependent.

Attributes

Returns

a string representation of the object.

Definition Classes
Component -> Proxy -> Any
Inherited from:
Component
Source
Component.scala
def toolkit: Toolkit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def tooltip: String

Attributes

Inherited from:
Component
Source
Component.scala
def tooltip_=(t: String): Unit

Attributes

Inherited from:
Component
Source
Component.scala
override def unsubscribe(listener: Reaction): Unit

Attributes

Definition Classes
LazyPublisher -> Publisher
Inherited from:
LazyPublisher (hidden)
Source
Publisher.scala
def validate(): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def visible: Boolean

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def visible_=(b: Boolean): Unit

Attributes

Inherited from:
UIElement
Source
UIElement.scala
def width(): Int

Attributes

Inherited from:
DrawSequent
Source
DrawSequent.scala
def xLayoutAlignment: Double

Used by certain layout managers, e.g., BoxLayout or OverlayLayout to align components relative to each other.

Used by certain layout managers, e.g., BoxLayout or OverlayLayout to align components relative to each other.

Attributes

Inherited from:
Component
Source
Component.scala
def xLayoutAlignment_=(x: Double): Unit

Attributes

Inherited from:
Component
Source
Component.scala
def yLayoutAlignment: Double

Attributes

Inherited from:
Component
Source
Component.scala
def yLayoutAlignment_=(y: Double): Unit

Attributes

Inherited from:
Component
Source
Component.scala

Concrete fields

val parent: DrawSequentProof[F, T]

Attributes

Source
DrawSequent.scala
val pos: List[Int]

Attributes

Source
DrawSequent.scala

Inherited fields

protected val _contents: Content

Attributes

Inherited from:
Wrapper
Source
Container.scala
val commaLabelSequent: Sequent[CommaLabel]

Attributes

Inherited from:
DrawSequent
Source
DrawSequent.scala
override val contents: Buffer[Component]

The child components of this container.

The child components of this container.

Attributes

Inherited from:
Wrapper
Source
SequentialContainer.scala
protected val listeners: RefSet[Reaction]

Attributes

Inherited from:
Publisher
Source
Publisher.scala
val main: SequentProofViewer[F, T]

Attributes

Inherited from:
DrawSequent
Source
DrawSequent.scala
lazy override val peer: JPanel

The underlying Swing peer.

The underlying Swing peer.

Attributes

Inherited from:
BoxPanel
Source
BoxPanel.scala
val reactions: Reactions

All reactions of this reactor.

All reactions of this reactor.

Attributes

Inherited from:
Reactor
Source
Reactor.scala
val turnstileLabel: LatexTurnstileLabel

Attributes

Inherited from:
DrawSequent
Source
DrawSequent.scala
Generated with