External_Hyperlink: proper error dialog;
authorwenzelm
Sun, 29 Aug 2010 21:21:37 +0200
changeset 38853 f593754b0772
parent 38852 23513fb32e7b
child 38854 eb6a35be18ca
External_Hyperlink: proper error dialog;
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))
     }