src/Tools/jEdit/src/jedit_editor.scala
changeset 60988 1d7a7e33fd67
parent 60933 6d03e05ef041
child 61011 018b0c996b54
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -225,7 +225,7 @@
       if (Path.is_wellformed(source_name)) {
         if (Path.is_valid(source_name)) {
           val path = Path.explode(source_name)
-          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
+          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
         }
         else None
       }