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