Packages

package jedit

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Type Members

  1. class AnnotationDialogue extends JFrame
  2. class BooleanOption extends MMTOption[Boolean]

    a Boolean-valued option

  3. class BuildActions extends AnyRef

    This class collects all build-related functionality to be triggered by GUI button, jedit actions, etc..

  4. class ContextMenu extends DynamicContextMenuService
  5. class DebugActions extends AnyRef
  6. 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.

  7. class ErrorListForwarder extends ErrorHandler

    sends MMT errors directly to jEdit ErrorList

  8. class FileOption extends TextOption[File]

    a File-valued option

  9. class IDCompletion extends SideKickCompletion

  10. sealed abstract class JAsset extends SourceAsset with MMTAsset

    node in the sidekick outline tree: common ancestor class

  11. class JAuxAsset extends SourceAsset with MMTAuxAsset

    a dummy asset for structuring the tree

  12. class JElemAsset extends JAsset with MMTElemAsset

    node for structural elements

  13. class JNotAsset extends JAsset with MMTNotAsset
  14. class JObjAsset extends JAsset with MMTObjAsset

    node for objects

  15. class JURIAsset extends JAsset with MMTURIAsset

    a node for URIs

  16. class LineInvalidator extends MMTTaskProgressListener

    used by sidekick to mark gutter lines for repainting

  17. class MMTConsole extends ThreadedConsole

    a MMT console for jEdit, it reads MMT actions and prints the log output

  18. class MMTDockable extends JPanel
  19. class MMTError extends DefaultError

    customizes the default errors of the ErrorList plugin

  20. class MMTErrorSource extends DefaultErrorSource

    customizes the default error source of the ErrorList plugin

  21. class MMTGraphDockable extends JPanel

    Created by raupi on 28.05.15.

  22. class MMTGutterAnnotations extends MMTTextAreaExtension

    adds markers in the gutter whenever an annotation for a declaration in made in that line is known to MMT

  23. class MMTGutterExtension extends MMTTextAreaExtension
  24. class MMTHyperlink extends AbstractHyperlink

    implements the action for clicking on a hyperlink provided by MMTHyperlinkSource

  25. class MMTHyperlinkSource extends HyperlinkSource

    uses SourceRefs to provide hyperlinks in MMT documents

  26. class MMTInterpreter extends Shell
  27. class MMTMouseAdapter extends MouseAdapter

    a MouseAdapter that the MMTPlugin adds to a TextAreaPainter in order to control mouse interaction

  28. class MMTOptimizationAnnotationReader extends AnnotationProvider

    Extension for reading built optimizations from GraphOptimizationTool and providing annotations

  29. abstract class MMTOption[A] extends AnyRef

    interface to the jedit settings file and the options dialog

  30. class MMTOptions extends AbstractOptionPane

    the MMT plugin options pane using the options defined in the companion object

  31. 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

  32. class MMTRefactorDockable extends JPanel
  33. class MMTSideKick extends SideKickParser with Logger
  34. abstract class MMTTextAreaExtension extends TextAreaExtension

    base class for MMT's text area extensions

  35. 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

  36. class MMTToolBar extends JToolBar
  37. 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)

  38. class MMTTreeDockable extends JPanel
  39. case class MyPosition(offset: Int) extends Position with Product with Serializable
  40. class OutputAsReport extends ReportHandler
  41. class ProverCompletion extends SideKickCompletion

    auto-completion popup for options that are generated with types and holes

  42. class ScalaConsole extends ThreadedConsole

    a Scala console for jEdit

  43. class ScrollTextareaPopup extends JFrame
  44. class StringOption extends TextOption[String]

    a string-valued option

  45. 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.

  46. abstract class TextOption[A] extends MMTOption[A]

    an option that is displayed as a text field

  47. class TextareaPopup extends JFrame

    pops up a small text window on top of a TextArea

  48. abstract class ThreadedConsole extends Shell

    common code for Consoles, handles executing commands with different threads

Value Members

  1. object ContextMenu
  2. object EditActions
  3. object Inserter
  4. object MMTError
  5. object MMTHyperlink
  6. 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

  7. object MMTPlugin
  8. object MMTSideKick
  9. object Publisher
  10. object StatusBarLogger extends ReportHandler
  11. object StyleChanger

Ungrouped