mixed theory/command entries;
authorwenzelm
Tue Mar 26 12:40:51 2013 +0100 (2013-03-26)
changeset 51534123bd97fcea1
parent 51533 3f6280aedbcc
child 51535 f2f480bc4223
mixed theory/command entries;
tuned;
src/Tools/jEdit/src/hyperlink.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/hyperlink.scala	Tue Mar 26 11:26:13 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/hyperlink.scala	Tue Mar 26 12:40:51 2013 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  object Hyperlink
     1.6  {
     1.7 -  def apply(jedit_file: String, line: Int, column: Int): Hyperlink =
     1.8 +  def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
     1.9      File_Link(jedit_file, line, column)
    1.10  }
    1.11  
     2.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Mar 26 11:26:13 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Mar 26 12:40:51 2013 +0100
     2.3 @@ -30,7 +30,7 @@
     2.4      reactions += {
     2.5        case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
     2.6          val index = peer.locationToIndex(point)
     2.7 -        if (index >= 0) jEdit.openFile(view, listData(index).node)
     2.8 +        if (index >= 0) Hyperlink(listData(index).node).follow(view)
     2.9      }
    2.10    }
    2.11    status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
     3.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 26 11:26:13 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 26 12:40:51 2013 +0100
     3.3 @@ -46,14 +46,29 @@
     3.4          entry: Entry, index: Int): Component =
     3.5        {
     3.6          val component = Renderer_Component
     3.7 -        component.text = Time.print_seconds(entry.timing) + "s " + entry.command.name
     3.8 +        component.text = entry.print
     3.9          component
    3.10        }
    3.11      }
    3.12    }
    3.13  
    3.14 -  private case class Entry(command: Command, timing: Double)
    3.15 +  private abstract class Entry
    3.16 +  {
    3.17 +    def timing: Double
    3.18 +    def print: String
    3.19 +    def follow(snapshot: Document.Snapshot)
    3.20 +  }
    3.21 +
    3.22 +  private case class Theory_Entry(name: Document.Node.Name, timing: Double) extends Entry
    3.23    {
    3.24 +    def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
    3.25 +    def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view)
    3.26 +  }
    3.27 +
    3.28 +  private case class Command_Entry(command: Command, timing: Double) extends Entry
    3.29 +  {
    3.30 +    def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
    3.31 +
    3.32      def follow(snapshot: Document.Snapshot)
    3.33      {
    3.34        val node = snapshot.version.nodes(command.node_name)
    3.35 @@ -88,7 +103,7 @@
    3.36  
    3.37    private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
    3.38  
    3.39 -  private val threshold_label = new Label("Timing threshold: ")
    3.40 +  private val threshold_label = new Label("Threshold: ")
    3.41  
    3.42    private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
    3.43      reactions += {
    3.44 @@ -110,8 +125,29 @@
    3.45    /* component state -- owned by Swing thread */
    3.46  
    3.47    private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
    3.48 -  private var current_name = Document.Node.Name.empty
    3.49 -  private var current_timing = Protocol.empty_node_timing
    3.50 +
    3.51 +  private def make_entries(): List[Entry] =
    3.52 +  {
    3.53 +    Swing_Thread.require()
    3.54 +
    3.55 +    val name =
    3.56 +      Document_View(view.getTextArea) match {
    3.57 +        case None => Document.Node.Name.empty
    3.58 +        case Some(doc_view) => doc_view.model.name
    3.59 +      }
    3.60 +    val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
    3.61 +
    3.62 +    val theories =
    3.63 +      (for {
    3.64 +        (node_name, node_timing) <- nodes_timing.toList
    3.65 +        if node_timing.total > timing_threshold
    3.66 +      } yield Theory_Entry(node_name, node_timing.total)).sorted(Entry.Ordering)
    3.67 +    val commands =
    3.68 +      (for ((command, command_timing) <- timing.commands.toList)
    3.69 +        yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
    3.70 +
    3.71 +    theories.flatMap(entry => entry :: (if (entry.name == name) commands else Nil))
    3.72 +  }
    3.73  
    3.74    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
    3.75    {
    3.76 @@ -134,18 +170,8 @@
    3.77          })
    3.78        nodes_timing = nodes_timing1
    3.79  
    3.80 -      Document_View(view.getTextArea) match {
    3.81 -        case Some(doc_view) =>
    3.82 -          val name = doc_view.model.name
    3.83 -          val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing
    3.84 -          if (current_name != name || current_timing != timing) {
    3.85 -            current_name = name
    3.86 -            current_timing = timing
    3.87 -            timing_view.listData =
    3.88 -              timing.commands.toList.map(p => Entry(p._1, p._2)).sorted(Entry.Ordering)
    3.89 -          }
    3.90 -        case None =>
    3.91 -      }
    3.92 +      val entries = make_entries()
    3.93 +      if (timing_view.listData.toList != entries) timing_view.listData = entries
    3.94      }
    3.95    }
    3.96