Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export proof when exporting problemfile
authorimmler@in.tum.de
Mon, 22 Jun 2009 17:07:08 +0200
changeset 31751 fda2cf4fef58
parent 31750 f28b7365fabf
child 31752 19a5f1c8a844
export proof when exporting problemfile
src/HOL/Tools/atp_wrapper.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
@@ -85,8 +85,13 @@
       else error ("Bad executable: " ^ Path.implode cmd)
     val (proof, rc) = system_out (cmdline ^ " " ^ fname)
 
-    (* remove *temporary* files *)
-    val _ = if destdir' = "" then OS.FileSys.remove fname else ()
+    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+    val _ =
+      if destdir' = "" then OS.FileSys.remove fname
+      else
+        let val out = TextIO.openOut (fname ^ "_proof")
+        val _ = TextIO.output (out, proof)
+        in TextIO.closeOut out end
     
     (* check for success and print out some information on failure *)
     val failure = find_failure proof
isabelle