equal
deleted
inserted
replaced
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 |