src/Tools/jEdit/src/plugin.scala
author wenzelm
Sat Jun 18 21:20:22 2011 +0200 (2011-06-18)
changeset 43449 591598bc52bc
parent 43443 5d9693c2337e
child 43452 5cf548485529
permissions -rw-r--r--
convenience functions;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/plugin.scala
wenzelm@36760
     2
    Author:     Makarius
wenzelm@36760
     3
wenzelm@36760
     4
Main Isabelle/jEdit plugin setup.
wenzelm@36760
     5
*/
wenzelm@34407
     6
wenzelm@34318
     7
package isabelle.jedit
wenzelm@34318
     8
wenzelm@34429
     9
wenzelm@36015
    10
import isabelle._
wenzelm@36015
    11
wenzelm@34429
    12
import java.io.{FileInputStream, IOException}
wenzelm@34318
    13
import java.awt.Font
wenzelm@34318
    14
wenzelm@34497
    15
import scala.collection.mutable
wenzelm@39517
    16
import scala.swing.ComboBox
immler@34406
    17
wenzelm@39241
    18
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
wenzelm@39241
    19
  Buffer, EditPane, ServiceManager, View}
immler@34406
    20
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@39043
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
wenzelm@43443
    22
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
wenzelm@39633
    23
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
wenzelm@37068
    24
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@34429
    25
wenzelm@43443
    26
import org.gjt.sp.util.SyntaxUtilities
wenzelm@39241
    27
import org.gjt.sp.util.Log
wenzelm@39241
    28
wenzelm@39630
    29
import scala.actors.Actor
wenzelm@39630
    30
import Actor._
wenzelm@39630
    31
wenzelm@34318
    32
wenzelm@34618
    33
object Isabelle
wenzelm@34618
    34
{
wenzelm@34784
    35
  /* plugin instance */
wenzelm@34784
    36
wenzelm@43443
    37
  var plugin: Plugin = null
wenzelm@34784
    38
  var system: Isabelle_System = null
wenzelm@34784
    39
  var session: Session = null
wenzelm@34784
    40
wenzelm@34784
    41
wenzelm@43443
    42
  /* extended syntax styles */
wenzelm@43443
    43
wenzelm@43443
    44
  def extended_styles: Boolean = plugin != null && plugin._extended_styles
wenzelm@43443
    45
wenzelm@43443
    46
wenzelm@34618
    47
  /* properties */
wenzelm@34618
    48
wenzelm@34618
    49
  val OPTION_PREFIX = "options.isabelle."
wenzelm@34618
    50
wenzelm@34618
    51
  object Property
wenzelm@34618
    52
  {
wenzelm@36814
    53
    def apply(name: String): String =
wenzelm@36814
    54
      jEdit.getProperty(OPTION_PREFIX + name)
wenzelm@36814
    55
    def apply(name: String, default: String): String =
wenzelm@36814
    56
      jEdit.getProperty(OPTION_PREFIX + name, default)
wenzelm@36814
    57
    def update(name: String, value: String) =
wenzelm@36814
    58
      jEdit.setProperty(OPTION_PREFIX + name, value)
wenzelm@34468
    59
  }
wenzelm@34433
    60
wenzelm@34618
    61
  object Boolean_Property
wenzelm@34618
    62
  {
wenzelm@36814
    63
    def apply(name: String): Boolean =
wenzelm@36814
    64
      jEdit.getBooleanProperty(OPTION_PREFIX + name)
wenzelm@36814
    65
    def apply(name: String, default: Boolean): Boolean =
wenzelm@36814
    66
      jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
wenzelm@36814
    67
    def update(name: String, value: Boolean) =
wenzelm@36814
    68
      jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
wenzelm@34618
    69
  }
wenzelm@34618
    70
wenzelm@34618
    71
  object Int_Property
wenzelm@34618
    72
  {
wenzelm@36814
    73
    def apply(name: String): Int =
wenzelm@36814
    74
      jEdit.getIntegerProperty(OPTION_PREFIX + name)
wenzelm@36814
    75
    def apply(name: String, default: Int): Int =
wenzelm@36814
    76
      jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
wenzelm@36814
    77
    def update(name: String, value: Int) =
wenzelm@36814
    78
      jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
wenzelm@34618
    79
  }
wenzelm@34618
    80
wenzelm@40848
    81
  object Double_Property
wenzelm@40848
    82
  {
wenzelm@40848
    83
    def apply(name: String): Double =
wenzelm@40848
    84
      jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
wenzelm@40848
    85
    def apply(name: String, default: Double): Double =
wenzelm@40848
    86
      jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
wenzelm@40848
    87
    def update(name: String, value: Double) =
wenzelm@40848
    88
      jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
wenzelm@40848
    89
  }
wenzelm@40848
    90
wenzelm@40850
    91
  object Time_Property
wenzelm@40850
    92
  {
wenzelm@40850
    93
    def apply(name: String): Time =
wenzelm@40850
    94
      Time.seconds(Double_Property(name))
wenzelm@40850
    95
    def apply(name: String, default: Time): Time =
wenzelm@40850
    96
      Time.seconds(Double_Property(name, default.seconds))
wenzelm@40850
    97
    def update(name: String, value: Time) =
wenzelm@40850
    98
      Double_Property.update(name, value.seconds)
wenzelm@40850
    99
  }
wenzelm@40850
   100
wenzelm@40848
   101
wenzelm@37164
   102
  /* font */
wenzelm@37164
   103
wenzelm@37164
   104
  def font_family(): String = jEdit.getProperty("view.font")
wenzelm@37164
   105
wenzelm@37019
   106
  def font_size(): Float =
wenzelm@37019
   107
    (jEdit.getIntegerProperty("view.fontsize", 16) *
wenzelm@37019
   108
      Int_Property("relative-font-size", 100)).toFloat / 100
wenzelm@36814
   109
wenzelm@34618
   110
wenzelm@39043
   111
  /* text area ranges */
wenzelm@39043
   112
wenzelm@39043
   113
  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
wenzelm@39043
   114
wenzelm@39043
   115
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
wenzelm@39043
   116
  {
wenzelm@39043
   117
    val p = text_area.offsetToXY(range.start)
wenzelm@39043
   118
    val q = text_area.offsetToXY(range.stop)
wenzelm@39043
   119
    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
wenzelm@39043
   120
    else None
wenzelm@39043
   121
  }
wenzelm@39043
   122
wenzelm@39043
   123
wenzelm@37201
   124
  /* tooltip markup */
wenzelm@37201
   125
wenzelm@37201
   126
  def tooltip(text: String): String =
wenzelm@37203
   127
    "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
wenzelm@37203
   128
        Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
wenzelm@37203
   129
      HTML.encode(text) + "</pre></html>"
wenzelm@37201
   130
wenzelm@40849
   131
  def tooltip_dismiss_delay(): Time =
wenzelm@40852
   132
    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
wenzelm@38854
   133
wenzelm@38854
   134
  def setup_tooltips()
wenzelm@38854
   135
  {
wenzelm@38854
   136
    Swing_Thread.now {
wenzelm@38854
   137
      val manager = javax.swing.ToolTipManager.sharedInstance
wenzelm@40849
   138
      manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
wenzelm@38854
   139
    }
wenzelm@38854
   140
  }
wenzelm@38854
   141
wenzelm@37201
   142
wenzelm@39241
   143
  /* icons */
wenzelm@39241
   144
wenzelm@39241
   145
  def load_icon(name: String): javax.swing.Icon =
wenzelm@39241
   146
  {
wenzelm@39241
   147
    val icon = GUIUtilities.loadIcon(name)
wenzelm@39241
   148
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
wenzelm@39630
   149
      Log.log(Log.ERROR, icon, "Bad icon: " + name)
wenzelm@39241
   150
    icon
wenzelm@39241
   151
  }
wenzelm@39241
   152
wenzelm@39241
   153
wenzelm@41382
   154
  /* check JVM */
wenzelm@41382
   155
wenzelm@41382
   156
  def check_jvm()
wenzelm@41382
   157
  {
wenzelm@41382
   158
    if (!Platform.is_hotspot) {
wenzelm@41382
   159
      Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
wenzelm@41382
   160
        "This is " + Platform.jvm_name,
wenzelm@41382
   161
        "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
wenzelm@41382
   162
    }
wenzelm@41382
   163
  }
wenzelm@41382
   164
wenzelm@41382
   165
wenzelm@38221
   166
  /* main jEdit components */
wenzelm@34784
   167
wenzelm@37177
   168
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
wenzelm@34784
   169
wenzelm@37177
   170
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
wenzelm@34784
   171
wenzelm@34784
   172
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
wenzelm@37177
   173
    view.getEditPanes().iterator.map(_.getTextArea)
wenzelm@34784
   174
wenzelm@34784
   175
  def jedit_text_areas(): Iterator[JEditTextArea] =
wenzelm@34784
   176
    jedit_views().flatMap(jedit_text_areas(_))
wenzelm@34784
   177
wenzelm@34784
   178
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
wenzelm@34784
   179
    jedit_text_areas().filter(_.getBuffer == buffer)
wenzelm@34784
   180
wenzelm@38843
   181
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@38640
   182
  {
wenzelm@38640
   183
    try { buffer.readLock(); body }
wenzelm@38640
   184
    finally { buffer.readUnlock() }
wenzelm@38640
   185
  }
wenzelm@38640
   186
wenzelm@38843
   187
  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@38843
   188
    Swing_Thread.now { buffer_lock(buffer) { body } }
wenzelm@38843
   189
wenzelm@40474
   190
  def buffer_text(buffer: JEditBuffer): String =
wenzelm@40474
   191
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
wenzelm@40474
   192
wenzelm@34784
   193
wenzelm@43449
   194
  /* document model and view */
wenzelm@43449
   195
wenzelm@43449
   196
  def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
wenzelm@43449
   197
  def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
wenzelm@43449
   198
wenzelm@43449
   199
wenzelm@37068
   200
  /* dockable windows */
wenzelm@37068
   201
wenzelm@37068
   202
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@37068
   203
wenzelm@39515
   204
  def docked_session(view: View): Option[Session_Dockable] =
wenzelm@39515
   205
    wm(view).getDockableWindow("isabelle-session") match {
wenzelm@39515
   206
      case dockable: Session_Dockable => Some(dockable)
wenzelm@39515
   207
      case _ => None
wenzelm@39515
   208
    }
wenzelm@39515
   209
wenzelm@37068
   210
  def docked_output(view: View): Option[Output_Dockable] =
wenzelm@37068
   211
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@37068
   212
      case dockable: Output_Dockable => Some(dockable)
wenzelm@37068
   213
      case _ => None
wenzelm@37068
   214
    }
wenzelm@37068
   215
wenzelm@37068
   216
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
wenzelm@37068
   217
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@37068
   218
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@37068
   219
      case _ => None
wenzelm@37068
   220
    }
wenzelm@37068
   221
wenzelm@37068
   222
  def docked_protocol(view: View): Option[Protocol_Dockable] =
wenzelm@37068
   223
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@37068
   224
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@37068
   225
      case _ => None
wenzelm@37068
   226
    }
wenzelm@37068
   227
wenzelm@37068
   228
wenzelm@39517
   229
  /* logic image */
wenzelm@39517
   230
wenzelm@39517
   231
  def default_logic(): String =
wenzelm@39517
   232
  {
wenzelm@39517
   233
    val logic = system.getenv("JEDIT_LOGIC")
wenzelm@39517
   234
    if (logic != "") logic
wenzelm@39517
   235
    else system.getenv_strict("ISABELLE_LOGIC")
wenzelm@39517
   236
  }
wenzelm@39517
   237
wenzelm@39517
   238
  class Logic_Entry(val name: String, val description: String)
wenzelm@39517
   239
  {
wenzelm@39517
   240
    override def toString = description
wenzelm@39517
   241
  }
wenzelm@39517
   242
wenzelm@39517
   243
  def logic_selector(logic: String): ComboBox[Logic_Entry] =
wenzelm@39517
   244
  {
wenzelm@39517
   245
    val entries =
wenzelm@39517
   246
      new Logic_Entry("", "default (" + default_logic() + ")") ::
wenzelm@39517
   247
        system.find_logics().map(name => new Logic_Entry(name, name))
wenzelm@39517
   248
    val component = new ComboBox(entries)
wenzelm@39517
   249
    entries.find(_.name == logic) match {
wenzelm@39517
   250
      case None =>
wenzelm@39517
   251
      case Some(entry) => component.selection.item = entry
wenzelm@39517
   252
    }
wenzelm@39702
   253
    component.tooltip = "Isabelle logic image"
wenzelm@39517
   254
    component
wenzelm@39517
   255
  }
wenzelm@39702
   256
wenzelm@39702
   257
  def start_session()
wenzelm@39702
   258
  {
wenzelm@40852
   259
    val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
wenzelm@39702
   260
    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
wenzelm@39702
   261
    val logic = {
wenzelm@39702
   262
      val logic = Property("logic")
wenzelm@39702
   263
      if (logic != null && logic != "") logic
wenzelm@39702
   264
      else Isabelle.default_logic()
wenzelm@39702
   265
    }
wenzelm@40850
   266
    session.start(timeout, modes ::: List(logic))
wenzelm@39702
   267
  }
wenzelm@34318
   268
}
wenzelm@34318
   269
wenzelm@34429
   270
wenzelm@34618
   271
class Plugin extends EBPlugin
wenzelm@34618
   272
{
wenzelm@43443
   273
  /* extended syntax styles */
wenzelm@43443
   274
wenzelm@43443
   275
  @volatile var _extended_styles: Boolean = false
wenzelm@43443
   276
wenzelm@43443
   277
  private def check_extended_styles()
wenzelm@43443
   278
  {
wenzelm@43443
   279
    val family = jEdit.getProperty("view.font")
wenzelm@43443
   280
    val size = jEdit.getIntegerProperty("view.fontsize", 12)
wenzelm@43443
   281
    val styles = SyntaxUtilities.loadStyles(family, size)
wenzelm@43443
   282
    _extended_styles = (styles.length == JEditToken.ID_COUNT * 3 + 1)
wenzelm@43443
   283
  }
wenzelm@43443
   284
wenzelm@43443
   285
wenzelm@39630
   286
  /* session management */
wenzelm@39630
   287
wenzelm@39735
   288
  private def init_model(buffer: Buffer)
wenzelm@39630
   289
  {
wenzelm@39630
   290
    Isabelle.swing_buffer_lock(buffer) {
wenzelm@39735
   291
      val opt_model =
wenzelm@39735
   292
        Document_Model(buffer) match {
wenzelm@39735
   293
          case Some(model) => model.refresh; Some(model)
wenzelm@39735
   294
          case None =>
wenzelm@39735
   295
            Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
wenzelm@41537
   296
              case Some((dir, thy_name)) =>
wenzelm@41537
   297
                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
wenzelm@39735
   298
              case None => None
wenzelm@39735
   299
            }
wenzelm@39735
   300
        }
wenzelm@39735
   301
      if (opt_model.isDefined) {
wenzelm@39735
   302
        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
wenzelm@39735
   303
          if (Document_View(text_area).map(_.model) != opt_model)
wenzelm@39735
   304
            Document_View.init(opt_model.get, text_area)
wenzelm@39735
   305
        }
wenzelm@39630
   306
      }
wenzelm@39630
   307
    }
wenzelm@39630
   308
  }
wenzelm@39630
   309
wenzelm@39735
   310
  private def exit_model(buffer: Buffer)
wenzelm@39630
   311
  {
wenzelm@39630
   312
    Isabelle.swing_buffer_lock(buffer) {
wenzelm@39637
   313
      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
wenzelm@39637
   314
      Document_Model.exit(buffer)
wenzelm@39630
   315
    }
wenzelm@39630
   316
  }
wenzelm@39630
   317
wenzelm@39735
   318
  private case class Init_Model(buffer: Buffer)
wenzelm@39735
   319
  private case class Exit_Model(buffer: Buffer)
wenzelm@39741
   320
  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
wenzelm@39741
   321
  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
wenzelm@39735
   322
wenzelm@39633
   323
  private val session_manager = actor {
wenzelm@39735
   324
    var ready = false
wenzelm@39633
   325
    loop {
wenzelm@39633
   326
      react {
wenzelm@39735
   327
        case phase: Session.Phase =>
wenzelm@39735
   328
          ready = phase == Session.Ready
wenzelm@39735
   329
          phase match {
wenzelm@39735
   330
            case Session.Failed =>
wenzelm@39735
   331
              Swing_Thread.now {
wenzelm@39735
   332
                val text = new scala.swing.TextArea(Isabelle.session.syslog())
wenzelm@39735
   333
                text.editable = false
wenzelm@39735
   334
                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
wenzelm@39735
   335
              }
wenzelm@39735
   336
wenzelm@39735
   337
            case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
wenzelm@39735
   338
            case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
wenzelm@39735
   339
            case _ =>
wenzelm@39735
   340
          }
wenzelm@39735
   341
wenzelm@39735
   342
        case Init_Model(buffer) =>
wenzelm@39735
   343
          if (ready) init_model(buffer)
wenzelm@39630
   344
wenzelm@39735
   345
        case Exit_Model(buffer) =>
wenzelm@39735
   346
          exit_model(buffer)
wenzelm@39735
   347
wenzelm@39735
   348
        case Init_View(buffer, text_area) =>
wenzelm@39735
   349
          if (ready) {
wenzelm@39735
   350
            Isabelle.swing_buffer_lock(buffer) {
wenzelm@39735
   351
              Document_Model(buffer) match {
wenzelm@39735
   352
                case Some(model) => Document_View.init(model, text_area)
wenzelm@39735
   353
                case None =>
wenzelm@39735
   354
              }
wenzelm@39735
   355
            }
wenzelm@39735
   356
          }
wenzelm@39735
   357
wenzelm@39735
   358
        case Exit_View(buffer, text_area) =>
wenzelm@39735
   359
          Isabelle.swing_buffer_lock(buffer) {
wenzelm@39735
   360
            Document_View.exit(text_area)
wenzelm@39735
   361
          }
wenzelm@39735
   362
wenzelm@39735
   363
        case bad => System.err.println("session_manager: ignoring bad message " + bad)
wenzelm@39630
   364
      }
wenzelm@39630
   365
    }
wenzelm@39630
   366
  }
wenzelm@39630
   367
wenzelm@39630
   368
wenzelm@34618
   369
  /* main plugin plumbing */
wenzelm@34433
   370
wenzelm@34767
   371
  override def handleMessage(message: EBMessage)
wenzelm@34618
   372
  {
wenzelm@34767
   373
    message match {
wenzelm@41383
   374
      case msg: EditorStarted =>
wenzelm@41383
   375
      Isabelle.check_jvm()
wenzelm@43443
   376
      check_extended_styles()
wenzelm@41383
   377
      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
wenzelm@39630
   378
wenzelm@37557
   379
      case msg: BufferUpdate
wenzelm@39735
   380
      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
wenzelm@39634
   381
wenzelm@39633
   382
        val buffer = msg.getBuffer
wenzelm@39735
   383
        if (buffer != null) session_manager ! Init_Model(buffer)
wenzelm@37557
   384
wenzelm@39634
   385
      case msg: EditPaneUpdate
wenzelm@39735
   386
      if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
wenzelm@39637
   387
          msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
wenzelm@39634
   388
          msg.getWhat == EditPaneUpdate.CREATED ||
wenzelm@39634
   389
          msg.getWhat == EditPaneUpdate.DESTROYED) =>
wenzelm@39634
   390
wenzelm@34784
   391
        val edit_pane = msg.getEditPane
wenzelm@34784
   392
        val buffer = edit_pane.getBuffer
wenzelm@34784
   393
        val text_area = edit_pane.getTextArea
wenzelm@34784
   394
wenzelm@39637
   395
        if (buffer != null && text_area != null) {
wenzelm@39735
   396
          if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
wenzelm@39735
   397
              msg.getWhat == EditPaneUpdate.CREATED)
wenzelm@39735
   398
            session_manager ! Init_View(buffer, text_area)
wenzelm@39735
   399
          else
wenzelm@39735
   400
            session_manager ! Exit_View(buffer, text_area)
immler@34671
   401
        }
wenzelm@34784
   402
wenzelm@34777
   403
      case msg: PropertiesChanged =>
wenzelm@43390
   404
        Swing_Thread.now { Isabelle.setup_tooltips() }
wenzelm@34791
   405
        Isabelle.session.global_settings.event(Session.Global_Settings)
wenzelm@34784
   406
wenzelm@34318
   407
      case _ =>
wenzelm@34318
   408
    }
wenzelm@34318
   409
  }
wenzelm@34318
   410
wenzelm@34618
   411
  override def start()
wenzelm@34618
   412
  {
wenzelm@43443
   413
    Isabelle.plugin = this
wenzelm@39630
   414
    Isabelle.setup_tooltips()
wenzelm@34615
   415
    Isabelle.system = new Isabelle_System
wenzelm@34774
   416
    Isabelle.system.install_fonts()
wenzelm@39628
   417
    Isabelle.session = new Session(Isabelle.system)
wenzelm@39633
   418
    Isabelle.session.phase_changed += session_manager
wenzelm@34318
   419
  }
wenzelm@34618
   420
wenzelm@39628
   421
  override def stop()
wenzelm@34618
   422
  {
wenzelm@39628
   423
    Isabelle.session.stop()
wenzelm@39633
   424
    Isabelle.session.phase_changed -= session_manager
wenzelm@34318
   425
  }
wenzelm@34318
   426
}