src/Tools/jEdit/src/jedit/ProverSetup.scala
author wenzelm
Fri, 26 Jun 2009 21:46:34 +0200
changeset 34629 fdc1087a970f
parent 34624 5e4f33d033ba
child 34632 f044d8446ae9
permissions -rw-r--r--
prover.set_document: plain name, no path for now;
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
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)
34629
fdc1087a970f prover.set_document: plain name, no path for now;
wenzelm
parents: 34624
diff changeset
    42
    prover.set_document(theory_view.change_receiver, buffer.getName)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    43
    theory_view.activate
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    44
    val MAX = TheoryView.MAX_CHANGE_LENGTH
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    45
    for (i <- 0 to buffer.getLength / MAX) {
34597
a0c84b0edb9a merged; resolved superficial conflicts
immler@in.tum.de
parents: 34582 34591
diff changeset
    46
      prover ! new isabelle.proofdocument.Text.Change(
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    47
        Isabelle.system.id(), i * MAX,
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    48
        buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), 0)
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    49
    }
34467
c7d7a92fe3d5 created DynamicTokenMarker
immler@in.tum.de
parents: 34464
diff changeset
    50
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    51
    // register output-view
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    52
    prover.output_info += (text =>
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    53
      {
34533
35308320713a preliminary/failed attempt to use the new IsarDocument access model to the prover;
wenzelm
parents: 34504
diff changeset
    54
        output_text_view.append(text + "\n")
34422
d5a41da986c3 more conventional action names;
wenzelm
parents: 34408
diff changeset
    55
        val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    56
        // link process output if dockable is active
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34502
diff changeset
    57
        if (dockable != null) {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    58
          val output_dockable = dockable.asInstanceOf[OutputDockable]
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34502
diff changeset
    59
          if (output_dockable.getComponent(0) != output_text_view ) {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    60
            output_dockable.asInstanceOf[OutputDockable].removeAll
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    61
            output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    62
            output_dockable.revalidate
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    63
          }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    64
        }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    65
      })
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    66
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    67
    // register for state-view
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    68
    state_update += (state => {
34422
d5a41da986c3 more conventional action names;
wenzelm
parents: 34408
diff changeset
    69
      val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    70
      val state_panel =
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    71
        if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    72
        else null
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34502
diff changeset
    73
      if (state_panel != null) {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    74
        if (state == null)
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    75
          state_panel.setDocument(null: Document)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    76
        else
34486
7985efd78aa1 tuned handling of accumulated results;
wenzelm
parents: 34470
diff changeset
    77
          state_panel.setDocument(state.result_document, UserAgent.baseURL)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    78
      }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    79
    })
34456
14367c0715e8 replaced EventSource by EventBus;
wenzelm
parents: 34443
diff changeset
    80
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
34607
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    83
  def deactivate
bb30b5056db6 minor tuning;
wenzelm
parents: 34603
diff changeset
    84
  {
34467
c7d7a92fe3d5 created DynamicTokenMarker
immler@in.tum.de
parents: 34464
diff changeset
    85
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
34460
cc5b9f02fbea ability to deactivate buffers
immler@in.tum.de
parents: 34406
diff changeset
    86
    theory_view.deactivate
cc5b9f02fbea ability to deactivate buffers
immler@in.tum.de
parents: 34406
diff changeset
    87
    prover.stop
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    88
  }
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    89
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents:
diff changeset
    90
}