# HG changeset patch
# User desharna
# Date 1761664046 -3600
# Node ID ea5f530ccfc572bee81b503a734c0c9722bea288
# Parent  19e7c4cece26fab8db8f0b8e4e8f0ba9c876f9a7
adapted tptp_translate to use new process_theory command

diff -r 19e7c4cece26 -r ea5f530ccfc5 src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Tue Oct 28 16:04:33 2025 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Tue Oct 28 16:07:26 2025 +0100
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 #
 # Author: Jasmin Blanchette
+# Author: Martin Desharnais-Schäfer
 #
 # DESCRIPTION: translate between TPTP formats
 
-
 PRG="$(basename "$0")"
 
 function usage() {
@@ -20,12 +20,25 @@
 [ "$#" -ne 2 -o "$1" = "-?" ] && usage
 
 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+SCRATCH_FILE=/tmp/${SCRATCH}.thy
 
 args=("$@")
 
-isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
+echo "theory ${SCRATCH} imports \"HOL-TPTP.ATP_Problem_Import\" begin \
+ML \<open> ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \<close> end" \
+    > "${SCRATCH_FILE}"
 
-echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML \<open> ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \<close> end" \
-  > /tmp/$SCRATCH.thy
-isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^   monotype.$"
+isabelle process_theories -O -U -l HOL-TPTP -f "${SCRATCH_FILE}" "${SCRATCH}" \
+    | grep --line-buffered -vE \
+        -e '^Running Draft ...$' \
+        -e '^[[:space:]]*$' \
+        -e '^Output \(line [[:digit:]]+ of ".*"):$' \
+        -e '^val it = \(\): unit$' \
+        -e '^Finished Draft \([0-9:]+ elapsed time(, [0-9:]+ cpu time, factor [0-9.]+)?\)$' \
+        -e '^PROOF FAILED for depth' \
+        -e '^Failure node' \
+        -e 'inferences so far.  Searching to depth' \
+        -e '^val ' \
+        -e 'Loading theory' \
+        -e '^poly.*warning: The type of' \
+        -e '^   monotype.$'