src/Pure/Thy/symbol_input.ML
author wenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 2564 9d66b758bce5
parent 2405 e1b946f9c8be
child 3605 d372fb6ec393
permissions -rw-r--r--
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
wenzelm@2405
     1
(*  Title:      Pure/Thy/symbol_input.ML
wenzelm@2405
     2
    ID:         $Id$
wenzelm@2405
     3
    Author:     David von Oheimb and Markus Wenzel, TU Muenchen
wenzelm@2405
     4
wenzelm@2405
     5
Defines 'use' command with symbol input filtering.
wenzelm@2405
     6
*)
wenzelm@2405
     7
wenzelm@2405
     8
signature SYMBOL_INPUT =
wenzelm@2405
     9
sig
wenzelm@2405
    10
  val use: string -> unit
wenzelm@2405
    11
end;
wenzelm@2405
    12
wenzelm@2405
    13
structure SymbolInput: SYMBOL_INPUT =
wenzelm@2405
    14
struct
wenzelm@2405
    15
wenzelm@2405
    16
fun file_exists name = file_info name <> "";
wenzelm@2405
    17
wenzelm@2405
    18
fun fix_name name =
wenzelm@2405
    19
  if file_exists name then name
wenzelm@2405
    20
  else if file_exists (name ^ ".ML") then name ^ ".ML"
wenzelm@2405
    21
  else if file_exists (name ^ ".sml") then name ^ ".sml"
wenzelm@2405
    22
  else error ("File not found: " ^ quote name);
wenzelm@2405
    23
wenzelm@2405
    24
wenzelm@2405
    25
val use =
wenzelm@2405
    26
  if not needs_filtered_use then use
wenzelm@2405
    27
  else
wenzelm@2405
    28
    fn raw_name =>
wenzelm@2405
    29
      let
wenzelm@2405
    30
        val name = fix_name raw_name;
wenzelm@2405
    31
wenzelm@2405
    32
        val infile = TextIO.openIn name;
wenzelm@2405
    33
        val txt = TextIO.inputAll infile;
wenzelm@2405
    34
        val _ = TextIO.closeIn infile;
wenzelm@2405
    35
wenzelm@2405
    36
        val txt_out = implode (SymbolFont.write_charnames' (explode txt));
wenzelm@2405
    37
      in
wenzelm@2405
    38
        if txt = txt_out then use name
wenzelm@2405
    39
        else
wenzelm@2405
    40
          let
wenzelm@2405
    41
            val tmp_name = "/tmp/" ^ base_name name;  (* FIXME unique prefix (!?) *)
wenzelm@2405
    42
            val outfile = TextIO.openOut tmp_name;
wenzelm@2405
    43
            val _ = TextIO.output (outfile, txt_out);
wenzelm@2405
    44
            val _ = TextIO.closeOut outfile;
wenzelm@2405
    45
wenzelm@2405
    46
            val rm = OS.FileSys.remove;
wenzelm@2405
    47
          in
wenzelm@2405
    48
            use tmp_name handle exn => (rm tmp_name; raise exn);
wenzelm@2405
    49
            rm tmp_name
wenzelm@2405
    50
          end
wenzelm@2405
    51
      end;
wenzelm@2405
    52
wenzelm@2405
    53
end;