diff -r 3f6280aedbcc -r 123bd97fcea1 src/Tools/jEdit/src/hyperlink.scala
--- a/src/Tools/jEdit/src/hyperlink.scala	Tue Mar 26 11:26:13 2013 +0100
+++ b/src/Tools/jEdit/src/hyperlink.scala	Tue Mar 26 12:40:51 2013 +0100
@@ -16,7 +16,7 @@
 
 object Hyperlink
 {
-  def apply(jedit_file: String, line: Int, column: Int): Hyperlink =
+  def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
     File_Link(jedit_file, line, column)
 }