src/Tools/jEdit/src/jedit/ProverSetup.scala
author immler@in.tum.de
Sun, 11 Jan 2009 13:15:05 +0100
changeset 34464 8a1ba195247a
parent 34462 fefbd0421e4e
child 34467 c7d7a92fe3d5
permissions -rw-r--r--
removed comment: theory-view registers when created
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
     1
/*
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34407
diff changeset
     2
 * Independent prover sessions
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
     3
 *
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34407
diff changeset
     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
wenzelm
parents: 34422
diff changeset
    10
import isabelle.prover.{Prover, Command}
34438
2faedc70b52d proper import isabelle.renderer.UserAgent;
wenzelm
parents: 34431
diff changeset
    11
import isabelle.renderer.UserAgent
2faedc70b52d proper import isabelle.renderer.UserAgent;
wenzelm
parents: 34431
diff changeset
    12
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    13
34431
wenzelm
parents: 34422
diff changeset
    14
import org.w3c.dom.Document
wenzelm
parents: 34422
diff changeset
    15
wenzelm
parents: 34422
diff changeset
    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
wenzelm
parents: 34422
diff changeset
    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
wenzelm
parents: 34422
diff changeset
    22
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    23
class ProverSetup(buffer: JEditBuffer)
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    24
{
34443
f2e13329cc49 dynamic instances Isabelle.system, Isabelle.symbols;
wenzelm
parents: 34441
diff changeset
    25
  val prover = new Prover(Isabelle.system, Isabelle.symbols)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    26
  var theory_view: TheoryView = null
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    27
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    28
  val state_update = new EventBus[Command]
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    29
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    30
  private var _selected_state: Command = null
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    31
  def selected_state = _selected_state
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    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
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    34
  val output_text_view = new JTextArea
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    35
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    36
  def activate(view: View) {
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
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
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    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
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    42
    prover.set_document(theory_view,
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    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
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    45
    prover.output_info += (text =>
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    46
      {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    47
        output_text_view.append(text)
34422
d5a41da986c3 more conventional action names;
wenzelm
parents: 34408
diff changeset
    48
        val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    49
        //link process output if dockable is active
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    50
        if(dockable != null) {
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    51
          val output_dockable = dockable.asInstanceOf[OutputDockable]
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    52
          if(output_dockable.getComponent(0) != output_text_view ) {
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    53
            output_dockable.asInstanceOf[OutputDockable].removeAll
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    54
            output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    55
            output_dockable.revalidate
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    56
          }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    57
        }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    58
      })
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    59
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    60
    //register for state-view
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    61
    state_update += (state => {
34422
d5a41da986c3 more conventional action names;
wenzelm
parents: 34408
diff changeset
    62
      val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    63
      val state_panel =
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    64
        if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    65
        else null
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    66
      if (state_panel != null){
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    67
        if (state == null)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    68
          state_panel.setDocument(null: Document)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    69
        else
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    70
          state_panel.setDocument(state.results_xml, UserAgent.baseURL)
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    71
      }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    72
    })
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    73
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
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    76
  def deactivate {
34460
cc5b9f02fbea ability to deactivate buffers
immler@in.tum.de
parents: 34406
diff changeset
    77
    theory_view.deactivate
cc5b9f02fbea ability to deactivate buffers
immler@in.tum.de
parents: 34406
diff changeset
    78
    prover.stop
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    79
  }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    80
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    81
}