src/Pure/Thy/symbol_input.ML
author wenzelm
Mon Dec 16 10:02:48 1996 +0100 (1996-12-16)
changeset 2405 e1b946f9c8be
child 3605 d372fb6ec393
permissions -rw-r--r--
symbol_input.ML: Defines 'use' command with symbol input filtering.
     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;