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@34429
|
10 |
|
wenzelm@34429
|
11 |
import java.io.{FileInputStream, IOException}
|
wenzelm@34318
|
12 |
import java.awt.Font
|
immler@34406
|
13 |
import javax.swing.JScrollPane
|
wenzelm@34318
|
14 |
|
wenzelm@34497
|
15 |
import scala.collection.mutable
|
immler@34406
|
16 |
|
wenzelm@34429
|
17 |
import isabelle.prover.{Prover, Command}
|
wenzelm@34487
|
18 |
import isabelle.IsabelleSystem
|
wenzelm@34429
|
19 |
|
wenzelm@34429
|
20 |
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
|
immler@34406
|
21 |
import org.gjt.sp.jedit.buffer.JEditBuffer
|
immler@34406
|
22 |
import org.gjt.sp.jedit.textarea.JEditTextArea
|
wenzelm@34429
|
23 |
import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
|
wenzelm@34429
|
24 |
|
wenzelm@34318
|
25 |
|
wenzelm@34440
|
26 |
object Isabelle {
|
wenzelm@34433
|
27 |
// name
|
wenzelm@34318
|
28 |
val NAME = "Isabelle"
|
wenzelm@34337
|
29 |
val VFS_PREFIX = "isabelle:"
|
wenzelm@34433
|
30 |
|
wenzelm@34433
|
31 |
// properties
|
wenzelm@34468
|
32 |
object Property {
|
wenzelm@34468
|
33 |
private val OPTION_PREFIX = "options.isabelle."
|
wenzelm@34468
|
34 |
def apply(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
|
wenzelm@34468
|
35 |
def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
|
wenzelm@34468
|
36 |
}
|
wenzelm@34433
|
37 |
|
wenzelm@34487
|
38 |
// Isabelle system instance
|
wenzelm@34441
|
39 |
var system: IsabelleSystem = null
|
wenzelm@34487
|
40 |
def symbols = system.symbols
|
wenzelm@34612
|
41 |
lazy val completion = new Completion + symbols
|
wenzelm@34440
|
42 |
|
wenzelm@34502
|
43 |
// settings
|
wenzelm@34502
|
44 |
def default_logic = {
|
wenzelm@34502
|
45 |
val logic = Isabelle.Property("logic")
|
wenzelm@34502
|
46 |
if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
|
wenzelm@34502
|
47 |
}
|
wenzelm@34502
|
48 |
|
wenzelm@34440
|
49 |
// plugin instance
|
wenzelm@34440
|
50 |
var plugin: Plugin = null
|
wenzelm@34433
|
51 |
|
wenzelm@34487
|
52 |
// running provers
|
immler@34475
|
53 |
def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
|
wenzelm@34318
|
54 |
}
|
wenzelm@34318
|
55 |
|
wenzelm@34429
|
56 |
|
wenzelm@34318
|
57 |
class Plugin extends EBPlugin {
|
wenzelm@34433
|
58 |
|
wenzelm@34433
|
59 |
// Isabelle font
|
wenzelm@34433
|
60 |
|
wenzelm@34433
|
61 |
var font: Font = null
|
wenzelm@34456
|
62 |
val font_changed = new EventBus[Font]
|
immler@34406
|
63 |
|
wenzelm@34433
|
64 |
def set_font(path: String, size: Float) {
|
wenzelm@34456
|
65 |
font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
|
wenzelm@34456
|
66 |
deriveFont(Font.PLAIN, size)
|
wenzelm@34456
|
67 |
font_changed.event(font)
|
wenzelm@34433
|
68 |
}
|
wenzelm@34433
|
69 |
|
wenzelm@34433
|
70 |
|
wenzelm@34449
|
71 |
/* unique ids */ // FIXME specific to "session" (!??)
|
wenzelm@34449
|
72 |
|
wenzelm@34449
|
73 |
private var id_count: BigInt = 0
|
wenzelm@34449
|
74 |
def id() : String = synchronized { id_count += 1; "editor:" + id_count }
|
wenzelm@34449
|
75 |
|
wenzelm@34449
|
76 |
|
wenzelm@34433
|
77 |
// mapping buffer <-> prover
|
wenzelm@34433
|
78 |
|
wenzelm@34497
|
79 |
private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
|
immler@34406
|
80 |
|
immler@34463
|
81 |
private def install(view: View) {
|
immler@34406
|
82 |
val buffer = view.getBuffer
|
immler@34463
|
83 |
val prover_setup = new ProverSetup(buffer)
|
immler@34463
|
84 |
mapping.update(buffer, prover_setup)
|
immler@34463
|
85 |
prover_setup.activate(view)
|
wenzelm@34318
|
86 |
}
|
immler@34406
|
87 |
|
immler@34463
|
88 |
private def uninstall(view: View) =
|
immler@34463
|
89 |
mapping.removeKey(view.getBuffer).get.deactivate
|
immler@34463
|
90 |
|
immler@34463
|
91 |
def switch_active (view : View) =
|
immler@34463
|
92 |
if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
|
immler@34463
|
93 |
else install(view)
|
immler@34406
|
94 |
|
immler@34406
|
95 |
def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
|
immler@34462
|
96 |
def is_active (buffer : JEditBuffer) = mapping.isDefinedAt(buffer)
|
immler@34463
|
97 |
|
wenzelm@34318
|
98 |
|
wenzelm@34433
|
99 |
// main plugin plumbing
|
wenzelm@34433
|
100 |
|
wenzelm@34429
|
101 |
override def handleMessage(msg: EBMessage) = msg match {
|
wenzelm@34433
|
102 |
case epu: EditPaneUpdate => epu.getWhat match {
|
wenzelm@34318
|
103 |
case EditPaneUpdate.BUFFER_CHANGED =>
|
immler@34406
|
104 |
mapping get epu.getEditPane.getBuffer match {
|
immler@34406
|
105 |
//only activate 'isabelle'-buffers!
|
immler@34406
|
106 |
case None =>
|
immler@34406
|
107 |
case Some(prover_setup) =>
|
immler@34406
|
108 |
prover_setup.theory_view.activate
|
wenzelm@34422
|
109 |
val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
|
wenzelm@34503
|
110 |
if (dockable != null) {
|
immler@34406
|
111 |
val output_dockable = dockable.asInstanceOf[OutputDockable]
|
wenzelm@34503
|
112 |
if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
|
immler@34406
|
113 |
output_dockable.asInstanceOf[OutputDockable].removeAll
|
immler@34406
|
114 |
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
|
immler@34406
|
115 |
output_dockable.revalidate
|
immler@34406
|
116 |
}
|
immler@34406
|
117 |
}
|
immler@34406
|
118 |
}
|
wenzelm@34318
|
119 |
case EditPaneUpdate.BUFFER_CHANGING =>
|
immler@34406
|
120 |
val buffer = epu.getEditPane.getBuffer
|
wenzelm@34503
|
121 |
if (buffer != null) mapping get buffer match {
|
immler@34406
|
122 |
//only deactivate 'isabelle'-buffers!
|
immler@34406
|
123 |
case None =>
|
immler@34406
|
124 |
case Some(prover_setup) => prover_setup.theory_view.deactivate
|
immler@34406
|
125 |
}
|
wenzelm@34318
|
126 |
case _ =>
|
wenzelm@34318
|
127 |
}
|
wenzelm@34318
|
128 |
case _ =>
|
wenzelm@34318
|
129 |
}
|
wenzelm@34318
|
130 |
|
wenzelm@34318
|
131 |
override def start() {
|
wenzelm@34441
|
132 |
Isabelle.system = new IsabelleSystem
|
wenzelm@34440
|
133 |
Isabelle.plugin = this
|
immler@34406
|
134 |
|
wenzelm@34468
|
135 |
if (Isabelle.Property("font-path") != null && Isabelle.Property("font-size") != null)
|
wenzelm@34318
|
136 |
try {
|
wenzelm@34468
|
137 |
set_font(Isabelle.Property("font-path"), Isabelle.Property("font-size").toFloat)
|
wenzelm@34318
|
138 |
}
|
wenzelm@34318
|
139 |
catch {
|
wenzelm@34429
|
140 |
case e: NumberFormatException =>
|
wenzelm@34318
|
141 |
}
|
wenzelm@34318
|
142 |
}
|
wenzelm@34318
|
143 |
|
wenzelm@34318
|
144 |
override def stop() {
|
wenzelm@34429
|
145 |
// TODO: proper cleanup
|
wenzelm@34441
|
146 |
Isabelle.system = null
|
wenzelm@34440
|
147 |
Isabelle.plugin = null
|
wenzelm@34318
|
148 |
}
|
wenzelm@34318
|
149 |
}
|