author | wenzelm |
Mon, 29 Dec 2008 20:43:04 +0100 | |
changeset 34456 | 14367c0715e8 |
parent 34449 | 57fce8528a22 |
child 34462 | fefbd0421e4e |
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 |
|
6 |
*/ |
|
7 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
34429 | 10 |
|
11 |
import java.io.{FileInputStream, IOException} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.Font |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
13 |
import javax.swing.JScrollPane |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
15 |
import scala.collection.mutable.HashMap |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
16 |
|
34429 | 17 |
import isabelle.prover.{Prover, Command} |
34433 | 18 |
import isabelle.{IsabelleSystem, Symbol} |
34429 | 19 |
|
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 |
|
34440 | 26 |
object Isabelle { |
34433 | 27 |
// name |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
28 |
val NAME = "Isabelle" |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
29 |
val OPTION_PREFIX = "options.isabelle." |
34337
5d5b69f2956b
renamed VFS protocol prefix from "isa:" to "isabelle:";
wenzelm
parents:
34318
diff
changeset
|
30 |
val VFS_PREFIX = "isabelle:" |
34433 | 31 |
|
32 |
// properties |
|
34429 | 33 |
def property(name: String) = jEdit.getProperty(OPTION_PREFIX + name) |
34 |
def property(name: String, value: String) = |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
35 |
jEdit.setProperty(OPTION_PREFIX + name, value) |
34433 | 36 |
|
34440 | 37 |
|
34441
ff3b7ae2b12a
replaced static IsabelleSystem by Isabelle.system;
wenzelm
parents:
34440
diff
changeset
|
38 |
// Isabelle system |
ff3b7ae2b12a
replaced static IsabelleSystem by Isabelle.system;
wenzelm
parents:
34440
diff
changeset
|
39 |
var system: IsabelleSystem = null |
34440 | 40 |
var symbols: Symbol.Interpretation = null |
41 |
||
42 |
||
43 |
// plugin instance |
|
44 |
var plugin: Plugin = null |
|
34433 | 45 |
|
46 |
// provers |
|
34440 | 47 |
def prover(buffer: JEditBuffer) = plugin.prover_setup(buffer).get.prover |
48 |
def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer).get |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
49 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
50 |
|
34429 | 51 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
52 |
class Plugin extends EBPlugin { |
34433 | 53 |
|
54 |
// Isabelle font |
|
55 |
||
56 |
var font: Font = null |
|
34456 | 57 |
val font_changed = new EventBus[Font] |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
58 |
|
34433 | 59 |
def set_font(path: String, size: Float) { |
34456 | 60 |
font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)). |
61 |
deriveFont(Font.PLAIN, size) |
|
62 |
font_changed.event(font) |
|
34433 | 63 |
} |
64 |
||
65 |
||
34449 | 66 |
/* unique ids */ // FIXME specific to "session" (!??) |
67 |
||
68 |
private var id_count: BigInt = 0 |
|
69 |
def id() : String = synchronized { id_count += 1; "editor:" + id_count } |
|
70 |
||
71 |
||
34433 | 72 |
// mapping buffer <-> prover |
73 |
||
74 |
private val mapping = new HashMap[JEditBuffer, ProverSetup] |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
75 |
|
34429 | 76 |
def install(view: View) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
77 |
val buffer = view.getBuffer |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
78 |
mapping.get(buffer) match{ |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
79 |
case None =>{ |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
80 |
val prover_setup = new ProverSetup(buffer) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
81 |
mapping.update(buffer, prover_setup) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
82 |
prover_setup.activate(view) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
83 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
84 |
case _ => System.err.println("Already installed plugin on Buffer") |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
85 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
86 |
} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
87 |
|
34429 | 88 |
def uninstall(view: View) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
89 |
val buffer = view.getBuffer |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
90 |
mapping.removeKey(buffer) match{ |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
91 |
case None => System.err.println("No Plugin installed on this Buffer") |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
92 |
case Some(proversetup) => |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
93 |
proversetup.deactivate |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
94 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
95 |
} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
96 |
|
34429 | 97 |
def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer) |
34433 | 98 |
def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer) |
99 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
100 |
|
34433 | 101 |
// main plugin plumbing |
102 |
||
34429 | 103 |
override def handleMessage(msg: EBMessage) = msg match { |
34433 | 104 |
case epu: EditPaneUpdate => epu.getWhat match { |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
105 |
case EditPaneUpdate.BUFFER_CHANGED => |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
106 |
mapping get epu.getEditPane.getBuffer match { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
107 |
//only activate 'isabelle'-buffers! |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
108 |
case None => |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
109 |
case Some(prover_setup) => |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
110 |
prover_setup.theory_view.activate |
34422 | 111 |
val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output") |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
112 |
if(dockable != null) { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
113 |
val output_dockable = dockable.asInstanceOf[OutputDockable] |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
114 |
if(output_dockable.getComponent(0) != prover_setup.output_text_view ) { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
115 |
output_dockable.asInstanceOf[OutputDockable].removeAll |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
116 |
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view)) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
117 |
output_dockable.revalidate |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
118 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
119 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
120 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
121 |
case EditPaneUpdate.BUFFER_CHANGING => |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
122 |
val buffer = epu.getEditPane.getBuffer |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
123 |
if(buffer != null) mapping get buffer match { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
124 |
//only deactivate 'isabelle'-buffers! |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
125 |
case None => |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
126 |
case Some(prover_setup) => prover_setup.theory_view.deactivate |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
127 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
128 |
case _ => |
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 |
case _ => |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
131 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
132 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
133 |
override def start() { |
34441
ff3b7ae2b12a
replaced static IsabelleSystem by Isabelle.system;
wenzelm
parents:
34440
diff
changeset
|
134 |
Isabelle.system = new IsabelleSystem |
34443
f2e13329cc49
dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents:
34441
diff
changeset
|
135 |
Isabelle.symbols = new Symbol.Interpretation(Isabelle.system) |
34440 | 136 |
Isabelle.plugin = this |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
137 |
|
34440 | 138 |
if (Isabelle.property("font-path") != null && Isabelle.property("font-size") != null) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
139 |
try { |
34440 | 140 |
set_font(Isabelle.property("font-path"), Isabelle.property("font-size").toFloat) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
141 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
142 |
catch { |
34429 | 143 |
case e: NumberFormatException => |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
144 |
} |
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 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
147 |
override def stop() { |
34429 | 148 |
// TODO: proper cleanup |
34441
ff3b7ae2b12a
replaced static IsabelleSystem by Isabelle.system;
wenzelm
parents:
34440
diff
changeset
|
149 |
Isabelle.symbols = null |
ff3b7ae2b12a
replaced static IsabelleSystem by Isabelle.system;
wenzelm
parents:
34440
diff
changeset
|
150 |
Isabelle.system = null |
34440 | 151 |
Isabelle.plugin = null |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
152 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
153 |
} |