improved tptp_graph robustness by relying on thy;
reused cleanup code;
improved messages;

--- a/src/HOL/TPTP/lib/Tools/tptp_graph	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Tue Apr 17 16:14:07 2012 +0100
@@ -71,6 +71,9 @@
       check_deps
       exit 0
       ;;
+    *)
+      exit 1
+      ;;
   esac
 done
 
@@ -88,31 +91,12 @@
       OUTPUT_FORMAT=2
       ;;
     *)
-      echo "Unrecognised output file extension."
+      echo "Unrecognised output file extension \".${2##*.}\"."
       exit 1
       ;;
 esac
 
-function generate_dot()
-{
-  #FIXME using a thy might be more robust
-  LOADER="use \"$TPTP_HOME/TPTP_Parser/ml_yacc_lib.ML\"; \
-          use \"$TPTP_HOME/TPTP_Parser/tptp_syntax.ML\"; \
-          use \"$TPTP_HOME/TPTP_Parser/tptp_lexyacc.ML\"; \
-          use \"$TPTP_HOME/TPTP_Parser/tptp_parser.ML\"; \
-          (*\"$TPTP_HOME/TPTP_Parser/tptp_problem_name.ML\";*) \
-          use \"$TPTP_HOME/TPTP_Parser/tptp_proof.ML\"; \
-          use \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\"; \
-          TPTP_To_Dot.write_proof_dot \"$1\" \"$2\"; exit 0;"
-  "$ISABELLE_PROCESS" -e "$LOADER" Pure
-}
-
-if [ "$OUTPUT_FORMAT" -eq 0 ]; then
-  [ -z "$NON_EXEC" ] && generate_dot "$1" "$2"
-  exit 0
-fi
-
-## set some essential variables
+## set some essential variables, prepare the work directory
 
 WORKDIR=""
 while :
@@ -125,10 +109,36 @@
 FILEDIR="$(cd "$(dirname "$2")"; cd "$(pwd -P)"; pwd)"
 FILENAME="${OUTPUT_FILENAME%.*}"
 WD="$(pwd)"
+mkdir -p $WORKDIR
 
-## generate and process files in temporary workdir, then move to destination dir
+function generate_dot()
+{
+  LOADER="tptp_graph_$RANDOM"
+  echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \
+        uses \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
+        begin ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
+        > $WORKDIR/$LOADER.thy
+  "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\"; exit 0;" Pure
+}
 
-mkdir -p $WORKDIR
+function cleanup_workdir()
+{
+  if [ -n "$KEEP_TEMP" ]; then
+      echo $WORKDIR
+  else
+      rm -rf $WORKDIR
+  fi
+}
+
+if [ "$OUTPUT_FORMAT" -eq 0 ]; then
+  [ -z "$NON_EXEC" ] && generate_dot "$1" "$2"
+  cleanup_workdir
+  exit 0
+fi
+
+## generate and process files in temporary workdir, then move required
+## output file to destination dir
+
 [ -z "$NON_EXEC" ] && generate_dot $1 "$WORKDIR/${FILENAME}.dot"
 cd $WORKDIR
 if [ -z "$NON_EXEC" ]; then
@@ -145,10 +155,6 @@
 fi
 [ -z "$NON_EXEC" ] && mv $TARGET $WD
 cd $WD
-if [ -n "$KEEP_TEMP" ]; then
-  echo $WORKDIR
-else
-  rm -rf $WORKDIR
-fi
+cleanup_workdir
 
 [ -n "$SHOW_TARGET" ] && echo "$FILEDIR/$TARGET"