src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34433 3da749b53842
parent 34429 03afc73e185f
child 34440 561a6d19bd95
equal deleted inserted replaced
34432:5a8b9fc98d8c 34433:3da749b53842
    14 
    14 
    15 import scala.collection.mutable.HashMap
    15 import scala.collection.mutable.HashMap
    16 
    16 
    17 import isabelle.utils.EventSource
    17 import isabelle.utils.EventSource
    18 import isabelle.prover.{Prover, Command}
    18 import isabelle.prover.{Prover, Command}
    19 import isabelle.IsabelleSystem
    19 import isabelle.{IsabelleSystem, Symbol}
    20 
    20 
    21 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    21 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    22 import org.gjt.sp.jedit.buffer.JEditBuffer
    22 import org.gjt.sp.jedit.buffer.JEditBuffer
    23 import org.gjt.sp.jedit.textarea.JEditTextArea
    23 import org.gjt.sp.jedit.textarea.JEditTextArea
    24 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    24 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    25 
    25 
    26 
    26 
    27 object Plugin {
    27 object Plugin {
       
    28   // name
    28   val NAME = "Isabelle"
    29   val NAME = "Isabelle"
    29   val OPTION_PREFIX = "options.isabelle."
    30   val OPTION_PREFIX = "options.isabelle."
    30   val VFS_PREFIX = "isabelle:"
    31   val VFS_PREFIX = "isabelle:"
    31   
    32 
       
    33   // properties
    32   def property(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
    34   def property(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
    33   def property(name: String, value: String) = 
    35   def property(name: String, value: String) = 
    34     jEdit.setProperty(OPTION_PREFIX + name, value)
    36     jEdit.setProperty(OPTION_PREFIX + name, value)
    35   
    37 
    36   var plugin: Plugin = null
    38   // dynamic instance
    37   def prover(buffer: JEditBuffer) = plugin.prover_setup(buffer).get.prover
    39   var self: Plugin = null
    38   def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer).get
    40 
       
    41   // provers
       
    42   def prover(buffer: JEditBuffer) = self.prover_setup(buffer).get.prover
       
    43   def prover_setup(buffer: JEditBuffer) = self.prover_setup(buffer).get
    39 }
    44 }
    40 
    45 
    41 
    46 
    42 class Plugin extends EBPlugin {
    47 class Plugin extends EBPlugin {
    43   
    48 
       
    49   // Isabelle symbols
       
    50   val symbols = new Symbol.Interpretation
       
    51 
       
    52 
       
    53   // Isabelle font
       
    54 
       
    55   var font: Font = null
       
    56   val font_changed = new EventSource[Font]
       
    57 
       
    58   def set_font(path: String, size: Float) {
       
    59     try {
       
    60       font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
       
    61         deriveFont(Font.PLAIN, size)
       
    62       font_changed.fire(font)
       
    63     }
       
    64     catch {
       
    65       case e: IOException =>
       
    66     }
       
    67   }
       
    68 
       
    69 
       
    70   // mapping buffer <-> prover
       
    71 
    44   private val mapping = new HashMap[JEditBuffer, ProverSetup]
    72   private val mapping = new HashMap[JEditBuffer, ProverSetup]
    45 
       
    46   var viewFont: Font = null
       
    47   val viewFontChanged = new EventSource[Font]
       
    48 
    73 
    49   def install(view: View) {
    74   def install(view: View) {
    50     val buffer = view.getBuffer
    75     val buffer = view.getBuffer
    51     mapping.get(buffer) match{
    76     mapping.get(buffer) match{
    52       case None =>{
    77       case None =>{
    66         proversetup.deactivate
    91         proversetup.deactivate
    67     }
    92     }
    68   }
    93   }
    69 
    94 
    70   def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
    95   def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
    71   def is_active(buffer: JEditBuffer) =
    96   def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
    72     mapping.get(buffer) match { case None => false case _ => true }
    97 
    73   
    98   
       
    99   // main plugin plumbing
       
   100 
    74   override def handleMessage(msg: EBMessage) = msg match {
   101   override def handleMessage(msg: EBMessage) = msg match {
    75     case epu: EditPaneUpdate => epu.getWhat() match {
   102     case epu: EditPaneUpdate => epu.getWhat match {
    76       case EditPaneUpdate.BUFFER_CHANGED =>
   103       case EditPaneUpdate.BUFFER_CHANGED =>
    77         mapping get epu.getEditPane.getBuffer match {
   104         mapping get epu.getEditPane.getBuffer match {
    78           //only activate 'isabelle'-buffers!
   105           //only activate 'isabelle'-buffers!
    79           case None =>
   106           case None =>
    80           case Some(prover_setup) => 
   107           case Some(prover_setup) => 
    99       case _ =>
   126       case _ =>
   100     }
   127     }
   101     case _ =>
   128     case _ =>
   102   }
   129   }
   103 
   130 
   104   def setFont(path: String, size: Float) {
       
   105     try {
       
   106       val fontStream = new FileInputStream(path)
       
   107       val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
       
   108       viewFont = font.deriveFont(Font.PLAIN, size)
       
   109 
       
   110       viewFontChanged.fire(viewFont)
       
   111     }
       
   112     catch {
       
   113       case e: IOException =>
       
   114     }
       
   115   }
       
   116   
       
   117   override def start() {
   131   override def start() {
   118     Plugin.plugin = this
   132     Plugin.self = this
   119     
   133     
   120     if (Plugin.property("font-path") != null && Plugin.property("font-size") != null)
   134     if (Plugin.property("font-path") != null && Plugin.property("font-size") != null)
   121       try {
   135       try {
   122         setFont(Plugin.property("font-path"), Plugin.property("font-size").toFloat)
   136         set_font(Plugin.property("font-path"), Plugin.property("font-size").toFloat)
   123       }
   137       }
   124       catch {
   138       catch {
   125         case e: NumberFormatException =>
   139         case e: NumberFormatException =>
   126       }
   140       }
   127   }
   141   }
   128   
   142   
   129   override def stop() {
   143   override def stop() {
   130     // TODO: proper cleanup
   144     // TODO: proper cleanup
   131     Plugin.plugin = null
   145     Plugin.self = null
   132   }
   146   }
   133 }
   147 }