need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
1.1 --- a/src/Pure/Thy/thy_load.scala Tue Aug 07 17:08:22 2012 +0200
1.2 +++ b/src/Pure/Thy/thy_load.scala Tue Aug 07 17:46:30 2012 +0200
1.3 @@ -39,7 +39,7 @@
1.4 /* file-system operations */
1.5
1.6 def append(dir: String, source_path: Path): String =
1.7 - (Path.explode(dir) + source_path).implode
1.8 + (Path.explode(dir) + source_path).expand.implode
1.9
1.10 def read_header(name: Document.Node.Name): Thy_Header =
1.11 {