| changeset 66849 | 42311fd08899 |
| parent 66773 | 0cd29455a5e8 |
| child 67014 | e6a695d6a6b2 |
--- 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