diff -r 982baed14542 -r 42311fd08899 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Oct 12 11:25:06 2017 +0200 +++ b/src/Pure/PIDE/document.scala Thu Oct 12 11:39:06 2017 +0200 @@ -117,7 +117,7 @@ case _ => false } - def path: Path = Path.explode(node) + def path: Path = Path.explode(File.standard_path(node)) def is_theory: Boolean = theory.nonEmpty