Cancel this question. I see the "file exists” is on purpose in the source code:
fun print_theories_as_tex_doc names path =
let val {dir, file} = Path.splitDirFile path
val dir = if Path.isAbsolute path orelse !emitTeXDir = "" then
dir
else
Path.concat(!emitTeXDir, dir)
val filename = Path.concat(dir, tex_suffix file)
val _ = not (FileSys.access (filename, [])) orelse
(TextIO.output(TextIO.stdErr,
"File " ^ path ^ " already exists.\n");
failwith "File exists”)
meanwhile I can use OS.FileSys.remove () to delete old files before calling
EmitTeX.print_theories_as_tex_doc () as I want. So there’s no issue at all.
Regards,
Chun
> Il giorno 06 mag 2017, alle ore 15:28, Chun Tian (binghe)
> <binghe.l...@gmail.com> ha scritto:
>
> Hi,
>
> When I use EmitTeX.print_theories_as_tex_doc to export theories into TeX
> documents, if the target TeX files already exist, the command reports HOL_ERR:
>
> File ../papers/references already exists.
> Exception-
> HOL_ERR
> {message = "File exists", origin_function = "failwith",
> origin_structure = "??"} raised
>
> This doesn’t make any sense, I think, as other commands like DB.html_theory
> () does allow overwriting files.
>
> Is there any hidden option that allows me to call
> EmitTeX.print_theories_as_tex_doc without deleting existing files first?
>
> Regards,
>
> Chun Tian
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
