equal
deleted
inserted
replaced
100 } |
100 } |
101 } |
101 } |
102 } |
102 } |
103 } |
103 } |
104 |
104 |
105 private def read_symbols(base: String) = { |
105 private def read_symbols(path: String) = { |
106 val file = new File(base + File.separator + "etc" + File.separator + "symbols") |
106 val file = new File(IsabelleSystem.platform_path(path)) |
107 if (file.canRead) { |
107 if (file.canRead) { |
108 for (line <- Source.fromFile(file).getLines) read_line(line) |
108 for (line <- Source.fromFile(file).getLines) read_line(line) |
109 } |
109 } |
110 } |
110 } |
111 |
111 |
130 } |
130 } |
131 |
131 |
132 |
132 |
133 /* constructor */ |
133 /* constructor */ |
134 |
134 |
135 read_symbols(IsabelleSystem.ISABELLE_HOME) |
135 read_symbols("$ISABELLE_HOME/etc/symbols") |
136 read_symbols(IsabelleSystem.ISABELLE_HOME_USER) |
136 read_symbols("$ISABELLE_HOME_USER/etc/symbols") |
137 init_recoders() |
137 init_recoders() |
138 } |
138 } |
139 |
139 |
140 } |
140 } |