author | wenzelm |
Tue, 27 Jan 2009 19:41:44 +0100 | |
changeset 34504 | 4bd676662792 |
parent 34503 | 7d0726f19d04 |
child 34517 | 163cda249619 |
child 34533 | 35308320713a |
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 |
{ |
|
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
25 |
var prover: Prover = null |
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) { |
|
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
37 |
prover = new Prover(Isabelle.system, Isabelle.default_logic) |
34498 | 38 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
39 |
val buffer = view.getBuffer |
34456 | 40 |
val dir = buffer.getDirectory |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
41 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
42 |
theory_view = new TheoryView(view.getTextArea) |
34456 | 43 |
prover.set_document(theory_view, |
44 |
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
|
45 |
theory_view.activate |
34467 | 46 |
|
47 |
//register output-view |
|
34456 | 48 |
prover.output_info += (text => |
49 |
{ |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
50 |
output_text_view.append(text) |
34422 | 51 |
val dockable = view.getDockableWindowManager.getDockable("isabelle-output") |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
52 |
//link process output if dockable is active |
34503 | 53 |
if (dockable != null) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
54 |
val output_dockable = dockable.asInstanceOf[OutputDockable] |
34503 | 55 |
if (output_dockable.getComponent(0) != output_text_view ) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
56 |
output_dockable.asInstanceOf[OutputDockable].removeAll |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
57 |
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view)) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
58 |
output_dockable.revalidate |
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 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
61 |
}) |
34456 | 62 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
63 |
//register for state-view |
34456 | 64 |
state_update += (state => { |
34422 | 65 |
val state_view = view.getDockableWindowManager.getDockable("isabelle-state") |
34456 | 66 |
val state_panel = |
67 |
if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel |
|
68 |
else null |
|
34503 | 69 |
if (state_panel != null) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
70 |
if (state == null) |
34456 | 71 |
state_panel.setDocument(null: Document) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
72 |
else |
34486 | 73 |
state_panel.setDocument(state.result_document, UserAgent.baseURL) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
74 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
75 |
}) |
34467 | 76 |
|
77 |
// one independent token marker per prover |
|
78 |
val token_marker = new DynamicTokenMarker |
|
79 |
buffer.setTokenMarker(token_marker) |
|
80 |
||
81 |
// register for new declarations |
|
34470 | 82 |
prover.decl_info += (pair => token_marker += (pair._1, pair._2)) |
34456 | 83 |
|
34406
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 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
86 |
def deactivate { |
34467 | 87 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
34460 | 88 |
theory_view.deactivate |
89 |
prover.stop |
|
34406
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 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
92 |
} |