changeset 50291 | 674893679352 |
parent 50204 | daeb1674fb91 |
child 50414 | e17a1f179bb0 |
--- a/src/Pure/Thy/thy_load.scala Thu Nov 29 23:12:50 2012 +0100 +++ b/src/Pure/Thy/thy_load.scala Fri Nov 30 10:42:54 2012 +0100 @@ -47,7 +47,10 @@ { val path = Path.explode(name.node) if (!path.is_file) error("No such file: " + path.toString) - f(File.read(path)) + + val text = File.read(path) + Symbol.decode_strict(text) + f(text) }