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