# HG changeset patch
# User sultana
# Date 1392825422 0
# Node ID c67c27f0ea9460fbb5404e1ace1b1e0ae3be458c
# Parent  37c1abaf4876b339ff55ce2b4e76d3537cc98611
improved configurability of DOT exporter;
tuned;

diff -r 37c1abaf4876 -r c67c27f0ea94 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -528,7 +528,8 @@
               | NONE => Free (n, dummyT) (*to infer the variable's type*)
              )
          | NONE =>
-             raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
+             Free (n, dummyT)
+             (*raise MISINTERPRET_TERM ("Could not type variable", tptp_t)*))
       else (*variables range over individuals*)
         Free (n, interpret_type config thy type_map (Defined_type Type_Ind)),
       thy)
diff -r 37c1abaf4876 -r c67c27f0ea94 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -25,21 +25,26 @@
 datatype style =
     (*Only draw shapes. No formulas or edge labels.*)
     Shapes
-    (*Don't draw shapes. Only write formulas (as nodes) and inference names (as edge labels)*)
+    (*Don't draw shapes. Only write formulas (as nodes) and inference names (as edge labels).*)
   | Formulas
+    (*Draw shapes and write the AF ID inside.*)
+  | IDs
 
+(*FIXME this kind of configurability isn't very user-friendly.*)
 (*Determine the require output style form the TPTP_GRAPH environment variable.
   Shapes is the default style.*)
 val required_style =
   if getenv "TPTP_GRAPH" = "formulas" then
     Formulas
+  else if getenv "TPTP_GRAPH" = "IDs" then
+    IDs
   else Shapes
 
 (*Draw an arc between two nodes*)
 fun dot_arc reverse (src, label) target =
   let
     val edge_label =
-      if required_style = Shapes then ""
+      if required_style = Shapes orelse required_style = IDs then ""
       else
         case label of
                 NONE => ""
@@ -104,6 +109,8 @@
    (*FIXME  add a parameter to switch to using the following code, which lowers, centers, and horizontally-bounds the label.
            (this is useful if you want to keep the shapes but also show formulas)*)
    (*    "\", label=\"\\\\begin{minipage}{10cm}\\\\vspace{21mm}\\\\centering$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\\\\end{minipage}\"];\n") ^*)
+      else if required_style = IDs then
+        "\", label=\"" ^ n ^ "\"];\n"
       else
         "\", label=\"\"];\n"
  in