src/Tools/jEdit/src/jedit/Plugin.scala
author wenzelm
Tue Oct 21 22:28:58 2008 +0200 (2008-10-21)
changeset 34337 5d5b69f2956b
parent 34318 c13e168a8ae6
child 34406 f81cd75ae331
permissions -rw-r--r--
renamed VFS protocol prefix from "isa:" to "isabelle:";
wenzelm@34318
     1
package isabelle.jedit
wenzelm@34318
     2
wenzelm@34318
     3
import java.awt.Font
wenzelm@34318
     4
import java.io.{ FileInputStream, IOException }
wenzelm@34318
     5
wenzelm@34318
     6
wenzelm@34318
     7
import isabelle.utils.EventSource
wenzelm@34318
     8
wenzelm@34318
     9
import isabelle.prover.{ Prover, Command }
wenzelm@34318
    10
wenzelm@34318
    11
import isabelle.IsabelleSystem
wenzelm@34318
    12
wenzelm@34318
    13
import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
wenzelm@34318
    14
import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
wenzelm@34318
    15
wenzelm@34318
    16
object Plugin {
wenzelm@34318
    17
  val NAME = "Isabelle"
wenzelm@34318
    18
  val OPTION_PREFIX = "options.isabelle."
wenzelm@34337
    19
  val VFS_PREFIX = "isabelle:"
wenzelm@34318
    20
  
wenzelm@34318
    21
  def property(name : String) = jEdit.getProperty(OPTION_PREFIX + name)
wenzelm@34318
    22
  def property(name : String, value : String) = 
wenzelm@34318
    23
    jEdit.setProperty(OPTION_PREFIX + name, value)
wenzelm@34318
    24
  
wenzelm@34318
    25
  var plugin : Plugin = null
wenzelm@34318
    26
}
wenzelm@34318
    27
wenzelm@34318
    28
class Plugin extends EBPlugin {
wenzelm@34318
    29
  import Plugin._
wenzelm@34318
    30
  
wenzelm@34318
    31
  val prover = new Prover()
wenzelm@34318
    32
  var theoryView : TheoryView = null
wenzelm@34318
    33
  
wenzelm@34318
    34
  var viewFont : Font = null 
wenzelm@34318
    35
  val viewFontChanged = new EventSource[Font]
wenzelm@34318
    36
  
wenzelm@34318
    37
  private var _selectedState : Command = null
wenzelm@34318
    38
  
wenzelm@34318
    39
  val stateUpdate = new EventSource[Command]
wenzelm@34318
    40
  
wenzelm@34318
    41
  def selectedState = _selectedState
wenzelm@34318
    42
  def selectedState_=(newState : Command) {
wenzelm@34318
    43
    _selectedState = newState
wenzelm@34318
    44
    stateUpdate fire newState
wenzelm@34318
    45
  }
wenzelm@34318
    46
  
wenzelm@34318
    47
  def activate(view : View) {
wenzelm@34318
    48
    val logic = property("logic")
wenzelm@34318
    49
    theoryView = new TheoryView(prover, view.getBuffer())
wenzelm@34318
    50
    prover.start(if (logic == null) logic else "HOL")
wenzelm@34318
    51
    val dir = view.getBuffer().getDirectory()
wenzelm@34318
    52
    prover.setDocument(theoryView, 
wenzelm@34337
    53
                       if (dir.startsWith(VFS_PREFIX)) dir.substring(VFS_PREFIX.length) else dir)
wenzelm@34318
    54
    TheoryView.activateTextArea(view.getTextArea())
wenzelm@34318
    55
  }
wenzelm@34318
    56
  
wenzelm@34318
    57
  override def handleMessage(msg : EBMessage) = msg match {
wenzelm@34318
    58
    case epu : EditPaneUpdate => epu.getWhat() match {
wenzelm@34318
    59
      case EditPaneUpdate.BUFFER_CHANGED =>
wenzelm@34318
    60
        TheoryView.activateTextArea(epu.getEditPane().getTextArea())
wenzelm@34318
    61
wenzelm@34318
    62
      case EditPaneUpdate.BUFFER_CHANGING =>
wenzelm@34318
    63
        TheoryView.deactivateTextArea(epu.getEditPane().getTextArea())
wenzelm@34318
    64
wenzelm@34318
    65
      case _ =>
wenzelm@34318
    66
    }
wenzelm@34318
    67
      
wenzelm@34318
    68
    case _ =>
wenzelm@34318
    69
  }
wenzelm@34318
    70
wenzelm@34318
    71
  def setFont(path : String, size : Float) {
wenzelm@34318
    72
    try {
wenzelm@34318
    73
      val fontStream = new FileInputStream(path)
wenzelm@34318
    74
      val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
wenzelm@34318
    75
      viewFont = font.deriveFont(Font.PLAIN, size)
wenzelm@34318
    76
      
wenzelm@34318
    77
      viewFontChanged.fire(viewFont)
wenzelm@34318
    78
    }
wenzelm@34318
    79
    catch {
wenzelm@34318
    80
      case e : IOException =>
wenzelm@34318
    81
    }
wenzelm@34318
    82
  }
wenzelm@34318
    83
  
wenzelm@34318
    84
  override def start() {
wenzelm@34318
    85
    plugin = this
wenzelm@34318
    86
wenzelm@34318
    87
    if (property("font-path") != null && property("font-size") != null)
wenzelm@34318
    88
      try {
wenzelm@34318
    89
        setFont(property("font-path"), property("font-size").toFloat)
wenzelm@34318
    90
      }
wenzelm@34318
    91
      catch {
wenzelm@34318
    92
        case e : NumberFormatException =>
wenzelm@34318
    93
      }
wenzelm@34318
    94
  }
wenzelm@34318
    95
  
wenzelm@34318
    96
  override def stop() {
wenzelm@34318
    97
    // TODO: implement cleanup
wenzelm@34318
    98
  }
wenzelm@34318
    99
}