From a08493538b6e678fd812356dd6965aa31bf1f769 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 1 Aug 2006 09:53:39 +0000 Subject: [PATCH] - added a label_of_uri function to easily change node labels - increased font size and use names as node labels (make CSC happy :)) --- components/metadata/metadataDeps.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/components/metadata/metadataDeps.ml b/components/metadata/metadataDeps.ml index 3247114a2..91fa8004c 100644 --- a/components/metadata/metadataDeps.ml +++ b/components/metadata/metadataDeps.ml @@ -98,7 +98,10 @@ struct let fat_value = 20 let fat_increment = fat_value let incomplete_attrs = ["style", "dashed"] - let global_node_attrs = ["fontsize", "9"; "width", ".4"; "height", ".4"] + let global_node_attrs = ["fontsize", "12"; "width", ".4"; "height", ".4"] + + let label_of_uri uri = UriManager.name_of_uri uri + (*let label_of_uri uri = UriManager.string_of_uri uri*) type neighborhood = { adjacency: UriManager.uri list lazy_t; (* all outgoing edges *) @@ -137,7 +140,7 @@ struct let suri = UriManager.string_of_uri uri in Pp.node suri ~attrs:([ "href", UriManager.string_of_uri uri; - (*"label", UriManager.name_of_uri uri*) + "label", label_of_uri uri ] @ (if is_complete uri then [] else incomplete_attrs)) fmt; let new_nodes = ref [] in -- 2.39.2