# HG changeset patch
# User wenzelm
# Date 1345834709 -7200
# Node ID 9c9bbaa2fff153bda9eb6aae7ab2466c9ac471dd
# Parent  27d8ccd1906c96837df5672518b58af4db494e41
more convenient switching of buffers;

diff -r 27d8ccd1906c -r 9c9bbaa2fff1 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 {