wenzelm@43282: /*  Title:      Tools/jEdit/src/plugin.scala
wenzelm@36760:     Author:     Makarius
wenzelm@36760: 
wenzelm@36760: Main Isabelle/jEdit plugin setup.
wenzelm@36760: */
wenzelm@34407: 
wenzelm@34318: package isabelle.jedit
wenzelm@34318: 
wenzelm@34429: 
wenzelm@36015: import isabelle._
wenzelm@36015: 
wenzelm@43520: import java.lang.System
wenzelm@43645: import java.io.{File, FileInputStream, IOException}
wenzelm@34318: import java.awt.Font
wenzelm@34318: 
wenzelm@34497: import scala.collection.mutable
wenzelm@39517: import scala.swing.ComboBox
immler@34406: 
wenzelm@39241: import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
wenzelm@43645:   Buffer, EditPane, MiscUtilities, ServiceManager, View}
immler@34406: import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@39043: import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
wenzelm@43452: import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
wenzelm@39633: import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
wenzelm@37068: import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@44160: import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
wenzelm@34429: 
wenzelm@43443: import org.gjt.sp.util.SyntaxUtilities
wenzelm@39241: import org.gjt.sp.util.Log
wenzelm@39241: 
wenzelm@39630: import scala.actors.Actor
wenzelm@39630: import Actor._
wenzelm@39630: 
wenzelm@34318: 
wenzelm@34618: object Isabelle
wenzelm@34618: {
wenzelm@34784:   /* plugin instance */
wenzelm@34784: 
wenzelm@43443:   var plugin: Plugin = null
wenzelm@34784:   var session: Session = null
wenzelm@34784: 
wenzelm@34784: 
wenzelm@34618:   /* properties */
wenzelm@34618: 
wenzelm@34618:   val OPTION_PREFIX = "options.isabelle."
wenzelm@34618: 
wenzelm@34618:   object Property
wenzelm@34618:   {
wenzelm@36814:     def apply(name: String): String =
wenzelm@36814:       jEdit.getProperty(OPTION_PREFIX + name)
wenzelm@36814:     def apply(name: String, default: String): String =
wenzelm@36814:       jEdit.getProperty(OPTION_PREFIX + name, default)
wenzelm@36814:     def update(name: String, value: String) =
wenzelm@36814:       jEdit.setProperty(OPTION_PREFIX + name, value)
wenzelm@34468:   }
wenzelm@34433: 
wenzelm@34618:   object Boolean_Property
wenzelm@34618:   {
wenzelm@36814:     def apply(name: String): Boolean =
wenzelm@36814:       jEdit.getBooleanProperty(OPTION_PREFIX + name)
wenzelm@36814:     def apply(name: String, default: Boolean): Boolean =
wenzelm@36814:       jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
wenzelm@36814:     def update(name: String, value: Boolean) =
wenzelm@36814:       jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
wenzelm@34618:   }
wenzelm@34618: 
wenzelm@34618:   object Int_Property
wenzelm@34618:   {
wenzelm@36814:     def apply(name: String): Int =
wenzelm@36814:       jEdit.getIntegerProperty(OPTION_PREFIX + name)
wenzelm@36814:     def apply(name: String, default: Int): Int =
wenzelm@36814:       jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
wenzelm@36814:     def update(name: String, value: Int) =
wenzelm@36814:       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
wenzelm@34618:   }
wenzelm@34618: 
wenzelm@40848:   object Double_Property
wenzelm@40848:   {
wenzelm@40848:     def apply(name: String): Double =
wenzelm@40848:       jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
wenzelm@40848:     def apply(name: String, default: Double): Double =
wenzelm@40848:       jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
wenzelm@40848:     def update(name: String, value: Double) =
wenzelm@40848:       jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
wenzelm@40848:   }
wenzelm@40848: 
wenzelm@40850:   object Time_Property
wenzelm@40850:   {
wenzelm@40850:     def apply(name: String): Time =
wenzelm@40850:       Time.seconds(Double_Property(name))
wenzelm@40850:     def apply(name: String, default: Time): Time =
wenzelm@40850:       Time.seconds(Double_Property(name, default.seconds))
wenzelm@40850:     def update(name: String, value: Time) =
wenzelm@40850:       Double_Property.update(name, value.seconds)
wenzelm@40850:   }
wenzelm@40850: 
wenzelm@40848: 
wenzelm@37164:   /* font */
wenzelm@37164: 
wenzelm@37164:   def font_family(): String = jEdit.getProperty("view.font")
wenzelm@37164: 
wenzelm@37019:   def font_size(): Float =
wenzelm@37019:     (jEdit.getIntegerProperty("view.fontsize", 16) *
wenzelm@37019:       Int_Property("relative-font-size", 100)).toFloat / 100
wenzelm@36814: 
wenzelm@34618: 
wenzelm@39043:   /* text area ranges */
wenzelm@39043: 
wenzelm@43714:   sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
wenzelm@39043: 
wenzelm@39043:   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
wenzelm@39043:   {
wenzelm@39043:     val p = text_area.offsetToXY(range.start)
wenzelm@39043:     val q = text_area.offsetToXY(range.stop)
wenzelm@39043:     if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
wenzelm@39043:     else None
wenzelm@39043:   }
wenzelm@39043: 
wenzelm@39043: 
wenzelm@37201:   /* tooltip markup */
wenzelm@37201: 
wenzelm@37201:   def tooltip(text: String): String =
wenzelm@37203:     "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
wenzelm@37203:         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
wenzelm@37203:       HTML.encode(text) + "</pre></html>"
wenzelm@37201: 
wenzelm@40849:   def tooltip_dismiss_delay(): Time =
wenzelm@40852:     Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
wenzelm@38854: 
wenzelm@38854:   def setup_tooltips()
wenzelm@38854:   {
wenzelm@38854:     Swing_Thread.now {
wenzelm@38854:       val manager = javax.swing.ToolTipManager.sharedInstance
wenzelm@40849:       manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
wenzelm@38854:     }
wenzelm@38854:   }
wenzelm@38854: 
wenzelm@37201: 
wenzelm@39241:   /* icons */
wenzelm@39241: 
wenzelm@39241:   def load_icon(name: String): javax.swing.Icon =
wenzelm@39241:   {
wenzelm@39241:     val icon = GUIUtilities.loadIcon(name)
wenzelm@39241:     if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
wenzelm@39630:       Log.log(Log.ERROR, icon, "Bad icon: " + name)
wenzelm@39241:     icon
wenzelm@39241:   }
wenzelm@39241: 
wenzelm@39241: 
wenzelm@41382:   /* check JVM */
wenzelm@41382: 
wenzelm@41382:   def check_jvm()
wenzelm@41382:   {
wenzelm@41382:     if (!Platform.is_hotspot) {
wenzelm@41382:       Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
wenzelm@41382:         "This is " + Platform.jvm_name,
wenzelm@41382:         "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
wenzelm@41382:     }
wenzelm@41382:   }
wenzelm@41382: 
wenzelm@41382: 
wenzelm@38221:   /* main jEdit components */
wenzelm@34784: 
wenzelm@37177:   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
wenzelm@34784: 
wenzelm@37177:   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
wenzelm@34784: 
wenzelm@34784:   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
wenzelm@37177:     view.getEditPanes().iterator.map(_.getTextArea)
wenzelm@34784: 
wenzelm@34784:   def jedit_text_areas(): Iterator[JEditTextArea] =
wenzelm@34784:     jedit_views().flatMap(jedit_text_areas(_))
wenzelm@34784: 
wenzelm@34784:   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
wenzelm@34784:     jedit_text_areas().filter(_.getBuffer == buffer)
wenzelm@34784: 
wenzelm@38843:   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@38640:   {
wenzelm@38640:     try { buffer.readLock(); body }
wenzelm@38640:     finally { buffer.readUnlock() }
wenzelm@38640:   }
wenzelm@38640: 
wenzelm@38843:   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@38843:     Swing_Thread.now { buffer_lock(buffer) { body } }
wenzelm@38843: 
wenzelm@40474:   def buffer_text(buffer: JEditBuffer): String =
wenzelm@40474:     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
wenzelm@40474: 
wenzelm@44160:   def buffer_path(buffer: Buffer): (String, String) =
wenzelm@44160:   {
wenzelm@44160:     val master_dir = buffer.getDirectory
wenzelm@44160:     val path = buffer.getSymlinkPath
wenzelm@44225:     (master_dir, path)
wenzelm@44160:   }
wenzelm@44160: 
wenzelm@34784: 
wenzelm@43449:   /* document model and view */
wenzelm@43449: 
wenzelm@43449:   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
wenzelm@43449:   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
wenzelm@43449: 
wenzelm@44379:   def document_views(buffer: Buffer): List[Document_View] =
wenzelm@44379:     for {
wenzelm@44379:       text_area <- jedit_text_areas(buffer).toList
wenzelm@44379:       val doc_view = document_view(text_area)
wenzelm@44379:       if doc_view.isDefined
wenzelm@44379:     } yield doc_view.get
wenzelm@44379: 
wenzelm@43510:   def init_model(buffer: Buffer)
wenzelm@43510:   {
wenzelm@43510:     swing_buffer_lock(buffer) {
wenzelm@43510:       val opt_model =
wenzelm@43510:         document_model(buffer) match {
wenzelm@43510:           case Some(model) => Some(model)
wenzelm@43510:           case None =>
wenzelm@44160:             val (master_dir, path) = buffer_path(buffer)
wenzelm@44160:             Thy_Header.thy_name(path) match {
wenzelm@44222:               case Some(name) =>
wenzelm@44222:                 Some(Document_Model.init(session, buffer, master_dir, path, name))
wenzelm@44160:               case None => None
wenzelm@43510:             }
wenzelm@43510:         }
wenzelm@43510:       if (opt_model.isDefined) {
wenzelm@43510:         for (text_area <- jedit_text_areas(buffer)) {
wenzelm@43510:           if (document_view(text_area).map(_.model) != opt_model)
wenzelm@43510:             Document_View.init(opt_model.get, text_area)
wenzelm@43510:         }
wenzelm@43510:       }
wenzelm@43510:     }
wenzelm@43510:   }
wenzelm@43510: 
wenzelm@43510:   def exit_model(buffer: Buffer)
wenzelm@43510:   {
wenzelm@43510:     swing_buffer_lock(buffer) {
wenzelm@43510:       jedit_text_areas(buffer).foreach(Document_View.exit)
wenzelm@43510:       Document_Model.exit(buffer)
wenzelm@43510:     }
wenzelm@43510:   }
wenzelm@43510: 
wenzelm@43510:   def init_view(buffer: Buffer, text_area: JEditTextArea)
wenzelm@43510:   {
wenzelm@43510:     swing_buffer_lock(buffer) {
wenzelm@43510:       document_model(buffer) match {
wenzelm@43510:         case Some(model) => Document_View.init(model, text_area)
wenzelm@43510:         case None =>
wenzelm@43510:       }
wenzelm@43510:     }
wenzelm@43510:   }
wenzelm@43510: 
wenzelm@43510:   def exit_view(buffer: Buffer, text_area: JEditTextArea)
wenzelm@43510:   {
wenzelm@43510:     swing_buffer_lock(buffer) {
wenzelm@43510:       Document_View.exit(text_area)
wenzelm@43510:     }
wenzelm@43510:   }
wenzelm@43510: 
wenzelm@43449: 
wenzelm@37068:   /* dockable windows */
wenzelm@37068: 
wenzelm@37068:   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@37068: 
wenzelm@39515:   def docked_session(view: View): Option[Session_Dockable] =
wenzelm@39515:     wm(view).getDockableWindow("isabelle-session") match {
wenzelm@39515:       case dockable: Session_Dockable => Some(dockable)
wenzelm@39515:       case _ => None
wenzelm@39515:     }
wenzelm@39515: 
wenzelm@37068:   def docked_output(view: View): Option[Output_Dockable] =
wenzelm@37068:     wm(view).getDockableWindow("isabelle-output") match {
wenzelm@37068:       case dockable: Output_Dockable => Some(dockable)
wenzelm@37068:       case _ => None
wenzelm@37068:     }
wenzelm@37068: 
wenzelm@37068:   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
wenzelm@37068:     wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@37068:       case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@37068:       case _ => None
wenzelm@37068:     }
wenzelm@37068: 
wenzelm@37068:   def docked_protocol(view: View): Option[Protocol_Dockable] =
wenzelm@37068:     wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@37068:       case dockable: Protocol_Dockable => Some(dockable)
wenzelm@37068:       case _ => None
wenzelm@37068:     }
wenzelm@37068: 
wenzelm@37068: 
wenzelm@39517:   /* logic image */
wenzelm@39517: 
wenzelm@39517:   def default_logic(): String =
wenzelm@39517:   {
wenzelm@43661:     val logic = Isabelle_System.getenv("JEDIT_LOGIC")
wenzelm@39517:     if (logic != "") logic
wenzelm@43661:     else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
wenzelm@39517:   }
wenzelm@39517: 
wenzelm@39517:   class Logic_Entry(val name: String, val description: String)
wenzelm@39517:   {
wenzelm@39517:     override def toString = description
wenzelm@39517:   }
wenzelm@39517: 
wenzelm@39517:   def logic_selector(logic: String): ComboBox[Logic_Entry] =
wenzelm@39517:   {
wenzelm@39517:     val entries =
wenzelm@39517:       new Logic_Entry("", "default (" + default_logic() + ")") ::
wenzelm@43661:         Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
wenzelm@39517:     val component = new ComboBox(entries)
wenzelm@39517:     entries.find(_.name == logic) match {
wenzelm@39517:       case None =>
wenzelm@39517:       case Some(entry) => component.selection.item = entry
wenzelm@39517:     }
wenzelm@39702:     component.tooltip = "Isabelle logic image"
wenzelm@39517:     component
wenzelm@39517:   }
wenzelm@39702: 
wenzelm@39702:   def start_session()
wenzelm@39702:   {
wenzelm@40852:     val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
wenzelm@43670:     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
wenzelm@39702:     val logic = {
wenzelm@39702:       val logic = Property("logic")
wenzelm@39702:       if (logic != null && logic != "") logic
wenzelm@39702:       else Isabelle.default_logic()
wenzelm@39702:     }
wenzelm@40850:     session.start(timeout, modes ::: List(logic))
wenzelm@39702:   }
wenzelm@44238: 
wenzelm@44238: 
wenzelm@44238:   /* convenience actions */
wenzelm@44238: 
wenzelm@44238:   private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
wenzelm@44238:   {
wenzelm@44238:     s1.foreach(text_area.userInput(_))
wenzelm@44238:     s2.foreach(text_area.userInput(_))
wenzelm@44238:     s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@44238:   }
wenzelm@44238: 
wenzelm@44238:   def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
wenzelm@44238:   def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
wenzelm@44238:   def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
wenzelm@44238:   def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
wenzelm@44238:   def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
wenzelm@44238:   def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
wenzelm@44238:   def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
wenzelm@34318: }
wenzelm@34318: 
wenzelm@34429: 
wenzelm@34618: class Plugin extends EBPlugin
wenzelm@34618: {
wenzelm@43645:   /* editor file store */
wenzelm@43645: 
wenzelm@43645:   private val file_store = new Session.File_Store
wenzelm@43645:   {
wenzelm@44185:     def append(master_dir: String, source_path: Path): String =
wenzelm@43645:     {
wenzelm@44185:       val path = source_path.expand
wenzelm@44185:       if (path.is_absolute) Isabelle_System.platform_path(path)
wenzelm@44185:       else {
wenzelm@44185:         val vfs = VFSManager.getVFSForPath(master_dir)
wenzelm@44185:         if (vfs.isInstanceOf[FileVFS])
wenzelm@44222:           MiscUtilities.resolveSymlinks(
wenzelm@44222:             vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
wenzelm@44185:         else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
wenzelm@44185:       }
wenzelm@44163:     }
wenzelm@43645: 
wenzelm@44163:     def require(canonical_name: String)
wenzelm@44163:     {
wenzelm@44163:       Swing_Thread.later {
wenzelm@44163:         if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
wenzelm@44163:           jEdit.openFile(null: View, canonical_name)
wenzelm@43645:       }
wenzelm@43645:     }
wenzelm@43645:   }
wenzelm@43645: 
wenzelm@43645: 
wenzelm@43645:   /* session manager */
wenzelm@39630: 
wenzelm@39633:   private val session_manager = actor {
wenzelm@39633:     loop {
wenzelm@39633:       react {
wenzelm@39735:         case phase: Session.Phase =>
wenzelm@39735:           phase match {
wenzelm@39735:             case Session.Failed =>
wenzelm@39735:               Swing_Thread.now {
wenzelm@39735:                 val text = new scala.swing.TextArea(Isabelle.session.syslog())
wenzelm@39735:                 text.editable = false
wenzelm@39735:                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
wenzelm@39735:               }
wenzelm@39735: 
wenzelm@43510:             case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
wenzelm@43510:             case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
wenzelm@39735:             case _ =>
wenzelm@39735:           }
wenzelm@39735:         case bad => System.err.println("session_manager: ignoring bad message " + bad)
wenzelm@39630:       }
wenzelm@39630:     }
wenzelm@39630:   }
wenzelm@39630: 
wenzelm@39630: 
wenzelm@34618:   /* main plugin plumbing */
wenzelm@34433: 
wenzelm@34767:   override def handleMessage(message: EBMessage)
wenzelm@34618:   {
wenzelm@43510:     Swing_Thread.assert()
wenzelm@34767:     message match {
wenzelm@41383:       case msg: EditorStarted =>
wenzelm@43510:         Isabelle.check_jvm()
wenzelm@43510:         if (Isabelle.Boolean_Property("auto-start"))
wenzelm@43510:           Isabelle.start_session()
wenzelm@39630: 
wenzelm@37557:       case msg: BufferUpdate
wenzelm@39735:       if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
wenzelm@39634: 
wenzelm@39633:         val buffer = msg.getBuffer
wenzelm@43643:         if (buffer != null && Isabelle.session.is_ready)
wenzelm@43510:           Isabelle.init_model(buffer)
wenzelm@37557: 
wenzelm@39634:       case msg: EditPaneUpdate
wenzelm@39735:       if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
wenzelm@39637:           msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
wenzelm@39634:           msg.getWhat == EditPaneUpdate.CREATED ||
wenzelm@39634:           msg.getWhat == EditPaneUpdate.DESTROYED) =>
wenzelm@39634: 
wenzelm@34784:         val edit_pane = msg.getEditPane
wenzelm@34784:         val buffer = edit_pane.getBuffer
wenzelm@34784:         val text_area = edit_pane.getTextArea
wenzelm@34784: 
wenzelm@39637:         if (buffer != null && text_area != null) {
wenzelm@39735:           if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
wenzelm@43510:               msg.getWhat == EditPaneUpdate.CREATED) {
wenzelm@43643:             if (Isabelle.session.is_ready)
wenzelm@43510:               Isabelle.init_view(buffer, text_area)
wenzelm@43510:           }
wenzelm@43510:           else Isabelle.exit_view(buffer, text_area)
immler@34671:         }
wenzelm@34784: 
wenzelm@34777:       case msg: PropertiesChanged =>
wenzelm@43390:         Swing_Thread.now { Isabelle.setup_tooltips() }
wenzelm@34791:         Isabelle.session.global_settings.event(Session.Global_Settings)
wenzelm@34784: 
wenzelm@34318:       case _ =>
wenzelm@34318:     }
wenzelm@34318:   }
wenzelm@34318: 
wenzelm@34618:   override def start()
wenzelm@34618:   {
wenzelm@43443:     Isabelle.plugin = this
wenzelm@39630:     Isabelle.setup_tooltips()
wenzelm@43661:     Isabelle_System.init()
wenzelm@43661:     Isabelle_System.install_fonts()
wenzelm@43661:     Isabelle.session = new Session(file_store)
wenzelm@43661:     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
wenzelm@43513:     if (ModeProvider.instance.isInstanceOf[ModeProvider])
wenzelm@43513:       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
wenzelm@39633:     Isabelle.session.phase_changed += session_manager
wenzelm@34318:   }
wenzelm@34618: 
wenzelm@39628:   override def stop()
wenzelm@34618:   {
wenzelm@43513:     Isabelle.session.phase_changed -= session_manager
wenzelm@43513:     Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
wenzelm@39628:     Isabelle.session.stop()
wenzelm@34318:   }
wenzelm@34318: }