1 /* |
1 /* |
2 * BufferExtension.scala |
2 * Independent prover sessions |
3 * |
3 * |
4 * To change this template, choose Tools | Template Manager |
4 * @author Fabian Immler, TU Munich |
5 * and open the template in the editor. |
|
6 */ |
5 */ |
7 |
6 |
8 package isabelle.jedit |
7 package isabelle.jedit |
9 |
8 |
10 import isabelle.utils.EventSource |
|
11 |
9 |
12 import isabelle.prover.{ Prover, Command } |
10 import isabelle.prover.{Prover, Command} |
|
11 import isabelle.renderer.UserAgent |
|
12 |
|
13 |
13 import org.w3c.dom.Document |
14 import org.w3c.dom.Document |
14 |
15 |
15 import isabelle.IsabelleSystem |
16 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, View} |
16 |
|
17 import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View } |
|
18 import org.gjt.sp.jedit.buffer.JEditBuffer |
17 import org.gjt.sp.jedit.buffer.JEditBuffer |
19 import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged } |
18 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged} |
20 |
19 |
21 import javax.swing.{JTextArea, JScrollPane} |
20 import javax.swing.{JTextArea, JScrollPane} |
22 |
21 |
23 class ProverSetup(buffer : JEditBuffer) { |
|
24 |
22 |
25 val prover = new Prover() |
23 class ProverSetup(buffer: JEditBuffer) |
26 var theory_view : TheoryView = null |
24 { |
27 |
25 val prover = new Prover(Isabelle.system, Isabelle.symbols) |
28 private var _selectedState : Command = null |
26 var theory_view: TheoryView = null |
29 |
27 |
30 val stateUpdate = new EventSource[Command] |
28 val state_update = new EventBus[Command] |
31 |
29 |
32 def selectedState = _selectedState |
30 private var _selected_state: Command = null |
33 def selectedState_=(newState : Command) { |
31 def selected_state = _selected_state |
34 _selectedState = newState |
32 def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) } |
35 stateUpdate fire newState |
|
36 } |
|
37 |
33 |
38 val output_text_view = new JTextArea("== Isabelle output ==\n") |
34 val output_text_view = new JTextArea |
39 |
35 |
40 def activate(view : View) { |
36 def activate(view: View) { |
41 val logic = Plugin.property("logic") |
37 prover.start(Isabelle.property("logic")) |
42 prover.start(if (logic == null) logic else "HOL") |
|
43 val buffer = view.getBuffer |
38 val buffer = view.getBuffer |
44 val dir = buffer.getDirectory() |
39 val dir = buffer.getDirectory |
45 |
40 |
46 theory_view = new TheoryView(view.getTextArea) |
41 theory_view = new TheoryView(view.getTextArea) |
47 prover.setDocument(theory_view , |
42 prover.set_document(theory_view, |
48 if (dir.startsWith(Plugin.VFS_PREFIX)) dir.substring(Plugin.VFS_PREFIX.length) else dir) |
43 if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir) |
49 theory_view.activate |
44 theory_view.activate |
50 prover.outputInfo.add( text => { |
45 prover.output_info += (text => |
|
46 { |
51 output_text_view.append(text) |
47 output_text_view.append(text) |
52 val dockable = view.getDockableWindowManager.getDockable("Isabelle_output") |
48 val dockable = view.getDockableWindowManager.getDockable("isabelle-output") |
53 //link process output if dockable is active |
49 //link process output if dockable is active |
54 if(dockable != null) { |
50 if(dockable != null) { |
55 val output_dockable = dockable.asInstanceOf[OutputDockable] |
51 val output_dockable = dockable.asInstanceOf[OutputDockable] |
56 if(output_dockable.getComponent(0) != output_text_view ) { |
52 if(output_dockable.getComponent(0) != output_text_view ) { |
57 output_dockable.asInstanceOf[OutputDockable].removeAll |
53 output_dockable.asInstanceOf[OutputDockable].removeAll |
58 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view)) |
54 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view)) |
59 output_dockable.revalidate |
55 output_dockable.revalidate |
60 } |
56 } |
61 } |
57 } |
62 }) |
58 }) |
63 |
59 |
64 //register for state-view |
60 //register for state-view |
65 stateUpdate.add(state => { |
61 state_update += (state => { |
66 val state_view = view.getDockableWindowManager.getDockable("Isabelle_state") |
62 val state_view = view.getDockableWindowManager.getDockable("isabelle-state") |
67 val state_panel = if(state_view != null) state_view.asInstanceOf[StateViewDockable].panel else null |
63 val state_panel = |
68 if(state_panel != null){ |
64 if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel |
|
65 else null |
|
66 if (state_panel != null){ |
69 if (state == null) |
67 if (state == null) |
70 state_panel.setDocument(null : Document) |
68 state_panel.setDocument(null: Document) |
71 else |
69 else |
72 state_panel.setDocument(state.results_xml, UserAgent.baseURL) |
70 state_panel.setDocument(state.results_xml, UserAgent.baseURL) |
73 } |
71 } |
74 }) |
72 }) |
75 |
73 |
76 //register for theory-view |
74 //register for theory-view |
77 |
75 |
78 // could also use this: |
76 // could also use this: |
79 // prover.commandInfo.add(c => Plugin.theory_view.repaint(c.command)) |
77 // prover.commandInfo.add(c => Isabelle.theory_view.repaint(c.command)) |
80 |
78 |
81 } |
79 } |
82 |
80 |
83 def deactivate { |
81 def deactivate { |
84 theory_view.deactivate |
82 theory_view.deactivate |