Ctr-C now cleans up (with a nice warning :-)

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 486866013dc2ed7c4129f22399f4ba0473e8cf6e..61f184584254256a30716d818eeda019814b26ba 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -246,7 +246,6 @@ object (self)
         | _ -> leave_href ())
     | None -> leave_href ()
 
-
   method private tactic_text_pattern_of_node node =
    let id = id_of_node node in
    let cic_info, unsh_sequent = self#get_cic_info id in
@@ -259,6 +258,16 @@ object (self)
        | Some hyp_name -> None, [ hyp_name, text ], None)
    | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
 
+  method private tactic_text_of_node node =
+   let id = id_of_node node in
+   let cic_info, unsh_sequent = self#get_cic_info id in
+   match self#get_term_by_id cic_info id with
+   | SelTerm (t, father_hyp) ->
+       let sequent = self#sequent_of_id ~paste_kind:`Term id in
+       let text = self#string_of_cic_sequent sequent in
+       text
+   | SelHyp (hyp_name, _ctxt) -> hyp_name
+
     (** @return a pattern structure which contains pretty printed terms *)
   method private tactic_text_pattern_of_selection =
     match self#get_selections with
@@ -420,10 +429,13 @@ object (self)
   method private string_of_node ~(paste_kind:paste_kind) node =
     if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
     then
-     let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
-      GrafiteAstPp.pp_tactic_pattern
-       ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
-       tactic_text_pattern
+      match paste_kind with
+      | `Pattern ->
+          let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
+          GrafiteAstPp.pp_tactic_pattern
+            ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
+            tactic_text_pattern
+      | `Term -> self#tactic_text_of_node node
     else string_of_dom_node node
 
   method private string_of_cic_sequent cic_sequent =
@@ -783,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 =
@@ -832,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
@@ -889,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 ()
 
@@ -984,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 () =