author | wenzelm |
Fri, 11 Dec 2009 22:40:55 +0100 | |
changeset 34779 | d1040b77b189 |
parent 34777 | 91d6089cef88 |
child 34780 | d0ff1c3a91ea |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
2 |
* Main Isabelle/jEdit plugin setup |
|
3 |
* |
|
4 |
* @author Johannes Hölzl, TU Munich |
|
5 |
* @author Fabian Immler, TU Munich |
|
34760 | 6 |
* @author Makarius |
34407 | 7 |
*/ |
8 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
34429 | 11 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
12 |
import isabelle.proofdocument.{Session, Theory_View} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
13 |
|
34429 | 14 |
import java.io.{FileInputStream, IOException} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
import java.awt.Font |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
16 |
import javax.swing.JScrollPane |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
|
34497 | 18 |
import scala.collection.mutable |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
19 |
|
34429 | 20 |
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
21 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
22 |
import org.gjt.sp.jedit.textarea.JEditTextArea |
34429 | 23 |
import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged} |
24 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
25 |
|
34618 | 26 |
object Isabelle |
27 |
{ |
|
28 |
/* name */ |
|
29 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
30 |
val NAME = "Isabelle" |
34623 | 31 |
|
34618 | 32 |
|
33 |
/* properties */ |
|
34 |
||
35 |
val OPTION_PREFIX = "options.isabelle." |
|
36 |
||
37 |
object Property |
|
38 |
{ |
|
39 |
def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name) |
|
34468
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34463
diff
changeset
|
40 |
def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value) |
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34463
diff
changeset
|
41 |
} |
34433 | 42 |
|
34618 | 43 |
object Boolean_Property |
44 |
{ |
|
45 |
def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name) |
|
46 |
def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value) |
|
47 |
} |
|
48 |
||
49 |
object Int_Property |
|
50 |
{ |
|
51 |
def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name) |
|
52 |
def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value) |
|
53 |
} |
|
54 |
||
55 |
||
56 |
/* settings */ |
|
57 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
58 |
def get_logic(): String = |
34618 | 59 |
{ |
34502 | 60 |
val logic = Isabelle.Property("logic") |
34703 | 61 |
if (logic != null) logic |
62 |
else system.getenv_strict("ISABELLE_LOGIC") |
|
34502 | 63 |
} |
64 |
||
34618 | 65 |
|
66 |
/* plugin instance */ |
|
67 |
||
34440 | 68 |
var plugin: Plugin = null |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
69 |
var system: Isabelle_System = null |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
70 |
var session: Session = null |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
71 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
72 |
|
34429 | 73 |
|
34618 | 74 |
class Plugin extends EBPlugin |
75 |
{ |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
76 |
/* mapping buffer <-> theory view */ |
34669 | 77 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
78 |
private var mapping = Map[JEditBuffer, Theory_View]() |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
79 |
|
34618 | 80 |
private def install(view: View) |
81 |
{ |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
82 |
val text_area = view.getTextArea |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
83 |
val buffer = view.getBuffer |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
84 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
85 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
86 |
val theory_view = new Theory_View(Isabelle.session, text_area) // FIXME multiple text areas!? |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
87 |
mapping += (buffer -> theory_view) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
88 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
89 |
Isabelle.session.start(Isabelle.get_logic()) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
90 |
theory_view.activate() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
91 |
Isabelle.session.begin_document(buffer.getName) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
92 |
} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
93 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
94 |
private def uninstall(view: View) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
95 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
96 |
val buffer = view.getBuffer |
34779 | 97 |
Isabelle.session.stop() |
98 |
mapping(buffer).deactivate() |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
99 |
mapping -= buffer |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
100 |
} |
34463
b510b7d88de2
changed install/uninstall prover on view to private
immler@in.tum.de
parents:
34462
diff
changeset
|
101 |
|
34764 | 102 |
def switch_active(view: View) = |
34463
b510b7d88de2
changed install/uninstall prover on view to private
immler@in.tum.de
parents:
34462
diff
changeset
|
103 |
if (mapping.isDefinedAt(view.getBuffer)) uninstall(view) |
b510b7d88de2
changed install/uninstall prover on view to private
immler@in.tum.de
parents:
34462
diff
changeset
|
104 |
else install(view) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
105 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
106 |
def theory_view(buffer: JEditBuffer): Option[Theory_View] = mapping.get(buffer) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
107 |
def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer) |
34618 | 108 |
|
109 |
||
110 |
/* main plugin plumbing */ |
|
34433 | 111 |
|
34767 | 112 |
override def handleMessage(message: EBMessage) |
34618 | 113 |
{ |
34767 | 114 |
message match { |
115 |
case msg: EditPaneUpdate => |
|
116 |
val buffer = msg.getEditPane.getBuffer |
|
117 |
msg.getWhat match { |
|
34671 | 118 |
case EditPaneUpdate.BUFFER_CHANGED => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
119 |
theory_view(buffer)map(_.activate) |
34671 | 120 |
case EditPaneUpdate.BUFFER_CHANGING => |
121 |
if (buffer != null) |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
122 |
theory_view(buffer).map(_.deactivate) |
34671 | 123 |
case _ => |
124 |
} |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
125 |
case msg: PropertiesChanged => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
126 |
Isabelle.session.global_settings.event(()) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
127 |
case _ => |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
128 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
129 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
130 |
|
34618 | 131 |
override def start() |
132 |
{ |
|
34751
6ed1b3701459
simplified treatment of Isabelle fonts, via Isabelle_System.register_fonts (requires Java 1.6);
wenzelm
parents:
34732
diff
changeset
|
133 |
Isabelle.plugin = this |
34615 | 134 |
Isabelle.system = new Isabelle_System |
34774 | 135 |
Isabelle.system.install_fonts() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
136 |
Isabelle.session = new Session(Isabelle.system) // FIXME dialog!? |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
137 |
} |
34618 | 138 |
|
139 |
override def stop() |
|
140 |
{ |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
141 |
Isabelle.session.stop() // FIXME dialog!? |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
142 |
Isabelle.session = null |
34441
ff3b7ae2b12a
replaced static IsabelleSystem by Isabelle.system;
wenzelm
parents:
34440
diff
changeset
|
143 |
Isabelle.system = null |
34440 | 144 |
Isabelle.plugin = null |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
145 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
146 |
} |