--- a/src/Tools/WWW_Find/unicode_symbols.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Thu Jun 30 13:21:41 2011 +0200
@@ -135,11 +135,6 @@
val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
-val symbols_path =
- [getenv "ISABELLE_HOME", "etc", "symbols"]
- |> map Path.explode
- |> Path.appends;
-
end;
local (* build tables *)
@@ -164,8 +159,7 @@
fun read_symbols path =
let
val parsed_lines =
- File.read path
- |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
+ Symbol_Pos.explode (File.read path, Path.position path)
|> tokenize
|> filter is_proper
|> Scan.finite stopper (Scan.repeat line)
@@ -179,7 +173,7 @@
end;
local
-val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
+val (fromsym, fromabbr, tosym, toabbr) = read_symbols (Path.explode "~~/etc/symbols");
in
val symbol_to_unicode = Symtab.lookup fromsym;
val abbrev_to_unicode = Symtab.lookup fromabbr;