summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | sultana |

Wed, 19 Feb 2014 15:57:02 +0000 | |

changeset 55590 | 14e8e51c7fa8 |

parent 55589 | 8e6b2ad9cfe0 |

child 55591 | 5a9ef4473133 |

edges are now being shown in the proof graph;
removed the shapes related to the conjecture and the negated conjecture, to remove clutter (since i'm also showing the inference's conclusion in latex);

--- 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 @@ -40,9 +40,13 @@ | 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" + + (*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" *) | Role_Plain => "plaintext" (* "circle" *) (*could also use none*) + | Role_Fi_Domain => raise NO_ROLE_SHAPE | Role_Fi_Functors => raise NO_ROLE_SHAPE | Role_Fi_Predicates => raise NO_ROLE_SHAPE @@ -107,8 +111,7 @@ "node[width=0.5];\n" ^ "node[shape=plaintext];\n" ^ (* "node[fillcolor=lightgray];\n" ^ *) - "node[fontsize=50];\n" ^ - "edge[dir=none];\n" + "node[fontsize=50];\n" in TPTP_Parser.parse_file input_file |> map (tptp_dot_node true true)