wenzelm@36760: /* Title: Tools/jEdit/src/jedit/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@34429: import java.io.{FileInputStream, IOException} wenzelm@34318: import java.awt.Font wenzelm@34822: import javax.swing.JTextArea wenzelm@34318: wenzelm@34497: import scala.collection.mutable immler@34406: wenzelm@34429: import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View} immler@34406: import org.gjt.sp.jedit.buffer.JEditBuffer immler@34406: import org.gjt.sp.jedit.textarea.JEditTextArea wenzelm@37557: import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged} wenzelm@37068: import org.gjt.sp.jedit.gui.DockableWindowManager wenzelm@34429: wenzelm@34318: wenzelm@34618: object Isabelle wenzelm@34618: { wenzelm@34784: /* plugin instance */ wenzelm@34784: wenzelm@34784: var system: Isabelle_System = 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@37164: 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@37201: wenzelm@34618: /* settings */ wenzelm@34618: wenzelm@34782: def default_logic(): String = wenzelm@34782: { wenzelm@34782: val logic = system.getenv("JEDIT_LOGIC") wenzelm@34782: if (logic != "") logic wenzelm@34782: else system.getenv_strict("ISABELLE_LOGIC") wenzelm@34782: } wenzelm@34782: wenzelm@34782: def isabelle_args(): List[String] = wenzelm@34618: { wenzelm@34780: val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) wenzelm@34780: val logic = { wenzelm@34784: val logic = Property("logic") wenzelm@34782: if (logic != null && logic != "") logic wenzelm@34782: else default_logic() wenzelm@34780: } wenzelm@34780: modes ++ List(logic) wenzelm@34502: } wenzelm@34502: wenzelm@34618: 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@38640: def buffer_read_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@37068: /* dockable windows */ wenzelm@37068: wenzelm@37068: private def wm(view: View): DockableWindowManager = view.getDockableWindowManager wenzelm@37068: 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@38221: /* manage prover */ // FIXME async!? wenzelm@34820: wenzelm@34820: private def prover_started(view: View): Boolean = wenzelm@34820: { wenzelm@34820: val timeout = Int_Property("startup-timeout") max 1000 wenzelm@38221: session.started(timeout, Isabelle.isabelle_args()) match { wenzelm@34820: case Some(err) => wenzelm@34822: val text = new JTextArea(err); text.setEditable(false) wenzelm@34822: Library.error_dialog(view, null, "Failed to start Isabelle process", text) wenzelm@34820: false wenzelm@34820: case None => true wenzelm@34820: } wenzelm@34820: } wenzelm@34820: wenzelm@34820: wenzelm@34784: /* activation */ wenzelm@34784: wenzelm@34820: def activate_buffer(view: View, buffer: Buffer) wenzelm@34784: { wenzelm@34820: if (prover_started(view)) { wenzelm@38222: // FIXME proper error handling wenzelm@38222: val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) wenzelm@38222: wenzelm@38222: val model = Document_Model.init(session, buffer, thy_name) wenzelm@34820: for (text_area <- jedit_text_areas(buffer)) wenzelm@34820: Document_View.init(model, text_area) wenzelm@34820: } wenzelm@34784: } wenzelm@34784: wenzelm@34784: def deactivate_buffer(buffer: Buffer) wenzelm@34784: { wenzelm@34784: session.stop() // FIXME not yet wenzelm@34784: wenzelm@34784: for (text_area <- jedit_text_areas(buffer)) wenzelm@34784: Document_View.exit(text_area) wenzelm@34784: Document_Model.exit(buffer) wenzelm@34784: } wenzelm@34784: wenzelm@34784: def switch_active(view: View) = wenzelm@34784: { wenzelm@34784: val buffer = view.getBuffer wenzelm@34788: if (Document_Model(buffer).isDefined) deactivate_buffer(buffer) wenzelm@34820: else activate_buffer(view, buffer) wenzelm@34784: } wenzelm@34784: wenzelm@34784: def is_active(view: View): Boolean = wenzelm@34788: Document_Model(view.getBuffer).isDefined wenzelm@34318: } wenzelm@34318: wenzelm@34429: wenzelm@34618: class Plugin extends EBPlugin wenzelm@34618: { wenzelm@34618: /* main plugin plumbing */ wenzelm@34433: wenzelm@34767: override def handleMessage(message: EBMessage) wenzelm@34618: { wenzelm@34767: message match { wenzelm@37557: case msg: BufferUpdate wenzelm@37557: if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => wenzelm@37557: Document_Model(msg.getBuffer) match { wenzelm@37557: case Some(model) => model.refresh() wenzelm@37557: case _ => wenzelm@37557: } wenzelm@37557: wenzelm@34767: case msg: EditPaneUpdate => 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@34787: def init_view() wenzelm@34787: { wenzelm@34788: Document_Model(buffer) match { wenzelm@34787: case Some(model) => Document_View.init(model, text_area) wenzelm@34787: case None => wenzelm@34787: } wenzelm@34787: } wenzelm@34787: def exit_view() wenzelm@34787: { wenzelm@34788: if (Document_View(text_area).isDefined) wenzelm@34787: Document_View.exit(text_area) wenzelm@34787: } wenzelm@34767: msg.getWhat match { wenzelm@34787: case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view() wenzelm@34787: case EditPaneUpdate.CREATED => init_view() wenzelm@34787: case EditPaneUpdate.DESTROYED => exit_view() immler@34671: case _ => immler@34671: } wenzelm@34784: wenzelm@34777: case msg: PropertiesChanged => wenzelm@37241: Swing_Thread.now { wenzelm@37241: for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined) wenzelm@37241: Document_View(text_area).get.extend_styles() wenzelm@37241: } wenzelm@37241: 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@34615: Isabelle.system = new Isabelle_System wenzelm@34774: Isabelle.system.install_fonts() wenzelm@34777: Isabelle.session = new Session(Isabelle.system) // FIXME dialog!? wenzelm@34318: } wenzelm@34618: wenzelm@34618: override def stop() wenzelm@34618: { wenzelm@34777: Isabelle.session.stop() // FIXME dialog!? wenzelm@34777: Isabelle.session = null wenzelm@34441: Isabelle.system = null wenzelm@34318: } wenzelm@34318: }