# HG changeset patch
# User blanchet
# Date 1384794284 -3600
# Node ID 073f041d83ae963aa94e4ecd585447c08ac41b68
# Parent  7468e8ce494ccc32898715d9bccf7282e2ee5dfc
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life

diff -r 7468e8ce494c -r 073f041d83ae src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Mon Nov 18 17:10:57 2013 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Nov 18 18:04:44 2013 +0100
@@ -20,7 +20,7 @@
   val sledgehammer_tptp_file : theory -> int -> string -> unit
   val isabelle_tptp_file : theory -> int -> string -> unit
   val isabelle_hot_tptp_file : theory -> int -> string -> unit
-  val translate_tptp_file : theory -> string -> string -> string -> unit
+  val translate_tptp_file : theory -> string -> string -> unit
 end;
 
 structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
@@ -301,9 +301,9 @@
 
 (** Translator between TPTP(-like) file formats **)
 
-fun translate_tptp_file thy format_str in_file_name out_file_name =
+fun translate_tptp_file thy format_str file_name =
   let
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I in_file_name
+    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
     val conj = make_conj ([], []) (map snd conjs)
 
     val (format, type_enc, lam_trans) =
@@ -327,7 +327,7 @@
     val ord_info = K []
     val lines = lines_of_atp_problem format ord ord_info atp_problem
   in
-    File.write_list (exploded_absolute_path out_file_name) lines
+    List.app Output.physical_stdout lines
   end
 
 end;
diff -r 7468e8ce494c -r 073f041d83ae src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Nov 18 17:10:57 2013 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Nov 18 18:04:44 2013 +0100
@@ -9,20 +9,21 @@
 
 function usage() {
   echo
-  echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE"
+  echo "Usage: isabelle $PRG FORMAT FILE"
   echo
   echo "  Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")."
+  echo "  Emits the result to standard output."
   echo
   exit 1
 }
 
-[ "$#" -ne 3 -o "$1" = "-?" ] && usage
+[ "$#" -ne 2 -o "$1" = "-?" ] && usage
 
 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
 
 args=("$@")
 
 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \
+ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end;" \
   > /tmp/$SCRATCH.thy
 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory"