src/Tools/jEdit/src/jedit/Plugin.scala
author wenzelm
Sun Oct 19 16:51:55 2008 +0200 (2008-10-19 ago)
changeset 34318 c13e168a8ae6
child 34337 5d5b69f2956b
permissions -rw-r--r--
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
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@34318
    19
  
wenzelm@34318
    20
  def property(name : String) = jEdit.getProperty(OPTION_PREFIX + name)
wenzelm@34318
    21
  def property(name : String, value : String) = 
wenzelm@34318
    22
    jEdit.setProperty(OPTION_PREFIX + name, value)
wenzelm@34318
    23
  
wenzelm@34318
    24
  var plugin : Plugin = null
wenzelm@34318
    25
}
wenzelm@34318
    26
wenzelm@34318
    27
class Plugin extends EBPlugin {
wenzelm@34318
    28
  import Plugin._
wenzelm@34318
    29
  
wenzelm@34318
    30
  val prover = new Prover()
wenzelm@34318
    31
  var theoryView : TheoryView = null
wenzelm@34318
    32
  
wenzelm@34318
    33
  var viewFont : Font = null 
wenzelm@34318
    34
  val viewFontChanged = new EventSource[Font]
wenzelm@34318
    35
  
wenzelm@34318
    36
  private var _selectedState : Command = null
wenzelm@34318
    37
  
wenzelm@34318
    38
  val stateUpdate = new EventSource[Command]
wenzelm@34318
    39
  
wenzelm@34318
    40
  def selectedState = _selectedState
wenzelm@34318
    41
  def selectedState_=(newState : Command) {
wenzelm@34318
    42
    _selectedState = newState
wenzelm@34318
    43
    stateUpdate fire newState
wenzelm@34318
    44
  }
wenzelm@34318
    45
  
wenzelm@34318
    46
  def activate(view : View) {
wenzelm@34318
    47
    val logic = property("logic")
wenzelm@34318
    48
    theoryView = new TheoryView(prover, view.getBuffer())
wenzelm@34318
    49
    prover.start(if (logic == null) logic else "HOL")
wenzelm@34318
    50
    val dir = view.getBuffer().getDirectory()
wenzelm@34318
    51
    prover.setDocument(theoryView, 
wenzelm@34318
    52
                       if (dir.startsWith("isa:")) dir.substring(4) else dir)
wenzelm@34318
    53
    TheoryView.activateTextArea(view.getTextArea())
wenzelm@34318
    54
  }
wenzelm@34318
    55
  
wenzelm@34318
    56
  override def handleMessage(msg : EBMessage) = msg match {
wenzelm@34318
    57
    case epu : EditPaneUpdate => epu.getWhat() match {
wenzelm@34318
    58
      case EditPaneUpdate.BUFFER_CHANGED =>
wenzelm@34318
    59
        TheoryView.activateTextArea(epu.getEditPane().getTextArea())
wenzelm@34318
    60
wenzelm@34318
    61
      case EditPaneUpdate.BUFFER_CHANGING =>
wenzelm@34318
    62
        TheoryView.deactivateTextArea(epu.getEditPane().getTextArea())
wenzelm@34318
    63
wenzelm@34318
    64
      case _ =>
wenzelm@34318
    65
    }
wenzelm@34318
    66
      
wenzelm@34318
    67
    case _ =>
wenzelm@34318
    68
  }
wenzelm@34318
    69
wenzelm@34318
    70
  def setFont(path : String, size : Float) {
wenzelm@34318
    71
    try {
wenzelm@34318
    72
      val fontStream = new FileInputStream(path)
wenzelm@34318
    73
      val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
wenzelm@34318
    74
      viewFont = font.deriveFont(Font.PLAIN, size)
wenzelm@34318
    75
      
wenzelm@34318
    76
      viewFontChanged.fire(viewFont)
wenzelm@34318
    77
    }
wenzelm@34318
    78
    catch {
wenzelm@34318
    79
      case e : IOException =>
wenzelm@34318
    80
    }
wenzelm@34318
    81
  }
wenzelm@34318
    82
  
wenzelm@34318
    83
  override def start() {
wenzelm@34318
    84
    plugin = this
wenzelm@34318
    85
wenzelm@34318
    86
    if (property("font-path") != null && property("font-size") != null)
wenzelm@34318
    87
      try {
wenzelm@34318
    88
        setFont(property("font-path"), property("font-size").toFloat)
wenzelm@34318
    89
      }
wenzelm@34318
    90
      catch {
wenzelm@34318
    91
        case e : NumberFormatException =>
wenzelm@34318
    92
      }
wenzelm@34318
    93
  }
wenzelm@34318
    94
  
wenzelm@34318
    95
  override def stop() {
wenzelm@34318
    96
    // TODO: implement cleanup
wenzelm@34318
    97
  }
wenzelm@34318
    98
}