# HG changeset patch
# User sultana
# Date 1392825422 0
# Node ID 5a9ef44731332141ec4d6035ab2fc31e2cec6e8e
# Parent  14e8e51c7fa858a3c52618dcf0dbcf91d6a49a0c
experimented with presentation of DOT+LaTeX;

diff -r 14e8e51c7fa8 -r 5a9ef4473133 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
@@ -41,10 +41,11 @@
   | Role_Lemma => "hexagon"
   | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*)
 
-  (*NOTE changed the next three to plaintext to avoid clutter, since
-         i'm also displaying the inference's conclusion in latex*)
-  | Role_Conjecture => "plaintext" (* "house" *)
-  | Role_Negated_Conjecture => "plaintext" (* "invhouse" *)
+  (*FIXME add a parameter to switch the behaviour described below.*)
+  (*NOTE can change the next three to plaintext to avoid clutter if
+         the inference's conclusion formula is also being displayed.*)
+  | Role_Conjecture => (* "plaintext" *) "house"
+  | Role_Negated_Conjecture => (* "plaintext" *) "invhouse"
   | Role_Plain => "plaintext" (* "circle" *) (*could also use none*)
 
   | Role_Fi_Domain => raise NO_ROLE_SHAPE
@@ -84,7 +85,10 @@
        else the_role_shape role) ^
    "\", style=\"" ^ the_lang_style lang ^
    (if role = Role_Definition then "\"];\n" else
-     "\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n") ^
+     (* "\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n") ^ *)
+(*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") ^
    (case TPTP_Proof.extract_source_info annot of
         SOME (TPTP_Proof.Inference (rule, _, pinfos)) =>
           let