wneuper/isa: src/Tools/jEdit/src/plugin.scala@395b7277ed76

     1 /*  Title:      Tools/jEdit/src/plugin.scala

     2     Author:     Makarius

     4 Main Isabelle/jEdit plugin setup.

     5 */

     7 package isabelle.jedit

    10 import isabelle._

    12 import java.lang.System

    13 import java.awt.Font

    14 import javax.swing.JOptionPane

    16 import scala.collection.mutable

    17 import scala.swing.{ComboBox, ListView, ScrollPane}

    19 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,

    20   Buffer, EditPane, ServiceManager, View}

    21 import org.gjt.sp.jedit.buffer.JEditBuffer

    22 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}

    23 import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}

    24 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}

    25 import org.gjt.sp.jedit.gui.DockableWindowManager

    27 import org.gjt.sp.util.SyntaxUtilities

    28 import org.gjt.sp.util.Log

    30 import scala.actors.Actor._

    33 object Isabelle

    34 {

    35   /* plugin instance */

    37   var plugin: Plugin = null

    38   var session: Session = null

    40   val thy_load = new JEdit_Thy_Load

    41   val thy_info = new Thy_Info(thy_load)

    44   /* properties */

    46   val OPTION_PREFIX = "options.isabelle."

    48   object Property

    49   {

    50     def apply(name: String): String =

    51       jEdit.getProperty(OPTION_PREFIX + name)

    52     def apply(name: String, default: String): String =

    53       jEdit.getProperty(OPTION_PREFIX + name, default)

    54     def update(name: String, value: String) =

    55       jEdit.setProperty(OPTION_PREFIX + name, value)

    56   }

    58   object Boolean_Property

    59   {

    60     def apply(name: String): Boolean =

    61       jEdit.getBooleanProperty(OPTION_PREFIX + name)

    62     def apply(name: String, default: Boolean): Boolean =

    63       jEdit.getBooleanProperty(OPTION_PREFIX + name, default)

    64     def update(name: String, value: Boolean) =

    65       jEdit.setBooleanProperty(OPTION_PREFIX + name, value)

    66   }

    68   object Int_Property

    69   {

    70     def apply(name: String): Int =

    71       jEdit.getIntegerProperty(OPTION_PREFIX + name)

    72     def apply(name: String, default: Int): Int =

    73       jEdit.getIntegerProperty(OPTION_PREFIX + name, default)

    74     def update(name: String, value: Int) =

    75       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)

    76   }

    78   object Double_Property

    79   {

    80     def apply(name: String): Double =

    81       jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)

    82     def apply(name: String, default: Double): Double =

    83       jEdit.getDoubleProperty(OPTION_PREFIX + name, default)

    84     def update(name: String, value: Double) =

    85       jEdit.setDoubleProperty(OPTION_PREFIX + name, value)

    86   }

    88   object Time_Property

    89   {

    90     def apply(name: String): Time =

    91       Time.seconds(Double_Property(name))

    92     def apply(name: String, default: Time): Time =

    93       Time.seconds(Double_Property(name, default.seconds))

    94     def update(name: String, value: Time) =

    95       Double_Property.update(name, value.seconds)

    96   }

    99   /* font */

   101   def font_family(): String = jEdit.getProperty("view.font")

   103   def font_size(): Float =

   104     (jEdit.getIntegerProperty("view.fontsize", 16) *

   105       Int_Property("relative-font-size", 100)).toFloat / 100

   108   /* tooltip markup */

   110   def tooltip(text: String): String =

   111     "<html><pre style=\"font-family: " + font_family() + "; font-size: " +

   112         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)

   113       HTML.encode(text) + "</pre></html>"

   115   private val tooltip_lb = Time.seconds(0.5)

   116   private val tooltip_ub = Time.seconds(60.0)

   117   def tooltip_dismiss_delay(): Time =

   118     Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub

   120   def setup_tooltips()

   121   {

   122     Swing_Thread.now {

   123       val manager = javax.swing.ToolTipManager.sharedInstance

   124       manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)

   125     }

   126   }

   129   /* icons */

   131   def load_icon(name: String): javax.swing.Icon =

   132   {

   133     val icon = GUIUtilities.loadIcon(name)

   134     if (icon.getIconWidth < 0 || icon.getIconHeight < 0)

   135       Log.log(Log.ERROR, icon, "Bad icon: " + name)

   136     icon

   137   }

   140   /* buffers */

   142   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =

   143     Swing_Thread.now { buffer_lock(buffer) { body } }

   145   def buffer_text(buffer: JEditBuffer): String =

   146     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }

   148   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath

   151   /* main jEdit components */

   153   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator

   155   def jedit_buffer(name: String): Option[Buffer] =

   156     jedit_buffers().find(buffer => buffer_name(buffer) == name)

   158   def jedit_views(): Iterator[View] = jEdit.getViews().iterator

   160   def jedit_text_areas(view: View): Iterator[JEditTextArea] =

   161     view.getEditPanes().iterator.map(_.getTextArea)

   163   def jedit_text_areas(): Iterator[JEditTextArea] =

   164     jedit_views().flatMap(jedit_text_areas(_))

   166   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =

   167     jedit_text_areas().filter(_.getBuffer == buffer)

   169   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =

   170   {

   171     try { buffer.readLock(); body }

   172     finally { buffer.readUnlock() }

   173   }

   176   /* document model and view */

   178   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)

   179   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)

   181   def document_views(buffer: Buffer): List[Document_View] =

   182     for {

   183       text_area <- jedit_text_areas(buffer).toList

   184       doc_view = document_view(text_area)

   185       if doc_view.isDefined

   186     } yield doc_view.get

   188   def init_model(buffer: Buffer)

   189   {

   190     swing_buffer_lock(buffer) {

   191       val opt_model =

   192         document_model(buffer) match {

   193           case Some(model) => Some(model)

   194           case None =>

   195             val name = buffer_name(buffer)

   196             Thy_Header.thy_name(name) match {

   197               case Some(theory) =>

   198                 val node_name = Document.Node.Name(name, buffer.getDirectory, theory)

   199                 Some(Document_Model.init(session, buffer, node_name))

   200               case None => None

   201             }

   202         }

   203       if (opt_model.isDefined) {

   204         for (text_area <- jedit_text_areas(buffer)) {

   205           if (document_view(text_area).map(_.model) != opt_model)

   206             Document_View.init(opt_model.get, text_area)

   207         }

   208       }

   209     }

   210   }

   212   def exit_model(buffer: Buffer)

   213   {

   214     swing_buffer_lock(buffer) {

   215       jedit_text_areas(buffer).foreach(Document_View.exit)

   216       Document_Model.exit(buffer)

   217     }

   218   }

   220   def init_view(buffer: Buffer, text_area: JEditTextArea)

   221   {

   222     swing_buffer_lock(buffer) {

   223       document_model(buffer) match {

   224         case Some(model) => Document_View.init(model, text_area)

   225         case None =>

   226       }

   227     }

   228   }

   230   def exit_view(buffer: Buffer, text_area: JEditTextArea)

   231   {

   232     swing_buffer_lock(buffer) {

   233       Document_View.exit(text_area)

   234     }

   235   }

   238   /* dockable windows */

   240   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager

   242   def docked_session(view: View): Option[Session_Dockable] =

   243     wm(view).getDockableWindow("isabelle-session") match {

   244       case dockable: Session_Dockable => Some(dockable)

   245       case _ => None

   246     }

   248   def docked_output(view: View): Option[Output_Dockable] =

   249     wm(view).getDockableWindow("isabelle-output") match {

   250       case dockable: Output_Dockable => Some(dockable)

   251       case _ => None

   252     }

   254   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =

   255     wm(view).getDockableWindow("isabelle-raw-output") match {

   256       case dockable: Raw_Output_Dockable => Some(dockable)

   257       case _ => None

   258     }

   260   def docked_protocol(view: View): Option[Protocol_Dockable] =

   261     wm(view).getDockableWindow("isabelle-protocol") match {

   262       case dockable: Protocol_Dockable => Some(dockable)

   263       case _ => None

   264     }

   267   /* logic image */

   269   def default_logic(): String =

   270   {

   271     val logic = Isabelle_System.getenv("JEDIT_LOGIC")

   272     if (logic != "") logic

   273     else Isabelle_System.getenv_strict("ISABELLE_LOGIC")

   274   }

   276   class Logic_Entry(val name: String, val description: String)

   277   {

   278     override def toString = description

   279   }

   281   def logic_selector(logic: String): ComboBox[Logic_Entry] =

   282   {

   283     val entries =

   284       new Logic_Entry("", "default (" + default_logic() + ")") ::

   285         Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))

   286     val component = new ComboBox(entries)

   287     entries.find(_.name == logic) match {

   288       case None =>

   289       case Some(entry) => component.selection.item = entry

   290     }

   291     component.tooltip = "Isabelle logic image"

   292     component

   293   }

   295   def start_session()

   296   {

   297     val timeout = Time_Property("startup-timeout", Time.seconds(25)) max Time.seconds(5)

   298     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)

   299     val logic = {

   300       val logic = Property("logic")

   301       if (logic != null && logic != "") logic

   302       else Isabelle.default_logic()

   303     }

   304     session.start(timeout, modes ::: List(logic))

   305   }

   308   /* convenience actions */

   310   private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")

   311   {

   312     s1.foreach(text_area.userInput(_))

   313     s2.foreach(text_area.userInput(_))

   314     s2.foreach(_ => text_area.goToPrevCharacter(false))

   315   }

   317   def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)

   318   def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)

   319   def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)

   320   def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)

   321   def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)

   322   def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)

   323   def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)

   325   def check_buffer(buffer: Buffer)

   326   {

   327     document_model(buffer) match {

   328       case None =>

   329       case Some(model) => model.full_perspective()

   330     }

   331   }

   333   def cancel_execution() { session.cancel_execution() }

   334 }

   337 class Plugin extends EBPlugin

   338 {

   339   /* theory files */

   341   private lazy val delay_load =

   342     Swing_Thread.delay_last(Isabelle.session.load_delay)

   343     {

   344       val view = jEdit.getActiveView()

   346       val buffers = Isabelle.jedit_buffers().toList

   347       if (buffers.forall(_.isLoaded)) {

   348         def loaded_buffer(name: String): Boolean =

   349           buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)

   351         val thys =

   352           for (buffer <- buffers; model <- Isabelle.document_model(buffer))

   353             yield model.name

   355         // FIXME avoid I/O in Swing thread!?!

   356         val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).

   357           filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))

   359         if (!files.isEmpty) {

   360           val files_list = new ListView(files.sorted)

   361           for (i <- 0 until files.length)

   362             files_list.selection.indices += i

   364           val answer =

   365             Library.confirm_dialog(view,

   366               "Auto loading of required files",

   367               JOptionPane.YES_NO_OPTION,

   368               "The following files are required to resolve theory imports.",

   369               "Reload selected files now?",

   370               new ScrollPane(files_list))

   371           if (answer == 0) {

   372             files.foreach(file =>

   373               if (files_list.selection.items.contains(file))

   374                 jEdit.openFile(null: View, file))

   375           }

   376         }

   377       }

   378     }

   381   /* session manager */

   383   private val session_manager = actor {

   384     loop {

   385       react {

   386         case phase: Session.Phase =>

   387           phase match {

   388             case Session.Failed =>

   389               Swing_Thread.later {

   390                 val text = new scala.swing.TextArea(Isabelle.session.current_syslog())

   391                 text.editable = false

   392                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)

   393               }

   395             case Session.Ready =>

   396               Isabelle.jedit_buffers.foreach(Isabelle.init_model)

   397               delay_load(true)

   399             case Session.Shutdown =>

   400               Isabelle.jedit_buffers.foreach(Isabelle.exit_model)

   401               delay_load(false)

   403             case _ =>

   404           }

   405         case bad => System.err.println("session_manager: ignoring bad message " + bad)

   406       }

   407     }

   408   }

   411   /* main plugin plumbing */

   413   override def handleMessage(message: EBMessage)

   414   {

   415     Swing_Thread.assert()

   416     message match {

   417       case msg: EditorStarted =>

   418         if (Isabelle.Boolean_Property("auto-start"))

   419           Isabelle.start_session()

   421       case msg: BufferUpdate

   422       if msg.getWhat == BufferUpdate.LOADED =>

   423         if (Isabelle.session.is_ready) {

   424           val buffer = msg.getBuffer

   425           if (buffer != null) Isabelle.init_model(buffer)

   426           delay_load(true)

   427         }

   429       case msg: EditPaneUpdate

   430       if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||

   431           msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||

   432           msg.getWhat == EditPaneUpdate.CREATED ||

   433           msg.getWhat == EditPaneUpdate.DESTROYED) =>

   434         val edit_pane = msg.getEditPane

   435         val buffer = edit_pane.getBuffer

   436         val text_area = edit_pane.getTextArea

   438         if (buffer != null && text_area != null) {

   439           if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||

   440               msg.getWhat == EditPaneUpdate.CREATED) {

   441             if (Isabelle.session.is_ready)

   442               Isabelle.init_view(buffer, text_area)

   443           }

   444           else Isabelle.exit_view(buffer, text_area)

   445         }

   447       case msg: PropertiesChanged =>

   448         Isabelle.setup_tooltips()

   449         Isabelle.session.global_settings.event(Session.Global_Settings)

   451       case _ =>

   452     }

   453   }

   455   override def start()

   456   {

   457     Isabelle.plugin = this

   458     Isabelle.setup_tooltips()

   459     Isabelle_System.init()

   460     Isabelle_System.install_fonts()

   461     Isabelle.session = new Session(Isabelle.thy_load)

   462     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)

   463     if (ModeProvider.instance.isInstanceOf[ModeProvider])

   464       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)

   465     Isabelle.session.phase_changed += session_manager

   466   }

   468   override def stop()

   469   {

   470     Isabelle.session.phase_changed -= session_manager

   471     Isabelle.jedit_buffers.foreach(Isabelle.exit_model)

   472     Isabelle.session.stop()

   473   }

   474 }

author	wenzelm
	Sat, 17 Mar 2012 17:44:29 +0100
changeset 47868	395b7277ed76
parent 47800	1752164d916b
child 47929	34761733526c
permissions	-rw-r--r--