author | wenzelm |
Tue, 20 Jan 2009 13:56:55 +0100 | |
changeset 34486 | 7985efd78aa1 |
parent 34470 | f4c033b33630 |
child 34490 | 820d0675e7b5 |
permissions | -rw-r--r-- |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
1 |
/* |
34408 | 2 |
* Independent prover sessions |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
3 |
* |
34408 | 4 |
* @author Fabian Immler, TU Munich |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
5 |
*/ |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
6 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
7 |
package isabelle.jedit |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
8 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
9 |
|
34431 | 10 |
import isabelle.prover.{Prover, Command} |
34438 | 11 |
import isabelle.renderer.UserAgent |
12 |
||
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
13 |
|
34431 | 14 |
import org.w3c.dom.Document |
15 |
||
16 |
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, View} |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
34431 | 18 |
import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
19 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
20 |
import javax.swing.{JTextArea, JScrollPane} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
21 |
|
34431 | 22 |
|
34456 | 23 |
class ProverSetup(buffer: JEditBuffer) |
24 |
{ |
|
34443
f2e13329cc49
dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents:
34441
diff
changeset
|
25 |
val prover = new Prover(Isabelle.system, Isabelle.symbols) |
34456 | 26 |
var theory_view: TheoryView = null |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
27 |
|
34456 | 28 |
val state_update = new EventBus[Command] |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
29 |
|
34456 | 30 |
private var _selected_state: Command = null |
31 |
def selected_state = _selected_state |
|
32 |
def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) } |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
33 |
|
34456 | 34 |
val output_text_view = new JTextArea |
35 |
||
36 |
def activate(view: View) { |
|
34468
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34467
diff
changeset
|
37 |
prover.start(Isabelle.Property("logic")) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
38 |
val buffer = view.getBuffer |
34456 | 39 |
val dir = buffer.getDirectory |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
40 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
41 |
theory_view = new TheoryView(view.getTextArea) |
34456 | 42 |
prover.set_document(theory_view, |
43 |
if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir) |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
44 |
theory_view.activate |
34467 | 45 |
|
46 |
//register output-view |
|
34456 | 47 |
prover.output_info += (text => |
48 |
{ |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
49 |
output_text_view.append(text) |
34422 | 50 |
val dockable = view.getDockableWindowManager.getDockable("isabelle-output") |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
51 |
//link process output if dockable is active |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
52 |
if(dockable != null) { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
53 |
val output_dockable = dockable.asInstanceOf[OutputDockable] |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
54 |
if(output_dockable.getComponent(0) != output_text_view ) { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
55 |
output_dockable.asInstanceOf[OutputDockable].removeAll |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
56 |
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view)) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
57 |
output_dockable.revalidate |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
58 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
59 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
60 |
}) |
34456 | 61 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
62 |
//register for state-view |
34456 | 63 |
state_update += (state => { |
34422 | 64 |
val state_view = view.getDockableWindowManager.getDockable("isabelle-state") |
34456 | 65 |
val state_panel = |
66 |
if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel |
|
67 |
else null |
|
68 |
if (state_panel != null){ |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
69 |
if (state == null) |
34456 | 70 |
state_panel.setDocument(null: Document) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
71 |
else |
34486 | 72 |
state_panel.setDocument(state.result_document, UserAgent.baseURL) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
73 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
74 |
}) |
34467 | 75 |
|
76 |
// one independent token marker per prover |
|
77 |
val token_marker = new DynamicTokenMarker |
|
78 |
buffer.setTokenMarker(token_marker) |
|
79 |
||
80 |
// register for new declarations |
|
34470 | 81 |
prover.decl_info += (pair => token_marker += (pair._1, pair._2)) |
34456 | 82 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
83 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
84 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
85 |
def deactivate { |
34467 | 86 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
34460 | 87 |
theory_view.deactivate |
88 |
prover.stop |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
89 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
90 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
91 |
} |