src/Tools/jEdit/src/jedit/history_dockable.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 src/Tools/jEdit/src/jedit/browse_version_dockable.scala@bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
immler@34652
     1
/*
wenzelm@34760
     2
 * Dockable window for navigating through the document history
immler@34652
     3
 *
immler@34652
     4
 * @author Fabian Immler, TU Munich
immler@34652
     5
 */
immler@34652
     6
immler@34652
     7
package isabelle.jedit
immler@34652
     8
wenzelm@34760
     9
immler@34660
    10
import isabelle.proofdocument.Change
immler@34652
    11
immler@34652
    12
import java.awt.Dimension
immler@34652
    13
import scala.swing.{ListView, FlowPanel}
immler@34652
    14
import scala.swing.event.ListSelectionChanged
immler@34652
    15
immler@34652
    16
import org.gjt.sp.jedit.View
immler@34652
    17
import org.gjt.sp.jedit.gui.DockableWindowManager
immler@34652
    18
immler@34652
    19
wenzelm@34760
    20
class History_Dockable(view: View, position: String) extends FlowPanel
immler@34686
    21
{
immler@34652
    22
  if (position == DockableWindowManager.FLOATING)
immler@34652
    23
    preferredSize = new Dimension(500, 250)
immler@34652
    24
wenzelm@34760
    25
  def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
wenzelm@34724
    26
  def get_versions() =
wenzelm@34724
    27
    prover_setup() match {
wenzelm@34724
    28
      case None => Nil
wenzelm@34724
    29
      case Some(setup) => setup.theory_view.changes
wenzelm@34724
    30
    }
wenzelm@34724
    31
immler@34660
    32
  val list = new ListView[Change]
immler@34652
    33
  list.fixedCellWidth = 500
immler@34686
    34
  list.listData = get_versions()
immler@34686
    35
  contents += list
immler@34652
    36
immler@34652
    37
  listenTo(list.selection)
immler@34652
    38
  reactions += {
immler@34652
    39
    case ListSelectionChanged(source, range, false) =>
wenzelm@34760
    40
      prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
wenzelm@34760
    41
  }
immler@34686
    42
wenzelm@34724
    43
  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
immler@34652
    44
}