src/Tools/jEdit/src/jedit/history_dockable.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -0,0 +1,44 @@
     1.4 +/*
     1.5 + * Dockable window for navigating through the document history
     1.6 + *
     1.7 + * @author Fabian Immler, TU Munich
     1.8 + */
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle.proofdocument.Change
    1.14 +
    1.15 +import java.awt.Dimension
    1.16 +import scala.swing.{ListView, FlowPanel}
    1.17 +import scala.swing.event.ListSelectionChanged
    1.18 +
    1.19 +import org.gjt.sp.jedit.View
    1.20 +import org.gjt.sp.jedit.gui.DockableWindowManager
    1.21 +
    1.22 +
    1.23 +class History_Dockable(view: View, position: String) extends FlowPanel
    1.24 +{
    1.25 +  if (position == DockableWindowManager.FLOATING)
    1.26 +    preferredSize = new Dimension(500, 250)
    1.27 +
    1.28 +  def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
    1.29 +  def get_versions() =
    1.30 +    prover_setup() match {
    1.31 +      case None => Nil
    1.32 +      case Some(setup) => setup.theory_view.changes
    1.33 +    }
    1.34 +
    1.35 +  val list = new ListView[Change]
    1.36 +  list.fixedCellWidth = 500
    1.37 +  list.listData = get_versions()
    1.38 +  contents += list
    1.39 +
    1.40 +  listenTo(list.selection)
    1.41 +  reactions += {
    1.42 +    case ListSelectionChanged(source, range, false) =>
    1.43 +      prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
    1.44 +  }
    1.45 +
    1.46 +  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
    1.47 +}