more convenient switching of buffers;
authorwenzelm
Fri, 24 Aug 2012 20:58:29 +0200
changeset 48925 9c9bbaa2fff1
parent 48924 27d8ccd1906c
child 48926 8d7778a19857
more convenient switching of buffers;
src/Tools/jEdit/src/hyperlink.scala
--- a/src/Tools/jEdit/src/hyperlink.scala	Fri Aug 24 20:47:33 2012 +0200
+++ b/src/Tools/jEdit/src/hyperlink.scala	Fri Aug 24 20:58:29 2012 +0200
@@ -33,7 +33,7 @@
 
     Isabelle.jedit_buffer(jedit_file) match {
       case Some(buffer) =>
-        view.setBuffer(buffer)
+        view.goToBuffer(buffer)
         val text_area = view.getTextArea
 
         try {