package jedit
- Alphabetic
- Public
- All
Type Members
- class AnnotationDialogue extends JFrame
-
class
BooleanOption extends MMTOption[Boolean]
a Boolean-valued option
-
class
BuildActions extends AnyRef
This class collects all build-related functionality to be triggered by GUI button, jedit actions, etc..
- class ContextMenu extends DynamicContextMenuService
- class DebugActions extends AnyRef
-
class
EditActions extends AnyRef
collects functionality that changes the text in the buffer these functions should be bound to actions in actions.xml, which can then be bound to keystrokes etc.
-
class
ErrorListForwarder extends ErrorHandler
sends MMT errors directly to jEdit ErrorList
-
class
FileOption extends TextOption[File]
a File-valued option
- class IDCompletion extends SideKickCompletion
-
sealed abstract
class
JAsset extends SourceAsset with MMTAsset
node in the sidekick outline tree: common ancestor class
-
class
JAuxAsset extends SourceAsset with MMTAuxAsset
a dummy asset for structuring the tree
-
class
JElemAsset extends JAsset with MMTElemAsset
node for structural elements
- class JNotAsset extends JAsset with MMTNotAsset
-
class
JObjAsset extends JAsset with MMTObjAsset
node for objects
-
class
JURIAsset extends JAsset with MMTURIAsset
a node for URIs
-
class
LineInvalidator extends MMTTaskProgressListener
used by sidekick to mark gutter lines for repainting
-
class
MMTConsole extends ThreadedConsole
a MMT console for jEdit, it reads MMT actions and prints the log output
- class MMTDockable extends JPanel
-
class
MMTError extends DefaultError
customizes the default errors of the ErrorList plugin
-
class
MMTErrorSource extends DefaultErrorSource
customizes the default error source of the ErrorList plugin
-
class
MMTGraphDockable extends JPanel
Created by raupi on 28.05.15.
-
class
MMTGutterAnnotations extends MMTTextAreaExtension
adds markers in the gutter whenever an annotation for a declaration in made in that line is known to MMT
- class MMTGutterExtension extends MMTTextAreaExtension
-
class
MMTHyperlink extends AbstractHyperlink
implements the action for clicking on a hyperlink provided by MMTHyperlinkSource
-
class
MMTHyperlinkSource extends HyperlinkSource
uses SourceRefs to provide hyperlinks in MMT documents
- class MMTInterpreter extends Shell
-
class
MMTMouseAdapter extends MouseAdapter
a MouseAdapter that the MMTPlugin adds to a TextAreaPainter in order to control mouse interaction
-
class
MMTOptimizationAnnotationReader extends AnnotationProvider
Extension for reading built optimizations from GraphOptimizationTool and providing annotations
-
abstract
class
MMTOption[A] extends AnyRef
interface to the jedit settings file and the options dialog
-
class
MMTOptions extends AbstractOptionPane
the MMT plugin options pane using the options defined in the companion object
-
class
MMTPlugin extends EBPlugin with Logger
The main class of the MMTPlugin after initialization, it creates a Controller and executes home/startup.mmt logging information is sent to home/mmtplugin.log the home directory is obtained from jEdit, e.g., settings/plugins/info.kwarc.mmt.jedit.MMTPlugin
- class MMTRefactorDockable extends JPanel
- class MMTSideKick extends SideKickParser with Logger
-
abstract
class
MMTTextAreaExtension extends TextAreaExtension
base class for MMT's text area extensions
-
class
MMTTextHighlighting extends MMTTextAreaExtension
A TextAreaExtension that is added to every EditPane it can be used for custom painting, e.g., background highlighting, tooltips Currently it highlights terminator characters
- class MMTToolBar extends JToolBar
-
class
MMTToolTips extends TextAreaExtension
shows tooltips such as type inference (separate from the other TextAreaExtension so that it can be put on a different layer)
- class MMTTreeDockable extends JPanel
- case class MyPosition(offset: Int) extends Position with Product with Serializable
- class OutputAsReport extends ReportHandler
-
class
ProverCompletion extends SideKickCompletion
auto-completion popup for options that are generated with types and holes
-
class
ScalaConsole extends ThreadedConsole
a Scala console for jEdit
- class ScrollTextareaPopup extends JFrame
-
class
StringOption extends TextOption[String]
a string-valued option
-
class
StyleChanger extends TextAreaExtension
A TextAreaExtension that is added to a layer below TEXT_LAYER in order to change the painter's styles for a certain mode The painter's styles are set by the EditPane according to SyntaxUtilities.loadStyles.
A TextAreaExtension that is added to a layer below TEXT_LAYER in order to change the painter's styles for a certain mode The painter's styles are set by the EditPane according to SyntaxUtilities.loadStyles. This class will override that setting. Tokens with type COMMENT3 and COMMENT4 will be subscripted resp. hidden, regardless of their style settings.
-
abstract
class
TextOption[A] extends MMTOption[A]
an option that is displayed as a text field
-
class
TextareaPopup extends JFrame
pops up a small text window on top of a TextArea
-
abstract
class
ThreadedConsole extends Shell
common code for Consoles, handles executing commands with different threads
Value Members
- object ContextMenu
- object EditActions
- object Inserter
- object MMTError
- object MMTHyperlink
-
object
MMTOptions extends Serializable
contains the various MMT options
contains the various MMT options
to add an option, just create it here and add it to the list of all options
- object MMTPlugin
- object MMTSideKick
- object Publisher
- object StatusBarLogger extends ReportHandler
- object StyleChanger