author | wenzelm |
Thu, 12 Oct 2017 11:39:06 +0200 | |
changeset 66849 | 42311fd08899 |
parent 66848 | 982baed14542 |
child 66850 | a91b6d80c911 |
--- 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