src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34618 e45052ff7233
parent 34615 5e61055bf35b
child 34623 a356a8ee6f00
equal deleted inserted replaced
34617:8d2c49605685 34618:e45052ff7233
    21 import org.gjt.sp.jedit.buffer.JEditBuffer
    21 import org.gjt.sp.jedit.buffer.JEditBuffer
    22 import org.gjt.sp.jedit.textarea.JEditTextArea
    22 import org.gjt.sp.jedit.textarea.JEditTextArea
    23 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    23 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    24 
    24 
    25 
    25 
    26 object Isabelle {
    26 object Isabelle
    27   // name
    27 {
       
    28   /* name */
       
    29 
    28   val NAME = "Isabelle"
    30   val NAME = "Isabelle"
    29   val VFS_PREFIX = "isabelle:"
    31   val VFS_PREFIX = "isabelle:"
    30 
    32 
    31   // properties
    33 
    32   object Property {
    34   /* properties */
    33     private val OPTION_PREFIX = "options.isabelle."
    35 
    34     def apply(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
    36   val OPTION_PREFIX = "options.isabelle."
       
    37 
       
    38   object Property
       
    39   {
       
    40     def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
    35     def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    41     def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    36   }
    42   }
    37 
    43 
    38   // Isabelle system instance
    44   object Boolean_Property
       
    45   {
       
    46     def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
       
    47     def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
       
    48   }
       
    49 
       
    50   object Int_Property
       
    51   {
       
    52     def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
       
    53     def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
       
    54   }
       
    55 
       
    56 
       
    57   /* Isabelle system instance */
       
    58 
    39   var system: Isabelle_System = null
    59   var system: Isabelle_System = null
    40   def symbols = system.symbols
    60   def symbols = system.symbols
    41   lazy val completion = new Completion + symbols
    61   lazy val completion = new Completion + symbols
    42 
    62 
    43   // settings
    63 
    44   def default_logic = {
    64   /* settings */
       
    65 
       
    66   def default_logic =
       
    67   {
    45     val logic = Isabelle.Property("logic")
    68     val logic = Isabelle.Property("logic")
    46     if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
    69     if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
    47   }
    70   }
    48 
    71 
    49   // plugin instance
    72 
       
    73   /* plugin instance */
       
    74 
    50   var plugin: Plugin = null
    75   var plugin: Plugin = null
    51 
    76 
    52   // running provers
    77 
       
    78   /* running provers */
       
    79 
    53   def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    80   def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    54 }
    81 }
    55 
    82 
    56 
    83 
    57 class Plugin extends EBPlugin {
    84 class Plugin extends EBPlugin
    58 
    85 {
    59   // Isabelle font
    86   /* Isabelle font */
    60 
    87 
    61   var font: Font = null
    88   var font: Font = null
    62   val font_changed = new EventBus[Font]
    89   val font_changed = new EventBus[Font]
    63 
    90 
    64   def set_font(path: String, size: Float) {
    91   def set_font(size: Int)
    65     font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
    92   {
    66       deriveFont(Font.PLAIN, size)
    93     font = Font.createFont(Font.TRUETYPE_FONT,
       
    94         new FileInputStream(Isabelle.system.platform_path("~~/lib/fonts/IsabelleMono.ttf"))).
       
    95       deriveFont(Font.PLAIN, size max 1)
    67     font_changed.event(font)
    96     font_changed.event(font)
    68   }
    97   }
    69 
    98 
    70 
    99 
    71   /* unique ids */  // FIXME specific to "session" (!??)
   100   /* mapping buffer <-> prover */
    72 
       
    73   private var id_count: BigInt = 0
       
    74   def id() : String = synchronized { id_count += 1; "editor:" + id_count }
       
    75 
       
    76 
       
    77   // mapping buffer <-> prover
       
    78 
   101 
    79   private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
   102   private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
    80 
   103 
    81   private def install(view: View) {
   104   private def install(view: View)
       
   105   {
    82     val buffer = view.getBuffer
   106     val buffer = view.getBuffer
    83     val prover_setup = new ProverSetup(buffer)
   107     val prover_setup = new ProverSetup(buffer)
    84     mapping.update(buffer, prover_setup)
   108     mapping.update(buffer, prover_setup)
    85     prover_setup.activate(view)
   109     prover_setup.activate(view)
    86   }
   110   }
    87 
   111 
    88   private def uninstall(view: View) =
   112   private def uninstall(view: View) =
    89     mapping.removeKey(view.getBuffer).get.deactivate
   113     mapping.removeKey(view.getBuffer).get.deactivate
    90 
   114 
    91   def switch_active (view : View) =
   115   def switch_active (view: View) =
    92     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   116     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
    93     else install(view)
   117     else install(view)
    94 
   118 
    95   def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
   119   def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
    96   def is_active (buffer : JEditBuffer) = mapping.isDefinedAt(buffer)
   120   def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
    97   
       
    98   
       
    99   // main plugin plumbing
       
   100 
   121 
   101   override def handleMessage(msg: EBMessage) = msg match {
   122 
   102     case epu: EditPaneUpdate => epu.getWhat match {
   123   /* main plugin plumbing */
   103       case EditPaneUpdate.BUFFER_CHANGED =>
   124 
   104         mapping get epu.getEditPane.getBuffer match {
   125   override def handleMessage(msg: EBMessage)
   105           //only activate 'isabelle'-buffers!
   126   {
   106           case None =>
   127     msg match {
   107           case Some(prover_setup) => 
   128       case epu: EditPaneUpdate => epu.getWhat match {
   108             prover_setup.theory_view.activate
   129         case EditPaneUpdate.BUFFER_CHANGED =>
   109             val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
   130           mapping get epu.getEditPane.getBuffer match {
   110             if (dockable != null) {
   131             // only activate 'isabelle' buffers
   111               val output_dockable = dockable.asInstanceOf[OutputDockable]
   132             case None =>
   112               if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
   133             case Some(prover_setup) =>
   113                 output_dockable.asInstanceOf[OutputDockable].removeAll
   134               prover_setup.theory_view.activate
   114                 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
   135               val dockable =
   115                 output_dockable.revalidate
   136                 epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
       
   137               if (dockable != null) {
       
   138                 val output_dockable = dockable.asInstanceOf[OutputDockable]
       
   139                 if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
       
   140                   output_dockable.asInstanceOf[OutputDockable].removeAll
       
   141                   output_dockable.asInstanceOf[OutputDockable].
       
   142                     add(new JScrollPane(prover_setup.output_text_view))
       
   143                   output_dockable.revalidate
       
   144                 }
   116               }
   145               }
   117             }
   146           }
   118         }
   147         case EditPaneUpdate.BUFFER_CHANGING =>
   119       case EditPaneUpdate.BUFFER_CHANGING =>
   148           val buffer = epu.getEditPane.getBuffer
   120         val buffer = epu.getEditPane.getBuffer
   149           if (buffer != null) mapping get buffer match {
   121         if (buffer != null) mapping get buffer match {
   150             // only deactivate 'isabelle' buffers
   122           //only deactivate 'isabelle'-buffers!
   151             case None =>
   123           case None =>
   152             case Some(prover_setup) => prover_setup.theory_view.deactivate
   124           case Some(prover_setup) => prover_setup.theory_view.deactivate
   153           }
   125         }
   154         case _ =>
       
   155       }
   126       case _ =>
   156       case _ =>
   127     }
   157     }
   128     case _ =>
       
   129   }
   158   }
   130 
   159 
   131   override def start() {
   160   override def start()
       
   161   {
   132     Isabelle.system = new Isabelle_System
   162     Isabelle.system = new Isabelle_System
   133     Isabelle.plugin = this
   163     Isabelle.plugin = this
   134     
   164     set_font(Isabelle.Int_Property("font-size"))
   135     if (Isabelle.Property("font-path") != null && Isabelle.Property("font-size") != null)
       
   136       try {
       
   137         set_font(Isabelle.Property("font-path"), Isabelle.Property("font-size").toFloat)
       
   138       }
       
   139       catch {
       
   140         case e: NumberFormatException =>
       
   141       }
       
   142   }
   165   }
   143   
   166 
   144   override def stop() {
   167   override def stop()
       
   168   {
   145     // TODO: proper cleanup
   169     // TODO: proper cleanup
   146     Isabelle.system = null
   170     Isabelle.system = null
   147     Isabelle.plugin = null
   171     Isabelle.plugin = null
   148   }
   172   }
       
   173 
   149 }
   174 }