wneuper/isa: src/Tools/jEdit/src/jedit/plugin.scala@803431dcc7fb

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

     2     Author:     Makarius

     4 Main Isabelle/jEdit plugin setup.

     5 */

     7 package isabelle.jedit

    10 import isabelle._

    12 import java.io.{FileInputStream, IOException}

    13 import java.awt.Font

    14 import javax.swing.JTextArea

    16 import scala.collection.mutable

    18 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}

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

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

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

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

    25 object Isabelle

    26 {

    27   /* plugin instance */

    29   var system: Isabelle_System = null

    30   var session: Session = null

    33   /* properties */

    35   val OPTION_PREFIX = "options.isabelle."

    37   object Property

    38   {

    39     def apply(name: String): String =

    40       jEdit.getProperty(OPTION_PREFIX + name)

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

    42       jEdit.getProperty(OPTION_PREFIX + name, default)

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

    44       jEdit.setProperty(OPTION_PREFIX + name, value)

    45   }

    47   object Boolean_Property

    48   {

    49     def apply(name: String): Boolean =

    50       jEdit.getBooleanProperty(OPTION_PREFIX + name)

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

    52       jEdit.getBooleanProperty(OPTION_PREFIX + name, default)

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

    54       jEdit.setBooleanProperty(OPTION_PREFIX + name, value)

    55   }

    57   object Int_Property

    58   {

    59     def apply(name: String): Int =

    60       jEdit.getIntegerProperty(OPTION_PREFIX + name)

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

    62       jEdit.getIntegerProperty(OPTION_PREFIX + name, default)

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

    64       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)

    65   }

    68   /* font */

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

    72   def font_size(): Float =

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

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

    77   /* text area ranges */

    79   case class Gfx_Range(val x: Int, val y: Int, val length: Int)

    81   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =

    82   {

    83     val p = text_area.offsetToXY(range.start)

    84     val q = text_area.offsetToXY(range.stop)

    85     if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))

    86     else None

    87   }

    90   /* tooltip markup */

    92   def tooltip(text: String): String =

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

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

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

    97   def tooltip_dismiss_delay(): Int =

    98     Int_Property("tooltip-dismiss-delay", 8000) max 500

   100   def setup_tooltips()

   101   {

   102     Swing_Thread.now {

   103       val manager = javax.swing.ToolTipManager.sharedInstance

   104       manager.setDismissDelay(tooltip_dismiss_delay())

   105     }

   106   }

   109   /* settings */

   111   def default_logic(): String =

   112   {

   113     val logic = system.getenv("JEDIT_LOGIC")

   114     if (logic != "") logic

   115     else system.getenv_strict("ISABELLE_LOGIC")

   116   }

   118   def isabelle_args(): List[String] =

   119   {

   120     val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)

   121     val logic = {

   122       val logic = Property("logic")

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

   124       else default_logic()

   125     }

   126     modes ++ List(logic)

   127   }

   130   /* main jEdit components */

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

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

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

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

   139   def jedit_text_areas(): Iterator[JEditTextArea] =

   140     jedit_views().flatMap(jedit_text_areas(_))

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

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

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

   146   {

   147     try { buffer.readLock(); body }

   148     finally { buffer.readUnlock() }

   149   }

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

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

   155   /* dockable windows */

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

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

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

   161       case dockable: Output_Dockable => Some(dockable)

   162       case _ => None

   163     }

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

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

   167       case dockable: Raw_Output_Dockable => Some(dockable)

   168       case _ => None

   169     }

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

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

   173       case dockable: Protocol_Dockable => Some(dockable)

   174       case _ => None

   175     }

   178   /* manage prover */  // FIXME async!?

   180   private def prover_started(view: View): Boolean =

   181   {

   182     val timeout = Int_Property("startup-timeout") max 1000

   183     session.started(timeout, Isabelle.isabelle_args()) match {

   184       case Some(err) =>

   185         val text = new JTextArea(err); text.setEditable(false)

   186         Library.error_dialog(view, null, "Failed to start Isabelle process", text)

   187         false

   188       case None => true

   189     }

   190   }

   193   /* activation */

   195   def activate_buffer(view: View, buffer: Buffer)

   196   {

   197     if (prover_started(view)) {

   198       // FIXME proper error handling

   199       val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))

   201       val model = Document_Model.init(session, buffer, thy_name)

   202       for (text_area <- jedit_text_areas(buffer))

   203         Document_View.init(model, text_area)

   204     }

   205   }

   207   def deactivate_buffer(buffer: Buffer)

   208   {

   209     session.stop()  // FIXME not yet

   211     for (text_area <- jedit_text_areas(buffer))

   212       Document_View.exit(text_area)

   213     Document_Model.exit(buffer)

   214   }

   216   def switch_active(view: View) =

   217   {

   218     val buffer = view.getBuffer

   219     if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)

   220     else activate_buffer(view, buffer)

   221   }

   223   def is_active(view: View): Boolean =

   224     Document_Model(view.getBuffer).isDefined

   225 }

   228 class Plugin extends EBPlugin

   229 {

   230   /* main plugin plumbing */

   232   override def handleMessage(message: EBMessage)

   233   {

   234     message match {

   235       case msg: BufferUpdate

   236         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>

   237         Document_Model(msg.getBuffer) match {

   238           case Some(model) => model.refresh()

   239           case _ =>

   240         }

   242       case msg: EditPaneUpdate =>

   243         val edit_pane = msg.getEditPane

   244         val buffer = edit_pane.getBuffer

   245         val text_area = edit_pane.getTextArea

   247         def init_view()

   248         {

   249           Document_Model(buffer) match {

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

   251             case None =>

   252           }

   253         }

   254         def exit_view()

   255         {

   256           if (Document_View(text_area).isDefined)

   257             Document_View.exit(text_area)

   258         }

   259         msg.getWhat match {

   260           case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()

   261           case EditPaneUpdate.CREATED => init_view()

   262           case EditPaneUpdate.DESTROYED => exit_view()

   263           case _ =>

   264         }

   266       case msg: PropertiesChanged =>

   267         Swing_Thread.now {

   268           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)

   269             Document_View(text_area).get.extend_styles()

   271           Isabelle.setup_tooltips()

   272         }

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

   276       case _ =>

   277     }

   278   }

   280   override def start()

   281   {

   282     Isabelle.system = new Isabelle_System

   283     Isabelle.system.install_fonts()

   284     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?

   286     Isabelle.setup_tooltips()

   287   }

   289   override def stop()  // FIXME fragile

   290   {

   291     Isabelle.session.stop()  // FIXME dialog!?

   292     Isabelle.session = null

   293   }

   294 }

author	wenzelm
	Tue, 07 Sep 2010 13:16:45 +0200
changeset 39448	803431dcc7fb
parent 39344	a0d7e9b580ec
child 39518	e9a442606db3
permissions	-rw-r--r--