src/Pure/PIDE/editor.scala
changeset 64663 4c9fb4d4bca3
parent 64524 e6a3c55b929b
child 64664 951507563033
--- 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(