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 }