1(*---------------------------------------------------------------------------*
2 * A version of "use" that filters quotations. The native MoscowML version   *
3 * of "use" is found in the "Meta" structure.                                *
4 *---------------------------------------------------------------------------*)
5
6local
7  (* used to stand for "has double quote", but the same analysis is necessary
8     even for files that contain single quotes because of the special
9     treatment that the filter gives to things like `s1 ^ s2`
10  *)
11  fun has_dq file =
12      let
13        val istrm = TextIO.openIn file
14        fun loop() =
15            case TextIO.input1 istrm of
16              NONE => false
17            | SOME #"`" => true
18            | SOME c => Char.ord c > 127 orelse loop()
19      in
20        loop() before TextIO.closeIn istrm
21      end handle Io _ => false
22  infix ++
23  fun p1 ++ p2 = Path.concat (p1, p2)
24  fun unquote_to file1 file2 =
25      Systeml.systeml [HOLDIR ++ "bin" ++ "unquote", file1, file2]
26in
27fun use s =
28  if has_dq s then
29    let
30      val filename = FileSys.tmpName()^".hol"
31    in
32      if Process.isSuccess (unquote_to s filename) then
33        (Meta.use filename; FileSys.remove filename)
34        handle e => (FileSys.remove filename handle _ => (); raise e)
35      else (TextIO.output(TextIO.stdOut,
36                          ("Failed to translate file: "^s^"\n"));
37            raise Fail "use")
38    end
39  else Meta.use s
40end;
41