diff options
| author |  mark <> | 2012-02-23 17:12:05 +0000 |
|---|---|---|
| committer | mark <> | 2012-02-23 17:12:05 +0000 |
| commit | 4ed83bcb88f220cc08c3223bd4f274eaa5f31e0c (patch) | |
| tree | 7bbf95ed0b561cfdf2e491ca8b6d614b9cdf0e49 /hol-light/TacticRecording/gvexport.ml | |
| parent | f1fdbc36e57c6005aed913830eabe2115dabc7c5 (diff) | |
Altered graph .dot export so that nodes are displayed as their tactic.
Diffstat (limited to 'hol-light/TacticRecording/gvexport.ml')
| -rw-r--r-- | hol-light/TacticRecording/gvexport.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/hol-light/TacticRecording/gvexport.ml b/hol-light/TacticRecording/gvexport.ml index 050ef997..952b3ad9 100644 --- a/hol-light/TacticRecording/gvexport.ml +++ b/hol-light/TacticRecording/gvexport.ml @@ -23,7 +23,10 @@ let rec print_gv_graphelem d ge = -> (print_indent d; print_goalid id1; print_string " -> "; print_goalid id2; print_string ";\n") | Single id - -> (print_indent d; print_goalid id; print_string ";\n");; + -> (print_indent d; print_goalid id; print_string ";\n") + | Name (id,x) + -> (print_indent d; print_goalid id; + print_string " [label = "; print_fstring x; print_string "];\n");; let print_gv_graph ges = let () = (cluster_count := 0) in |