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@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@39241: Buffer, EditPane, ServiceManager, View} immler@34406: import org.gjt.sp.jedit.buffer.JEditBuffer wenzelm@39043: import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} wenzelm@39633: import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} wenzelm@37068: import org.gjt.sp.jedit.gui.DockableWindowManager wenzelm@34429: 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@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@39043: /* text area ranges */ wenzelm@39043: wenzelm@39043: 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: "
" +  // FIXME proper scaling (!?)
wenzelm@37203:       HTML.encode(text) + "
" wenzelm@37201: wenzelm@38854: def tooltip_dismiss_delay(): Int = wenzelm@38854: Int_Property("tooltip-dismiss-delay", 8000) max 500 wenzelm@38854: wenzelm@38854: def setup_tooltips() wenzelm@38854: { wenzelm@38854: Swing_Thread.now { wenzelm@38854: val manager = javax.swing.ToolTipManager.sharedInstance wenzelm@38854: manager.setDismissDelay(tooltip_dismiss_delay()) 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@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@34784: 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@39517: val logic = system.getenv("JEDIT_LOGIC") wenzelm@39517: if (logic != "") logic wenzelm@39517: else 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@39517: 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@39702: val timeout = Int_Property("startup-timeout") max 1000 wenzelm@39702: val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.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@39702: session.start(timeout, modes ::: List(logic)) wenzelm@39702: } wenzelm@34318: } wenzelm@34318: wenzelm@34429: wenzelm@34618: class Plugin extends EBPlugin wenzelm@34618: { wenzelm@39630: /* session management */ wenzelm@39630: wenzelm@39735: private def init_model(buffer: Buffer) wenzelm@39630: { wenzelm@39630: Isabelle.swing_buffer_lock(buffer) { wenzelm@39735: val opt_model = wenzelm@39735: Document_Model(buffer) match { wenzelm@39735: case Some(model) => model.refresh; Some(model) wenzelm@39735: case None => wenzelm@39735: Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match { wenzelm@39735: case Some((_, thy_name)) => wenzelm@39735: Some(Document_Model.init(Isabelle.session, buffer, thy_name)) wenzelm@39735: case None => None wenzelm@39735: } wenzelm@39735: } wenzelm@39735: if (opt_model.isDefined) { wenzelm@39735: for (text_area <- Isabelle.jedit_text_areas(buffer)) { wenzelm@39735: if (Document_View(text_area).map(_.model) != opt_model) wenzelm@39735: Document_View.init(opt_model.get, text_area) wenzelm@39735: } wenzelm@39630: } wenzelm@39630: } wenzelm@39630: } wenzelm@39630: wenzelm@39735: private def exit_model(buffer: Buffer) wenzelm@39630: { wenzelm@39630: Isabelle.swing_buffer_lock(buffer) { wenzelm@39637: Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit) wenzelm@39637: Document_Model.exit(buffer) wenzelm@39630: } wenzelm@39630: } wenzelm@39630: wenzelm@39735: private case class Init_Model(buffer: Buffer) wenzelm@39735: private case class Exit_Model(buffer: Buffer) wenzelm@39741: private case class Init_View(buffer: Buffer, text_area: JEditTextArea) wenzelm@39741: private case class Exit_View(buffer: Buffer, text_area: JEditTextArea) wenzelm@39735: wenzelm@39633: private val session_manager = actor { wenzelm@39735: var ready = false wenzelm@39633: loop { wenzelm@39633: react { wenzelm@39735: case phase: Session.Phase => wenzelm@39735: ready = phase == Session.Ready 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@39735: case Session.Ready => Isabelle.jedit_buffers.foreach(init_model) wenzelm@39735: case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model) wenzelm@39735: case _ => wenzelm@39735: } wenzelm@39735: wenzelm@39735: case Init_Model(buffer) => wenzelm@39735: if (ready) init_model(buffer) wenzelm@39630: wenzelm@39735: case Exit_Model(buffer) => wenzelm@39735: exit_model(buffer) wenzelm@39735: wenzelm@39735: case Init_View(buffer, text_area) => wenzelm@39735: if (ready) { wenzelm@39735: Isabelle.swing_buffer_lock(buffer) { wenzelm@39735: Document_Model(buffer) match { wenzelm@39735: case Some(model) => Document_View.init(model, text_area) wenzelm@39735: case None => wenzelm@39735: } wenzelm@39735: } wenzelm@39735: } wenzelm@39735: wenzelm@39735: case Exit_View(buffer, text_area) => wenzelm@39735: Isabelle.swing_buffer_lock(buffer) { wenzelm@39735: Document_View.exit(text_area) wenzelm@39735: } 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@34767: message match { wenzelm@39702: case msg: EditorStarted wenzelm@39702: if Isabelle.Boolean_Property("auto-start") => 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@39735: if (buffer != null) session_manager ! 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@39735: msg.getWhat == EditPaneUpdate.CREATED) wenzelm@39735: session_manager ! Init_View(buffer, text_area) wenzelm@39735: else wenzelm@39735: session_manager ! Exit_View(buffer, text_area) immler@34671: } wenzelm@34784: wenzelm@34777: case msg: PropertiesChanged => wenzelm@37241: Swing_Thread.now { wenzelm@39630: Isabelle.setup_tooltips() 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@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@39630: Isabelle.setup_tooltips() wenzelm@34615: Isabelle.system = new Isabelle_System wenzelm@34774: Isabelle.system.install_fonts() wenzelm@39628: Isabelle.session = new Session(Isabelle.system) wenzelm@39633: Isabelle.session.phase_changed += session_manager wenzelm@34318: } wenzelm@34618: wenzelm@39628: override def stop() wenzelm@34618: { wenzelm@39628: Isabelle.session.stop() wenzelm@39633: Isabelle.session.phase_changed -= session_manager wenzelm@34318: } wenzelm@34318: }