equal
deleted
inserted
replaced
45 |
45 |
46 def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
46 def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
47 { |
47 { |
48 val path = Path.explode(name.node) |
48 val path = Path.explode(name.node) |
49 if (!path.is_file) error("No such file: " + path.toString) |
49 if (!path.is_file) error("No such file: " + path.toString) |
50 f(File.read(path)) |
50 |
|
51 val text = File.read(path) |
|
52 Symbol.decode_strict(text) |
|
53 f(text) |
51 } |
54 } |
52 |
55 |
53 |
56 |
54 /* theory files */ |
57 /* theory files */ |
55 |
58 |