src/Pure/Thy/symbol_input.ML
author berghofe
Wed Aug 06 00:29:02 1997 +0200 (1997-08-06)
changeset 3605 d372fb6ec393
parent 2405 e1b946f9c8be
child 3626 d91708377b6a
permissions -rw-r--r--
Removed function file_exists (now included in library.ML)
     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 fix_name name =
    17   if file_exists name then name
    18   else if file_exists (name ^ ".ML") then name ^ ".ML"
    19   else if file_exists (name ^ ".sml") then name ^ ".sml"
    20   else error ("File not found: " ^ quote name);
    21 
    22 
    23 val use =
    24   if not needs_filtered_use then use
    25   else
    26     fn raw_name =>
    27       let
    28         val name = fix_name raw_name;
    29 
    30         val infile = TextIO.openIn name;
    31         val txt = TextIO.inputAll infile;
    32         val _ = TextIO.closeIn infile;
    33 
    34         val txt_out = implode (SymbolFont.write_charnames' (explode txt));
    35       in
    36         if txt = txt_out then use name
    37         else
    38           let
    39             val tmp_name = "/tmp/" ^ base_name name;  (* FIXME unique prefix (!?) *)
    40             val outfile = TextIO.openOut tmp_name;
    41             val _ = TextIO.output (outfile, txt_out);
    42             val _ = TextIO.closeOut outfile;
    43 
    44             val rm = OS.FileSys.remove;
    45           in
    46             use tmp_name handle exn => (rm tmp_name; raise exn);
    47             rm tmp_name
    48           end
    49       end;
    50 
    51 end;