equal
deleted
inserted
replaced
10 val use: string -> unit |
10 val use: string -> unit |
11 end; |
11 end; |
12 |
12 |
13 structure SymbolInput: SYMBOL_INPUT = |
13 structure SymbolInput: SYMBOL_INPUT = |
14 struct |
14 struct |
15 |
|
16 fun file_exists name = file_info name <> ""; |
|
17 |
15 |
18 fun fix_name name = |
16 fun fix_name name = |
19 if file_exists name then name |
17 if file_exists name then name |
20 else if file_exists (name ^ ".ML") then name ^ ".ML" |
18 else if file_exists (name ^ ".ML") then name ^ ".ML" |
21 else if file_exists (name ^ ".sml") then name ^ ".sml" |
19 else if file_exists (name ^ ".sml") then name ^ ".sml" |