src/Tools/jEdit/src/timing_dockable.scala
changeset 66082 2d12a730a380
parent 65897 94b0da1b242e
child 66191 d91108ba9474
equal deleted inserted replaced
66081:441f95b05944 66082:2d12a730a380
    86   private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
    86   private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
    87     extends Entry
    87     extends Entry
    88   {
    88   {
    89     def print: String =
    89     def print: String =
    90       Time.print_seconds(timing) + "s theory " + quote(name.theory)
    90       Time.print_seconds(timing) + "s theory " + quote(name.theory)
    91     def follow(snapshot: Document.Snapshot) { JEdit_Editor.goto_file(true, view, name.node) }
    91     def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
    92   }
    92   }
    93 
    93 
    94   private case class Command_Entry(command: Command, timing: Double) extends Entry
    94   private case class Command_Entry(command: Command, timing: Double) extends Entry
    95   {
    95   {
    96     def print: String =
    96     def print: String =
    97       "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
    97       "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
    98     def follow(snapshot: Document.Snapshot)
    98     def follow(snapshot: Document.Snapshot)
    99     { JEdit_Editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
    99     { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
   100   }
   100   }
   101 
   101 
   102 
   102 
   103   /* timing view */
   103   /* timing view */
   104 
   104