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@34318: import java.awt.Font wenzelm@44573: import javax.swing.JOptionPane wenzelm@34318: wenzelm@34497: import scala.collection.mutable wenzelm@44606: import scala.swing.{ComboBox, ListView, ScrollPane} immler@34406: wenzelm@39241: import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, wenzelm@44577: Buffer, EditPane, 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@49099: import org.gjt.sp.jedit.msg.{EditorStarted, ViewUpdate, wenzelm@49099: BufferUpdate, EditPaneUpdate, PropertiesChanged} wenzelm@37068: import org.gjt.sp.jedit.gui.DockableWindowManager wenzelm@34429: wenzelm@43443: import org.gjt.sp.util.SyntaxUtilities wenzelm@39241: import org.gjt.sp.util.Log wenzelm@39241: wenzelm@44721: import scala.actors.Actor._ wenzelm@39630: wenzelm@34318: wenzelm@34618: object Isabelle wenzelm@34618: { wenzelm@34784: /* plugin instance */ wenzelm@34784: wenzelm@49099: @volatile var plugin: Plugin = null wenzelm@49099: @volatile var session: Session = null wenzelm@49099: @volatile var startup_failure: Option[Throwable] = None wenzelm@49099: @volatile var startup_notified = false wenzelm@34784: wenzelm@48870: def thy_load(): JEdit_Thy_Load = wenzelm@48870: session.thy_load.asInstanceOf[JEdit_Thy_Load] wenzelm@44955: wenzelm@48884: def get_recent_syntax(): Option[Outer_Syntax] = wenzelm@48884: { wenzelm@48884: val current_session = session wenzelm@48884: if (current_session != null) Some(current_session.recent_syntax) wenzelm@48884: else None wenzelm@48884: } wenzelm@48884: 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@37201: /* tooltip markup */ wenzelm@37201: wenzelm@37201: def tooltip(text: String): String = wenzelm@37203: "
" +  // FIXME proper scaling (!?)
wenzelm@37203:       HTML.encode(text) + "
" wenzelm@37201: wenzelm@44699: private val tooltip_lb = Time.seconds(0.5) wenzelm@44699: private val tooltip_ub = Time.seconds(60.0) wenzelm@40849: def tooltip_dismiss_delay(): Time = wenzelm@44699: Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub 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@44580: /* buffers */ wenzelm@44580: wenzelm@44580: def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = wenzelm@44580: Swing_Thread.now { buffer_lock(buffer) { body } } wenzelm@44580: wenzelm@44580: def buffer_text(buffer: JEditBuffer): String = wenzelm@44580: buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } wenzelm@44580: wenzelm@44580: def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath wenzelm@44580: wenzelm@48718: def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = wenzelm@48718: Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName)) wenzelm@48718: wenzelm@48718: def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = wenzelm@48718: { wenzelm@48718: val name = buffer_name(buffer) wenzelm@48718: Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) wenzelm@48718: } wenzelm@48718: wenzelm@44580: wenzelm@38221: /* main jEdit components */ wenzelm@34784: wenzelm@37177: def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator wenzelm@34784: wenzelm@44580: def jedit_buffer(name: String): Option[Buffer] = wenzelm@44580: jedit_buffers().find(buffer => buffer_name(buffer) == name) wenzelm@44580: 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@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@46997: doc_view = document_view(text_area) wenzelm@44379: if doc_view.isDefined wenzelm@44379: } yield doc_view.get wenzelm@44379: wenzelm@47058: def exit_model(buffer: Buffer) wenzelm@47058: { wenzelm@47058: swing_buffer_lock(buffer) { wenzelm@47058: jedit_text_areas(buffer).foreach(Document_View.exit) wenzelm@47058: Document_Model.exit(buffer) wenzelm@47058: } wenzelm@47058: } wenzelm@47058: wenzelm@43510: def init_model(buffer: Buffer) wenzelm@43510: { wenzelm@43510: swing_buffer_lock(buffer) { wenzelm@43510: val opt_model = wenzelm@48717: buffer_node_name(buffer) match { wenzelm@48717: case Some(node_name) => wenzelm@47058: document_model(buffer) match { wenzelm@47058: case Some(model) if model.name == node_name => Some(model) wenzelm@47058: case _ => Some(Document_Model.init(session, buffer, node_name)) wenzelm@43510: } wenzelm@47058: case None => None 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 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@48870: def session_args(): List[String] = wenzelm@39702: { 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@48870: modes ::: List(logic) wenzelm@48870: } wenzelm@48870: wenzelm@49098: def session_content(inlined_files: Boolean): Build.Session_Content = wenzelm@48870: { wenzelm@48870: val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) wenzelm@48870: val name = Path.explode(session_args().last).base.implode // FIXME more robust wenzelm@49098: Build.session_content(inlined_files, dirs, name).check_errors 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@44864: wenzelm@44864: def check_buffer(buffer: Buffer) wenzelm@44864: { wenzelm@44864: document_model(buffer) match { wenzelm@44864: case None => wenzelm@44864: case Some(model) => model.full_perspective() wenzelm@44864: } wenzelm@44864: } wenzelm@44864: wenzelm@44864: def cancel_execution() { session.cancel_execution() } wenzelm@34318: } wenzelm@34318: wenzelm@34429: wenzelm@34618: class Plugin extends EBPlugin wenzelm@34618: { wenzelm@44577: /* theory files */ wenzelm@44574: wenzelm@44573: private lazy val delay_load = wenzelm@44574: Swing_Thread.delay_last(Isabelle.session.load_delay) wenzelm@44574: { wenzelm@44963: val view = jEdit.getActiveView() wenzelm@44963: wenzelm@44574: val buffers = Isabelle.jedit_buffers().toList wenzelm@46761: if (buffers.forall(_.isLoaded)) { wenzelm@46761: def loaded_buffer(name: String): Boolean = wenzelm@46761: buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) wenzelm@44574: wenzelm@46761: val thys = wenzelm@46761: for (buffer <- buffers; model <- Isabelle.document_model(buffer)) wenzelm@46761: yield model.name wenzelm@46761: wenzelm@48870: val thy_info = new Thy_Info(Isabelle.thy_load) wenzelm@46761: // FIXME avoid I/O in Swing thread!?! wenzelm@49098: val files = thy_info.dependencies(true, thys).deps.map(_._1.node). wenzelm@46761: filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file)) wenzelm@44574: wenzelm@46761: if (!files.isEmpty) { wenzelm@46761: val files_list = new ListView(files.sorted) wenzelm@46761: for (i <- 0 until files.length) wenzelm@46761: files_list.selection.indices += i wenzelm@44606: wenzelm@46761: val answer = wenzelm@46761: Library.confirm_dialog(view, wenzelm@46761: "Auto loading of required files", wenzelm@46761: JOptionPane.YES_NO_OPTION, wenzelm@46761: "The following files are required to resolve theory imports.", wenzelm@46761: "Reload selected files now?", wenzelm@46761: new ScrollPane(files_list)) wenzelm@46761: if (answer == 0) { wenzelm@46761: files.foreach(file => wenzelm@46761: if (files_list.selection.items.contains(file)) wenzelm@46761: jEdit.openFile(null: View, file)) wenzelm@46761: } wenzelm@46761: } wenzelm@44606: } wenzelm@44574: } wenzelm@44573: wenzelm@44574: wenzelm@44574: /* session manager */ wenzelm@44573: 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@46918: Swing_Thread.later { wenzelm@48022: Library.error_dialog(jEdit.getActiveView, "Prover process failure", wenzelm@48022: "Isabelle Syslog", Library.scrollable_text(Isabelle.session.current_syslog())) wenzelm@39735: } wenzelm@39735: wenzelm@44573: case Session.Ready => wenzelm@44573: Isabelle.jedit_buffers.foreach(Isabelle.init_model) wenzelm@46740: delay_load(true) wenzelm@44573: wenzelm@46740: case Session.Shutdown => wenzelm@46740: Isabelle.jedit_buffers.foreach(Isabelle.exit_model) wenzelm@46740: delay_load(false) wenzelm@46740: 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@39630: wenzelm@49099: if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) { wenzelm@49099: message match { wenzelm@49099: case msg: ViewUpdate => wenzelm@49099: Library.error_dialog(msg.getView, "Isabelle plugin startup failure", wenzelm@49099: Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)), wenzelm@49099: "Prover IDE inactive!") wenzelm@49099: Isabelle.startup_notified = true wenzelm@49099: case _ => wenzelm@49099: } wenzelm@49099: } wenzelm@49099: wenzelm@49099: if (Isabelle.startup_failure.isEmpty) { wenzelm@49099: message match { wenzelm@49099: case msg: EditorStarted => wenzelm@49099: if (Isabelle.Boolean_Property("auto-start")) wenzelm@49099: Isabelle.session.start(Isabelle.session_args()) wenzelm@37557: wenzelm@49099: case msg: BufferUpdate wenzelm@49099: if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => wenzelm@49099: if (Isabelle.session.is_ready) { wenzelm@49099: val buffer = msg.getBuffer wenzelm@49099: if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer) wenzelm@49099: delay_load(true) wenzelm@49099: } wenzelm@34784: wenzelm@49099: case msg: EditPaneUpdate wenzelm@49099: if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || wenzelm@49099: msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || wenzelm@49099: msg.getWhat == EditPaneUpdate.CREATED || wenzelm@49099: msg.getWhat == EditPaneUpdate.DESTROYED) => wenzelm@49099: val edit_pane = msg.getEditPane wenzelm@49099: val buffer = edit_pane.getBuffer wenzelm@49099: val text_area = edit_pane.getTextArea wenzelm@49099: wenzelm@49099: if (buffer != null && text_area != null) { wenzelm@49099: if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || wenzelm@49099: msg.getWhat == EditPaneUpdate.CREATED) { wenzelm@49099: if (Isabelle.session.is_ready) wenzelm@49099: Isabelle.init_view(buffer, text_area) wenzelm@49099: } wenzelm@49099: else Isabelle.exit_view(buffer, text_area) wenzelm@43510: } wenzelm@34784: wenzelm@49099: case msg: PropertiesChanged => wenzelm@49099: Isabelle.setup_tooltips() wenzelm@49099: Isabelle.session.global_settings.event(Session.Global_Settings) wenzelm@34784: wenzelm@49099: case _ => wenzelm@49099: } wenzelm@34318: } wenzelm@34318: } wenzelm@34318: wenzelm@34618: override def start() wenzelm@49099: { wenzelm@49099: try { wenzelm@49099: Isabelle.plugin = this wenzelm@49099: Isabelle.setup_tooltips() wenzelm@49099: Isabelle_System.init() wenzelm@49099: Isabelle_System.install_fonts() wenzelm@49099: wenzelm@49099: SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) wenzelm@49099: if (ModeProvider.instance.isInstanceOf[ModeProvider]) wenzelm@49099: ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) wenzelm@48870: wenzelm@49099: val content = Isabelle.session_content(false) wenzelm@49099: val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax) wenzelm@49099: Isabelle.session = new Session(thy_load) wenzelm@48870: wenzelm@49099: Isabelle.session.phase_changed += session_manager wenzelm@49099: Isabelle.startup_failure = None wenzelm@49099: } wenzelm@49099: catch { wenzelm@49099: case exn: Throwable => wenzelm@49099: stop() wenzelm@49099: Isabelle.session = null wenzelm@49099: Isabelle.startup_failure = Some(exn) wenzelm@49099: Isabelle.startup_notified = false wenzelm@49099: } wenzelm@34318: } wenzelm@34618: wenzelm@39628: override def stop() wenzelm@34618: { wenzelm@49099: if (Isabelle.session != null) { wenzelm@49099: Isabelle.session.phase_changed -= session_manager wenzelm@49099: Isabelle.jedit_buffers.foreach(Isabelle.exit_model) wenzelm@49099: Isabelle.session.stop() wenzelm@49099: } wenzelm@34318: } wenzelm@34318: }