# HG changeset patch
# User wenzelm
# Date 1283109697 -7200
# Node ID f593754b07722a856c575449487330381d792fe7
# Parent  23513fb32e7bc75345bf8437f10b0667198951cf
External_Hyperlink: proper error dialog;

diff -r 23513fb32e7b -r f593754b0772 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 29 21:02:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 29 21:21:37 2010 +0200
@@ -29,7 +29,8 @@
 {
   override def click(view: View) = {
     Isabelle.system.source_file(ref_file) match {
-      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
+      case None =>
+        Library.error_dialog(view, "File not found", "Could not find source file " + ref_file)
       case Some(file) =>
         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
     }