src/Tools/jEdit/src/timing_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 57612 990ffb84489b
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     1 /*  Title:      Tools/jEdit/src/timing_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for timing information.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
    13 import scala.swing.event.{MouseClicked, ValueChanged}
    14 
    15 import java.awt.{BorderLayout, Graphics2D, Insets, Color}
    16 import javax.swing.{JList, BorderFactory}
    17 import javax.swing.border.{BevelBorder, SoftBevelBorder}
    18 
    19 import org.gjt.sp.jedit.{View, jEdit}
    20 
    21 
    22 class Timing_Dockable(view: View, position: String) extends Dockable(view, position)
    23 {
    24   /* entry */
    25 
    26   private object Entry
    27   {
    28     object Ordering extends scala.math.Ordering[Entry]
    29     {
    30       def compare(entry1: Entry, entry2: Entry): Int =
    31         entry2.timing compare entry1.timing
    32     }
    33 
    34     object Renderer_Component extends Label
    35     {
    36       opaque = false
    37       xAlignment = Alignment.Leading
    38       border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    39 
    40       var entry: Entry = null
    41       override def paintComponent(gfx: Graphics2D)
    42       {
    43         def paint_rectangle(color: Color)
    44         {
    45           val size = peer.getSize()
    46           val insets = border.getBorderInsets(peer)
    47           val x = insets.left
    48           val y = insets.top
    49           val w = size.width - x - insets.right
    50           val h = size.height - y - insets.bottom
    51           gfx.setColor(color)
    52           gfx.fillRect(x, y, w, h)
    53         }
    54 
    55         entry match {
    56           case theory_entry: Theory_Entry if theory_entry.current =>
    57             paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
    58           case _: Command_Entry =>
    59             paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
    60           case _ =>
    61         }
    62         super.paintComponent(gfx)
    63       }
    64     }
    65 
    66     class Renderer extends ListView.Renderer[Entry]
    67     {
    68       def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
    69         entry: Entry, index: Int): Component =
    70       {
    71         val component = Renderer_Component
    72         component.entry = entry
    73         component.text = entry.print
    74         component
    75       }
    76     }
    77   }
    78 
    79   private abstract class Entry
    80   {
    81     def timing: Double
    82     def print: String
    83     def follow(snapshot: Document.Snapshot)
    84   }
    85 
    86   private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
    87     extends Entry
    88   {
    89     def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
    90     def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
    91   }
    92 
    93   private case class Command_Entry(command: Command, timing: Double) extends Entry
    94   {
    95     def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
    96     def follow(snapshot: Document.Snapshot)
    97     { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
    98   }
    99 
   100 
   101   /* timing view */
   102 
   103   private val timing_view = new ListView(Nil: List[Entry]) {
   104     listenTo(mouse.clicks)
   105     reactions += {
   106       case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
   107         val index = peer.locationToIndex(point)
   108         if (index >= 0) listData(index).follow(PIDE.session.snapshot())
   109     }
   110   }
   111   timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   112   timing_view.peer.setVisibleRowCount(0)
   113   timing_view.selection.intervalMode = ListView.IntervalMode.Single
   114   timing_view.renderer = new Entry.Renderer
   115 
   116   set_content(new ScrollPane(timing_view))
   117 
   118 
   119   /* timing threshold */
   120 
   121   private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
   122 
   123   private val threshold_tooltip = "Threshold for timing display (seconds)"
   124 
   125   private val threshold_label = new Label("Threshold: ") {
   126     tooltip = threshold_tooltip
   127   }
   128 
   129   private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
   130     reactions += {
   131       case _: ValueChanged =>
   132         text match {
   133           case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
   134           case _ =>
   135         }
   136         handle_update()
   137     }
   138     tooltip = threshold_tooltip
   139     verifier = ((s: String) =>
   140       s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
   141   }
   142 
   143   private val controls =
   144     new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value)
   145   add(controls.peer, BorderLayout.NORTH)
   146 
   147 
   148   /* component state -- owned by Swing thread */
   149 
   150   private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
   151 
   152   private def make_entries(): List[Entry] =
   153   {
   154     Swing_Thread.require {}
   155 
   156     val name =
   157       Document_View(view.getTextArea) match {
   158         case None => Document.Node.Name.empty
   159         case Some(doc_view) => doc_view.model.node_name
   160       }
   161     val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
   162 
   163     val theories =
   164       (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty)
   165         yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
   166     val commands =
   167       (for ((command, command_timing) <- timing.commands.toList)
   168         yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
   169 
   170     theories.flatMap(entry =>
   171       if (entry.name == name) entry.copy(current = true) :: commands
   172       else List(entry))
   173   }
   174 
   175   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   176   {
   177     Swing_Thread.require {}
   178 
   179     val snapshot = PIDE.session.snapshot()
   180 
   181     val iterator =
   182       restriction match {
   183         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
   184         case None => snapshot.version.nodes.iterator
   185       }
   186     val nodes_timing1 =
   187       (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
   188           if (PIDE.resources.loaded_theories(name.theory)) timing1
   189           else {
   190             val node_timing =
   191               Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
   192             timing1 + (name -> node_timing)
   193           }
   194       })
   195     nodes_timing = nodes_timing1
   196 
   197     val entries = make_entries()
   198     if (timing_view.listData.toList != entries) timing_view.listData = entries
   199   }
   200 
   201 
   202   /* main */
   203 
   204   private val main =
   205     Session.Consumer[Session.Commands_Changed](getClass.getName) {
   206       case changed =>
   207         Swing_Thread.later { handle_update(Some(changed.nodes)) }
   208     }
   209 
   210   override def init()
   211   {
   212     PIDE.session.commands_changed += main
   213     handle_update()
   214   }
   215 
   216   override def exit()
   217   {
   218     PIDE.session.commands_changed -= main
   219   }
   220 }