equal
deleted
inserted
replaced
|
1 (* Title: Pure/Thy/symbol_input.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb and Markus Wenzel, TU Muenchen |
|
4 |
|
5 Defines 'use' command with symbol input filtering. |
|
6 *) |
|
7 |
|
8 signature SYMBOL_INPUT = |
|
9 sig |
|
10 val use: string -> unit |
|
11 end; |
|
12 |
|
13 structure SymbolInput: SYMBOL_INPUT = |
|
14 struct |
|
15 |
|
16 fun file_exists name = file_info name <> ""; |
|
17 |
|
18 fun fix_name name = |
|
19 if file_exists name then name |
|
20 else if file_exists (name ^ ".ML") then name ^ ".ML" |
|
21 else if file_exists (name ^ ".sml") then name ^ ".sml" |
|
22 else error ("File not found: " ^ quote name); |
|
23 |
|
24 |
|
25 val use = |
|
26 if not needs_filtered_use then use |
|
27 else |
|
28 fn raw_name => |
|
29 let |
|
30 val name = fix_name raw_name; |
|
31 |
|
32 val infile = TextIO.openIn name; |
|
33 val txt = TextIO.inputAll infile; |
|
34 val _ = TextIO.closeIn infile; |
|
35 |
|
36 val txt_out = implode (SymbolFont.write_charnames' (explode txt)); |
|
37 in |
|
38 if txt = txt_out then use name |
|
39 else |
|
40 let |
|
41 val tmp_name = "/tmp/" ^ base_name name; (* FIXME unique prefix (!?) *) |
|
42 val outfile = TextIO.openOut tmp_name; |
|
43 val _ = TextIO.output (outfile, txt_out); |
|
44 val _ = TextIO.closeOut outfile; |
|
45 |
|
46 val rm = OS.FileSys.remove; |
|
47 in |
|
48 use tmp_name handle exn => (rm tmp_name; raise exn); |
|
49 rm tmp_name |
|
50 end |
|
51 end; |
|
52 |
|
53 end; |