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 |
22 |
24 class ProverSetup(buffer : JEditBuffer) { |
23 class ProverSetup(buffer: JEditBuffer) |
|
24 { |
|
25 val prover = new Prover(Isabelle.system, Isabelle.symbols) |
|
26 var theory_view: TheoryView = null |
25 |
27 |
26 val prover = new Prover(Isabelle.system, Isabelle.symbols) |
28 val state_update = new EventBus[Command] |
27 var theory_view : TheoryView = null |
|
28 |
|
29 private var _selectedState : Command = null |
|
30 |
29 |
31 val stateUpdate = new EventSource[Command] |
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) } |
32 |
33 |
33 def selectedState = _selectedState |
34 val output_text_view = new JTextArea |
34 def selectedState_=(newState : Command) { |
|
35 _selectedState = newState |
|
36 stateUpdate fire newState |
|
37 } |
|
38 |
35 |
39 val output_text_view = new JTextArea("== Isabelle output ==\n") |
36 def activate(view: View) { |
40 |
37 prover.start(Isabelle.property("logic")) |
41 def activate(view : View) { |
|
42 val logic = Isabelle.property("logic") |
|
43 prover.start(if (logic == null) logic else "HOL") // FIXME avoid hardwired logic |
|
44 val buffer = view.getBuffer |
38 val buffer = view.getBuffer |
45 val dir = buffer.getDirectory() |
39 val dir = buffer.getDirectory |
46 |
40 |
47 theory_view = new TheoryView(view.getTextArea) |
41 theory_view = new TheoryView(view.getTextArea) |
48 prover.setDocument(theory_view , |
42 prover.set_document(theory_view, |
49 if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir) |
43 if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir) |
50 theory_view.activate |
44 theory_view.activate |
51 prover.outputInfo.add( text => { |
45 prover.output_info += (text => |
|
46 { |
52 output_text_view.append(text) |
47 output_text_view.append(text) |
53 val dockable = view.getDockableWindowManager.getDockable("isabelle-output") |
48 val dockable = view.getDockableWindowManager.getDockable("isabelle-output") |
54 //link process output if dockable is active |
49 //link process output if dockable is active |
55 if(dockable != null) { |
50 if(dockable != null) { |
56 val output_dockable = dockable.asInstanceOf[OutputDockable] |
51 val output_dockable = dockable.asInstanceOf[OutputDockable] |
59 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view)) |
54 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view)) |
60 output_dockable.revalidate |
55 output_dockable.revalidate |
61 } |
56 } |
62 } |
57 } |
63 }) |
58 }) |
64 |
59 |
65 //register for state-view |
60 //register for state-view |
66 stateUpdate.add(state => { |
61 state_update += (state => { |
67 val state_view = view.getDockableWindowManager.getDockable("isabelle-state") |
62 val state_view = view.getDockableWindowManager.getDockable("isabelle-state") |
68 val state_panel = if(state_view != null) state_view.asInstanceOf[StateViewDockable].panel else null |
63 val state_panel = |
69 if(state_panel != null){ |
64 if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel |
|
65 else null |
|
66 if (state_panel != null){ |
70 if (state == null) |
67 if (state == null) |
71 state_panel.setDocument(null : Document) |
68 state_panel.setDocument(null: Document) |
72 else |
69 else |
73 state_panel.setDocument(state.results_xml, UserAgent.baseURL) |
70 state_panel.setDocument(state.results_xml, UserAgent.baseURL) |
74 } |
71 } |
75 }) |
72 }) |
76 |
73 |
77 //register for theory-view |
74 //register for theory-view |
78 |
75 |
79 // could also use this: |
76 // could also use this: |
80 // prover.commandInfo.add(c => Isabelle.theory_view.repaint(c.command)) |
77 // prover.commandInfo.add(c => Isabelle.theory_view.repaint(c.command)) |
81 |
78 |