From c97fb85c9e568dfb4459a7118fcba2db38f5654c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 12 Jul 2006 17:15:19 +0000 Subject: [PATCH] use lablGraphviz to render the coercion graph and added a callback to follow hyperlinks there --- matita/matita.glade | 42 ++++++++++++++++++++++++++++++++++++++++ matita/matitaMathView.ml | 13 +++++++------ 2 files changed, 49 insertions(+), 6 deletions(-) diff --git a/matita/matita.glade b/matita/matita.glade index 8fc50338f..f94406c92 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -465,6 +465,48 @@ tab + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + False + True + + + + + + True + Graph + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + + tab + + 0 diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 10b7470a5..61f184584 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -795,6 +795,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in let gui = get_gui () in let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in + let gviz = LablGraphviz.gDot ~packing:win#graphScrolledWin#add () in let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in let combo,_ = GEdit.combo_box_text ~strings:queries () in let activate_combo_query input q = @@ -844,11 +845,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let filename, oc = Filename.open_temp_file "xx" ".dot" in output_string oc str; close_out oc; - let ps = Filename.temp_file "yy" ".png" in - ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename)); - Sys.remove filename; - at_exit (fun _ -> Sys.remove ps); - win#browserImage#set_file ps + gviz#load_graph_from_file filename; + HExtlib.safe_remove filename in object (self) inherit scriptAccessor @@ -901,6 +899,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri))))); + gviz#connect_href (fun _ attrs -> + let uri = List.assoc "href" attrs in + self#load (`Uri (UriManager.uri_of_string uri))); self#_load (`About `Blank); toplevel#show () @@ -996,7 +997,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) Lazy.force load_easter_egg method private coerchgraph () = - win#mathOrListNotebook#goto_page 2; + win#mathOrListNotebook#goto_page 3; load_coerchgraph () method private home () = -- 2.39.2