src/Tools/jEdit/src/jedit/Plugin.scala
author wenzelm
Fri Dec 19 22:24:32 2008 +0100 (2008-12-19)
changeset 34407 aad6834ba380
parent 34406 f81cd75ae331
child 34422 d5a41da986c3
permissions -rw-r--r--
added some headers and comments;
wenzelm@34407
     1
/*
wenzelm@34407
     2
 * Main Isabelle/jEdit plugin setup
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
wenzelm@34407
     5
 * @author Fabian Immler, TU Munich
wenzelm@34407
     6
 */
wenzelm@34407
     7
wenzelm@34318
     8
package isabelle.jedit
wenzelm@34318
     9
wenzelm@34318
    10
import java.awt.Font
wenzelm@34318
    11
import java.io.{ FileInputStream, IOException }
immler@34406
    12
import javax.swing.JScrollPane
wenzelm@34318
    13
wenzelm@34318
    14
import isabelle.utils.EventSource
wenzelm@34318
    15
wenzelm@34318
    16
import isabelle.prover.{ Prover, Command }
wenzelm@34318
    17
wenzelm@34318
    18
import isabelle.IsabelleSystem
wenzelm@34318
    19
immler@34406
    20
import scala.collection.mutable.HashMap
immler@34406
    21
immler@34406
    22
import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View }
immler@34406
    23
import org.gjt.sp.jedit.buffer.JEditBuffer
immler@34406
    24
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@34318
    25
import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
wenzelm@34318
    26
wenzelm@34318
    27
object Plugin {
wenzelm@34318
    28
  val NAME = "Isabelle"
wenzelm@34318
    29
  val OPTION_PREFIX = "options.isabelle."
wenzelm@34337
    30
  val VFS_PREFIX = "isabelle:"
wenzelm@34318
    31
  
wenzelm@34318
    32
  def property(name : String) = jEdit.getProperty(OPTION_PREFIX + name)
wenzelm@34318
    33
  def property(name : String, value : String) = 
wenzelm@34318
    34
    jEdit.setProperty(OPTION_PREFIX + name, value)
wenzelm@34318
    35
  
wenzelm@34318
    36
  var plugin : Plugin = null
immler@34406
    37
  def prover(buffer : JEditBuffer) = plugin.prover_setup(buffer).get.prover
immler@34406
    38
  def prover_setup(buffer : JEditBuffer) = plugin.prover_setup(buffer).get
immler@34406
    39
wenzelm@34318
    40
}
wenzelm@34318
    41
wenzelm@34318
    42
class Plugin extends EBPlugin {
wenzelm@34318
    43
  import Plugin._
immler@34406
    44
immler@34406
    45
  private val mapping = new HashMap[JEditBuffer, ProverSetup]
immler@34406
    46
immler@34406
    47
  var viewFont : Font = null
wenzelm@34318
    48
  val viewFontChanged = new EventSource[Font]
immler@34406
    49
immler@34406
    50
  def install(view : View) {
immler@34406
    51
    val buffer = view.getBuffer
immler@34406
    52
    mapping.get(buffer) match{
immler@34406
    53
      case None =>{
immler@34406
    54
          val prover_setup = new ProverSetup(buffer)
immler@34406
    55
          mapping.update(buffer, prover_setup)
immler@34406
    56
          prover_setup.activate(view)
immler@34406
    57
      }
immler@34406
    58
      case _ => System.err.println("Already installed plugin on Buffer")
immler@34406
    59
    }
wenzelm@34318
    60
  }
immler@34406
    61
immler@34406
    62
  def uninstall(view : View) {
immler@34406
    63
    val buffer = view.getBuffer
immler@34406
    64
    mapping.removeKey(buffer) match{
immler@34406
    65
      case None => System.err.println("No Plugin installed on this Buffer")
immler@34406
    66
      case Some(proversetup) =>
immler@34406
    67
        proversetup.deactivate
immler@34406
    68
    }
wenzelm@34318
    69
  }
immler@34406
    70
immler@34406
    71
  def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
immler@34406
    72
  def is_active (buffer : JEditBuffer) = mapping.get(buffer) match { case None => false case _ => true}
wenzelm@34318
    73
  
wenzelm@34318
    74
  override def handleMessage(msg : EBMessage) = msg match {
wenzelm@34318
    75
    case epu : EditPaneUpdate => epu.getWhat() match {
wenzelm@34318
    76
      case EditPaneUpdate.BUFFER_CHANGED =>
immler@34406
    77
        mapping get epu.getEditPane.getBuffer match {
immler@34406
    78
          //only activate 'isabelle'-buffers!
immler@34406
    79
          case None =>
immler@34406
    80
          case Some(prover_setup) => 
immler@34406
    81
            prover_setup.theory_view.activate
immler@34406
    82
            val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("Isabelle_output")
immler@34406
    83
            if(dockable != null) {
immler@34406
    84
              val output_dockable = dockable.asInstanceOf[OutputDockable]
immler@34406
    85
              if(output_dockable.getComponent(0) != prover_setup.output_text_view ) {
immler@34406
    86
                output_dockable.asInstanceOf[OutputDockable].removeAll
immler@34406
    87
                output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
immler@34406
    88
                output_dockable.revalidate
immler@34406
    89
              }
immler@34406
    90
            }
immler@34406
    91
        }
wenzelm@34318
    92
      case EditPaneUpdate.BUFFER_CHANGING =>
immler@34406
    93
        val buffer = epu.getEditPane.getBuffer
immler@34406
    94
        if(buffer != null) mapping get buffer match {
immler@34406
    95
          //only deactivate 'isabelle'-buffers!
immler@34406
    96
          case None =>
immler@34406
    97
          case Some(prover_setup) => prover_setup.theory_view.deactivate
immler@34406
    98
        }
wenzelm@34318
    99
      case _ =>
wenzelm@34318
   100
    }
wenzelm@34318
   101
      
wenzelm@34318
   102
    case _ =>
wenzelm@34318
   103
  }
wenzelm@34318
   104
wenzelm@34318
   105
  def setFont(path : String, size : Float) {
wenzelm@34318
   106
    try {
wenzelm@34318
   107
      val fontStream = new FileInputStream(path)
wenzelm@34318
   108
      val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
wenzelm@34318
   109
      viewFont = font.deriveFont(Font.PLAIN, size)
immler@34406
   110
wenzelm@34318
   111
      viewFontChanged.fire(viewFont)
wenzelm@34318
   112
    }
wenzelm@34318
   113
    catch {
wenzelm@34318
   114
      case e : IOException =>
wenzelm@34318
   115
    }
wenzelm@34318
   116
  }
wenzelm@34318
   117
  
wenzelm@34318
   118
  override def start() {
wenzelm@34318
   119
    plugin = this
immler@34406
   120
    
wenzelm@34318
   121
    if (property("font-path") != null && property("font-size") != null)
wenzelm@34318
   122
      try {
wenzelm@34318
   123
        setFont(property("font-path"), property("font-size").toFloat)
wenzelm@34318
   124
      }
wenzelm@34318
   125
      catch {
wenzelm@34318
   126
        case e : NumberFormatException =>
wenzelm@34318
   127
      }
wenzelm@34318
   128
  }
wenzelm@34318
   129
  
wenzelm@34318
   130
  override def stop() {
wenzelm@34318
   131
    // TODO: implement cleanup
wenzelm@34318
   132
  }
wenzelm@34318
   133
}