author | immler@in.tum.de |
Thu, 19 Mar 2009 16:48:29 +0100 | |
changeset 34539 | 5d88e0681d44 |
parent 34538 | 20bfcca24658 |
parent 34534 | b06946a1d4cb |
child 34566 | 28fa2f219f01 |
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 |
||
34431 | 13 |
import org.w3c.dom.Document |
14 |
||
15 |
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
|
16 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
34431 | 17 |
import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
18 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
19 |
import javax.swing.{JTextArea, JScrollPane} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
20 |
|
34431 | 21 |
|
34456 | 22 |
class ProverSetup(buffer: JEditBuffer) |
23 |
{ |
|
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
24 |
var prover: Prover = null |
34456 | 25 |
var theory_view: TheoryView = null |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
26 |
|
34456 | 27 |
val state_update = new EventBus[Command] |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
28 |
|
34456 | 29 |
private var _selected_state: Command = null |
30 |
def selected_state = _selected_state |
|
31 |
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
|
32 |
|
34456 | 33 |
val output_text_view = new JTextArea |
34 |
||
35 |
def activate(view: View) { |
|
34504
4bd676662792
eliminated Prover.start -- part of main constructor;
wenzelm
parents:
34503
diff
changeset
|
36 |
prover = new Prover(Isabelle.system, Isabelle.default_logic) |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
37 |
prover.start() //start actor |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
38 |
val buffer = view.getBuffer |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34504
diff
changeset
|
39 |
val path = buffer.getPath |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
40 |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
41 |
theory_view = new TheoryView(view.getTextArea, prover) |
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
42 |
prover.set_document(theory_view.change_receiver, |
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34504
diff
changeset
|
43 |
if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) |
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 |
{ |
|
34533
35308320713a
preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents:
34504
diff
changeset
|
49 |
output_text_view.append(text + "\n") |
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 |
34503 | 52 |
if (dockable != null) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
53 |
val output_dockable = dockable.asInstanceOf[OutputDockable] |
34503 | 54 |
if (output_dockable.getComponent(0) != output_text_view ) { |
34406
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 |
|
34503 | 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 |
}) |
34456 | 75 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
76 |
} |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
77 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
78 |
def deactivate { |
34467 | 79 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
34460 | 80 |
theory_view.deactivate |
81 |
prover.stop |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff
changeset
|
82 |
} |
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 |
} |