src/Tools/jEdit/src/jedit/ProverSetup.scala
author wenzelm
Tue, 16 Jun 2009 19:52:45 +0200
changeset 34607 bb30b5056db6
parent 34603 83a37e3b8c9c
child 34624 5e4f33d033ba
permissions -rw-r--r--
minor tuning;
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
/*
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
     2
 * Independent prover sessions for each buffer
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
34431
wenzelm
parents: 34422
diff changeset
    13
import org.w3c.dom.Document
wenzelm
parents: 34422
diff changeset
    14
wenzelm
parents: 34422
diff changeset
    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
wenzelm
parents: 34422
diff changeset
    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
wenzelm
parents: 34422
diff changeset
    21
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    22
class ProverSetup(buffer: JEditBuffer)
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    23
{
34504
4bd676662792 eliminated Prover.start -- part of main constructor;
wenzelm
parents: 34503
diff changeset
    24
  var prover: Prover = null
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    25
  var theory_view: TheoryView = null
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    26
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    27
  val state_update = new EventBus[Command]
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    28
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    29
  private var _selected_state: Command = null
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    30
  def selected_state = _selected_state
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    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
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    33
  val output_text_view = new JTextArea
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    34
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    35
  def activate(view: View)
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    36
  {
34504
4bd676662792 eliminated Prover.start -- part of main constructor;
wenzelm
parents: 34503
diff changeset
    37
    prover = new Prover(Isabelle.system, Isabelle.default_logic)
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    38
    prover.start() // start actor
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    39
    val buffer = view.getBuffer
34533
35308320713a preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents: 34504
diff changeset
    40
    val path = buffer.getPath
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    41
34538
20bfcca24658 Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents: 34532
diff changeset
    42
    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
    43
    prover.set_document(theory_view.change_receiver,
34582
5d5d253c7c29 superficial tuning;
wenzelm
parents: 34566
diff changeset
    44
      if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length)
5d5d253c7c29 superficial tuning;
wenzelm
parents: 34566
diff changeset
    45
      else path)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    46
    theory_view.activate
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    47
    val MAX = TheoryView.MAX_CHANGE_LENGTH
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    48
    for (i <- 0 to buffer.getLength / MAX) {
34597
a0c84b0edb9a merged; resolved superficial conflicts
immler@in.tum.de
parents: 34582 34591
diff changeset
    49
      prover ! new isabelle.proofdocument.Text.Change(
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    50
        Isabelle.system.id(), i * MAX,
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    51
        buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), 0)
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    52
    }
34467
c7d7a92fe3d5 created DynamicTokenMarker
immler@in.tum.de
parents: 34464
diff changeset
    53
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    54
    // register output-view
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    55
    prover.output_info += (text =>
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    56
      {
34533
35308320713a preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents: 34504
diff changeset
    57
        output_text_view.append(text + "\n")
34422
d5a41da986c3 more conventional action names;
wenzelm
parents: 34408
diff changeset
    58
        val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    59
        // link process output if dockable is active
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34502
diff changeset
    60
        if (dockable != null) {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    61
          val output_dockable = dockable.asInstanceOf[OutputDockable]
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34502
diff changeset
    62
          if (output_dockable.getComponent(0) != output_text_view ) {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    63
            output_dockable.asInstanceOf[OutputDockable].removeAll
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    64
            output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    65
            output_dockable.revalidate
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    66
          }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    67
        }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    68
      })
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    69
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    70
    // register for state-view
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    71
    state_update += (state => {
34422
d5a41da986c3 more conventional action names;
wenzelm
parents: 34408
diff changeset
    72
      val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    73
      val state_panel =
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    74
        if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    75
        else null
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34502
diff changeset
    76
      if (state_panel != null) {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    77
        if (state == null)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    78
          state_panel.setDocument(null: Document)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    79
        else
34486
7985efd78aa1 tuned handling of accumulated results;
wenzelm
parents: 34470
diff changeset
    80
          state_panel.setDocument(state.result_document, UserAgent.baseURL)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    81
      }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    82
    })
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    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
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    86
  def deactivate
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    87
  {
34467
c7d7a92fe3d5 created DynamicTokenMarker
immler@in.tum.de
parents: 34464
diff changeset
    88
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
34460
cc5b9f02fbea ability to deactivate buffers
immler@in.tum.de
parents: 34406
diff changeset
    89
    theory_view.deactivate
cc5b9f02fbea ability to deactivate buffers
immler@in.tum.de
parents: 34406
diff changeset
    90
    prover.stop
34406
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
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    93
}