# HG changeset patch
# User wenzelm
# Date 1482504833 -3600
# Node ID 4c9fb4d4bca3cf3be23f204ea19cc1739b38481c
# Parent  5a2c15faf89ca27b476bfacf5072147ee7640dce
tuned;

diff -r 5a2c15faf89c -r 4c9fb4d4bca3 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Fri Dec 23 11:53:31 2016 +0100
+++ b/src/Pure/PIDE/editor.scala	Fri Dec 23 15:53:53 2016 +0100
@@ -24,7 +24,7 @@
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
 
   abstract class Hyperlink {
-    def external: Boolean
+    def external: Boolean = false
     def follow(context: Context): Unit
   }
   def hyperlink_command(
diff -r 5a2c15faf89c -r 4c9fb4d4bca3 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 11:53:31 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 15:53:53 2016 +0100
@@ -224,14 +224,14 @@
       case doc: Doc.Text_File if doc.name == name => doc.path
       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
         new Hyperlink {
-          val external = !path.is_file
+          override val external = !path.is_file
           def follow(view: View): Unit = goto_doc(view, path)
           override def toString: String = "doc " + quote(name)
         })
 
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
-      val external = true
+      override val external = true
       def follow(view: View): Unit =
         Standard_Thread.fork("hyperlink_url") {
           try { Isabelle_System.open(Url.escape(name)) }
@@ -247,7 +247,6 @@
 
   def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
     new Hyperlink {
-      val external = false
       def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
     }
@@ -257,7 +256,6 @@
 
   def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
     new Hyperlink {
-      val external = false
       def follow(view: View): Unit = goto_file(focus, view, pos)
       override def toString: String = "file " + quote(pos.name)
     }