equal
deleted
inserted
replaced
60 } |
60 } |
61 else this |
61 else this |
62 } |
62 } |
63 |
63 |
64 def goto(view: View): Unit = GUI_Thread.require { |
64 def goto(view: View): Unit = GUI_Thread.require { |
65 JEdit_Lib.jedit_buffer(name) match { |
65 PIDE.editor.goto_file(true, view, name, offset = offset) |
66 case Some(buffer) => PIDE.editor.goto_buffer(true, view, buffer, offset) |
|
67 case None => PIDE.editor.goto_file(true, view, name) |
|
68 } |
|
69 } |
66 } |
70 } |
67 } |
71 |
68 |
72 object History { |
69 object History { |
73 val limit: Int = 500 |
70 val limit: Int = 500 |