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;
     1 /*
     2  * Dockable window for navigating through the document history
     3  *
     4  * @author Fabian Immler, TU Munich
     5  */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle.proofdocument.Change
    11 
    12 import java.awt.Dimension
    13 import scala.swing.{ListView, FlowPanel}
    14 import scala.swing.event.ListSelectionChanged
    15 
    16 import org.gjt.sp.jedit.View
    17 import org.gjt.sp.jedit.gui.DockableWindowManager
    18 
    19 
    20 class History_Dockable(view: View, position: String) extends FlowPanel
    21 {
    22   if (position == DockableWindowManager.FLOATING)
    23     preferredSize = new Dimension(500, 250)
    24 
    25   def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
    26   def get_versions() =
    27     prover_setup() match {
    28       case None => Nil
    29       case Some(setup) => setup.theory_view.changes
    30     }
    31 
    32   val list = new ListView[Change]
    33   list.fixedCellWidth = 500
    34   list.listData = get_versions()
    35   contents += list
    36 
    37   listenTo(list.selection)
    38   reactions += {
    39     case ListSelectionChanged(source, range, false) =>
    40       prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
    41   }
    42 
    43   prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
    44 }