# HG changeset patch
# User sultana
# Date 1392825422 0
# Node ID c94f1a72d9c500639efa8777c53140540e180a4b
# Parent  014138b356c4b65f0eb7287b1f909094201d65e5
added more node shapes (matched with roles);

diff -r 014138b356c4 -r c94f1a72d9c5 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 16:33:11 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -3,6 +3,9 @@
 
 Translates parsed TPTP proofs into DOT format. This can then be processed
 by an accompanying script to translate the proofs into other formats.
+
+It tries to adhere to the symbols used in IDV, as described in
+"An Interactive Derivation Viewer" by Trac & Puzis & Sutcliffe, UITP 2006.
 *)
 
 signature TPTP_TO_DOT =
@@ -32,11 +35,11 @@
 fun the_role_shape role =
   case role of
     Role_Axiom => "triangle"
-  | Role_Hypothesis => "???"
-  | Role_Definition => raise NO_ROLE_SHAPE
-  | Role_Assumption => "???"
-  | Role_Lemma => "???"
-  | Role_Theorem => "???"
+  | Role_Hypothesis => "invtrapezium"
+  | Role_Definition => "invtriangle" (*NOTE this is not standard wrt IDV*)
+  | Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*)
+  | Role_Lemma => "hexagon"
+  | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*)
   | Role_Conjecture => "house"
   | Role_Negated_Conjecture => "invhouse"
   | Role_Plain => "circle"
@@ -70,8 +73,7 @@
 fun tptp_dot_node with_label reverse_arrows
  (Annotated_Formula (_, lang, n, role, fmla_tptp, annot)) =
  (*don't expect to find 'Include' in proofs*)
- if have_role_shape role
- then
+ if have_role_shape role then
    "\"" ^ n ^
    "\" [shape=\"" ^
       (if is_last_line lang fmla_tptp then "doublecircle"