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@34760
|
6 |
* @author Makarius
|
wenzelm@34407
|
7 |
*/
|
wenzelm@34407
|
8 |
|
wenzelm@34318
|
9 |
package isabelle.jedit
|
wenzelm@34318
|
10 |
|
wenzelm@34429
|
11 |
|
wenzelm@36015
|
12 |
import isabelle._
|
wenzelm@36015
|
13 |
|
wenzelm@34429
|
14 |
import java.io.{FileInputStream, IOException}
|
wenzelm@34318
|
15 |
import java.awt.Font
|
wenzelm@34822
|
16 |
import javax.swing.JTextArea
|
wenzelm@34318
|
17 |
|
wenzelm@34497
|
18 |
import scala.collection.mutable
|
immler@34406
|
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@34618
|
26 |
object Isabelle
|
wenzelm@34618
|
27 |
{
|
wenzelm@34784
|
28 |
/* plugin instance */
|
wenzelm@34784
|
29 |
|
wenzelm@34784
|
30 |
var system: Isabelle_System = null
|
wenzelm@34784
|
31 |
var session: Session = null
|
wenzelm@34784
|
32 |
|
wenzelm@34784
|
33 |
|
wenzelm@34618
|
34 |
/* name */
|
wenzelm@34618
|
35 |
|
wenzelm@34318
|
36 |
val NAME = "Isabelle"
|
wenzelm@34623
|
37 |
|
wenzelm@34618
|
38 |
|
wenzelm@34618
|
39 |
/* properties */
|
wenzelm@34618
|
40 |
|
wenzelm@34618
|
41 |
val OPTION_PREFIX = "options.isabelle."
|
wenzelm@34618
|
42 |
|
wenzelm@34618
|
43 |
object Property
|
wenzelm@34618
|
44 |
{
|
wenzelm@34618
|
45 |
def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
|
wenzelm@34468
|
46 |
def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
|
wenzelm@34468
|
47 |
}
|
wenzelm@34433
|
48 |
|
wenzelm@34618
|
49 |
object Boolean_Property
|
wenzelm@34618
|
50 |
{
|
wenzelm@34618
|
51 |
def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
|
wenzelm@34618
|
52 |
def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
|
wenzelm@34618
|
53 |
}
|
wenzelm@34618
|
54 |
|
wenzelm@34618
|
55 |
object Int_Property
|
wenzelm@34618
|
56 |
{
|
wenzelm@34618
|
57 |
def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
|
wenzelm@34618
|
58 |
def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
|
wenzelm@34618
|
59 |
}
|
wenzelm@34618
|
60 |
|
wenzelm@34618
|
61 |
|
wenzelm@34618
|
62 |
/* settings */
|
wenzelm@34618
|
63 |
|
wenzelm@34782
|
64 |
def default_logic(): String =
|
wenzelm@34782
|
65 |
{
|
wenzelm@34782
|
66 |
val logic = system.getenv("JEDIT_LOGIC")
|
wenzelm@34782
|
67 |
if (logic != "") logic
|
wenzelm@34782
|
68 |
else system.getenv_strict("ISABELLE_LOGIC")
|
wenzelm@34782
|
69 |
}
|
wenzelm@34782
|
70 |
|
wenzelm@34782
|
71 |
def isabelle_args(): List[String] =
|
wenzelm@34618
|
72 |
{
|
wenzelm@34780
|
73 |
val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
|
wenzelm@34780
|
74 |
val logic = {
|
wenzelm@34784
|
75 |
val logic = Property("logic")
|
wenzelm@34782
|
76 |
if (logic != null && logic != "") logic
|
wenzelm@34782
|
77 |
else default_logic()
|
wenzelm@34780
|
78 |
}
|
wenzelm@34780
|
79 |
modes ++ List(logic)
|
wenzelm@34502
|
80 |
}
|
wenzelm@34502
|
81 |
|
wenzelm@34618
|
82 |
|
wenzelm@34784
|
83 |
/* main jEdit components */ // FIXME ownership!?
|
wenzelm@34784
|
84 |
|
wenzelm@34784
|
85 |
def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
|
wenzelm@34784
|
86 |
|
wenzelm@34784
|
87 |
def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
|
wenzelm@34784
|
88 |
|
wenzelm@34784
|
89 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
|
wenzelm@34784
|
90 |
Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
|
wenzelm@34784
|
91 |
|
wenzelm@34784
|
92 |
def jedit_text_areas(): Iterator[JEditTextArea] =
|
wenzelm@34784
|
93 |
jedit_views().flatMap(jedit_text_areas(_))
|
wenzelm@34784
|
94 |
|
wenzelm@34784
|
95 |
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
|
wenzelm@34784
|
96 |
jedit_text_areas().filter(_.getBuffer == buffer)
|
wenzelm@34784
|
97 |
|
wenzelm@34784
|
98 |
|
wenzelm@34820
|
99 |
/* manage prover */
|
wenzelm@34820
|
100 |
|
wenzelm@34820
|
101 |
private def prover_started(view: View): Boolean =
|
wenzelm@34820
|
102 |
{
|
wenzelm@34820
|
103 |
val timeout = Int_Property("startup-timeout") max 1000
|
wenzelm@34820
|
104 |
session.start(timeout, Isabelle.isabelle_args()) match {
|
wenzelm@34820
|
105 |
case Some(err) =>
|
wenzelm@34822
|
106 |
val text = new JTextArea(err); text.setEditable(false)
|
wenzelm@34822
|
107 |
Library.error_dialog(view, null, "Failed to start Isabelle process", text)
|
wenzelm@34820
|
108 |
false
|
wenzelm@34820
|
109 |
case None => true
|
wenzelm@34820
|
110 |
}
|
wenzelm@34820
|
111 |
}
|
wenzelm@34820
|
112 |
|
wenzelm@34820
|
113 |
|
wenzelm@34784
|
114 |
/* activation */
|
wenzelm@34784
|
115 |
|
wenzelm@34820
|
116 |
def activate_buffer(view: View, buffer: Buffer)
|
wenzelm@34784
|
117 |
{
|
wenzelm@34820
|
118 |
if (prover_started(view)) {
|
wenzelm@34820
|
119 |
val model = Document_Model.init(session, buffer)
|
wenzelm@34820
|
120 |
for (text_area <- jedit_text_areas(buffer))
|
wenzelm@34820
|
121 |
Document_View.init(model, text_area)
|
wenzelm@34820
|
122 |
}
|
wenzelm@34784
|
123 |
}
|
wenzelm@34784
|
124 |
|
wenzelm@34784
|
125 |
def deactivate_buffer(buffer: Buffer)
|
wenzelm@34784
|
126 |
{
|
wenzelm@34784
|
127 |
session.stop() // FIXME not yet
|
wenzelm@34784
|
128 |
|
wenzelm@34784
|
129 |
for (text_area <- jedit_text_areas(buffer))
|
wenzelm@34784
|
130 |
Document_View.exit(text_area)
|
wenzelm@34784
|
131 |
Document_Model.exit(buffer)
|
wenzelm@34784
|
132 |
}
|
wenzelm@34784
|
133 |
|
wenzelm@34784
|
134 |
def switch_active(view: View) =
|
wenzelm@34784
|
135 |
{
|
wenzelm@34784
|
136 |
val buffer = view.getBuffer
|
wenzelm@34788
|
137 |
if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
|
wenzelm@34820
|
138 |
else activate_buffer(view, buffer)
|
wenzelm@34784
|
139 |
}
|
wenzelm@34784
|
140 |
|
wenzelm@34784
|
141 |
def is_active(view: View): Boolean =
|
wenzelm@34788
|
142 |
Document_Model(view.getBuffer).isDefined
|
wenzelm@34318
|
143 |
}
|
wenzelm@34318
|
144 |
|
wenzelm@34429
|
145 |
|
wenzelm@34618
|
146 |
class Plugin extends EBPlugin
|
wenzelm@34618
|
147 |
{
|
wenzelm@34618
|
148 |
/* main plugin plumbing */
|
wenzelm@34433
|
149 |
|
wenzelm@34767
|
150 |
override def handleMessage(message: EBMessage)
|
wenzelm@34618
|
151 |
{
|
wenzelm@34767
|
152 |
message match {
|
wenzelm@34767
|
153 |
case msg: EditPaneUpdate =>
|
wenzelm@34784
|
154 |
val edit_pane = msg.getEditPane
|
wenzelm@34784
|
155 |
val buffer = edit_pane.getBuffer
|
wenzelm@34784
|
156 |
val text_area = edit_pane.getTextArea
|
wenzelm@34784
|
157 |
|
wenzelm@34787
|
158 |
def init_view()
|
wenzelm@34787
|
159 |
{
|
wenzelm@34788
|
160 |
Document_Model(buffer) match {
|
wenzelm@34787
|
161 |
case Some(model) => Document_View.init(model, text_area)
|
wenzelm@34787
|
162 |
case None =>
|
wenzelm@34787
|
163 |
}
|
wenzelm@34787
|
164 |
}
|
wenzelm@34787
|
165 |
def exit_view()
|
wenzelm@34787
|
166 |
{
|
wenzelm@34788
|
167 |
if (Document_View(text_area).isDefined)
|
wenzelm@34787
|
168 |
Document_View.exit(text_area)
|
wenzelm@34787
|
169 |
}
|
wenzelm@34767
|
170 |
msg.getWhat match {
|
wenzelm@34787
|
171 |
case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
|
wenzelm@34787
|
172 |
case EditPaneUpdate.CREATED => init_view()
|
wenzelm@34787
|
173 |
case EditPaneUpdate.DESTROYED => exit_view()
|
immler@34671
|
174 |
case _ =>
|
immler@34671
|
175 |
}
|
wenzelm@34784
|
176 |
|
wenzelm@34777
|
177 |
case msg: PropertiesChanged =>
|
wenzelm@34791
|
178 |
Isabelle.session.global_settings.event(Session.Global_Settings)
|
wenzelm@34784
|
179 |
|
wenzelm@34318
|
180 |
case _ =>
|
wenzelm@34318
|
181 |
}
|
wenzelm@34318
|
182 |
}
|
wenzelm@34318
|
183 |
|
wenzelm@34618
|
184 |
override def start()
|
wenzelm@34618
|
185 |
{
|
wenzelm@34615
|
186 |
Isabelle.system = new Isabelle_System
|
wenzelm@34774
|
187 |
Isabelle.system.install_fonts()
|
wenzelm@34777
|
188 |
Isabelle.session = new Session(Isabelle.system) // FIXME dialog!?
|
wenzelm@34318
|
189 |
}
|
wenzelm@34618
|
190 |
|
wenzelm@34618
|
191 |
override def stop()
|
wenzelm@34618
|
192 |
{
|
wenzelm@34777
|
193 |
Isabelle.session.stop() // FIXME dialog!?
|
wenzelm@34777
|
194 |
Isabelle.session = null
|
wenzelm@34441
|
195 |
Isabelle.system = null
|
wenzelm@34318
|
196 |
}
|
wenzelm@34318
|
197 |
}
|