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 5de25e45b13b784bca64eb50c5fafbe7d7341f99..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 =
@@ -571,8 +583,8 @@ end
 let tab_label meta_markup =
   let rec aux =
     function
-    | `Current m -> sprintf "<b>%s</b>" (aux m)
     | `Closed m -> sprintf "<s>%s</s>" (aux m)
+    | `Current m -> sprintf "<b>%s</b>" (aux m)
     | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
     | `Meta n -> sprintf "?%d" n
   in
@@ -694,7 +706,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         ~env:(fun depth tag (pos, sw) ->
           let markup =
             match depth, pos with
-            | 0, _ -> `Current (render_switch sw)
+            | 0, 0 -> `Current (render_switch sw)
+            | 0, _ -> `Shift (pos, `Current (render_switch sw))
             | 1, pos when Stack.head_tag stack = `BranchTag ->
                 `Shift (pos, render_switch sw)
             | _ -> render_switch sw
@@ -782,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 =
@@ -824,7 +838,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   let load_easter_egg = lazy (
-    win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+    win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
+  in
+  let load_coerchgraph () = 
+      let str = CoercGraph.generate_dot_file () in
+      let filename, oc = Filename.open_temp_file "xx" ".dot" in
+      output_string oc str;
+      close_out oc;
+      gviz#load_graph_from_file filename;
+      HExtlib.safe_remove filename
   in
   object (self)
     inherit scriptAccessor
@@ -877,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 ()
 
@@ -940,12 +965,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       * @param uri string *)
     method private _load ?(force=false) entry =
       handle_error (fun () ->
-       if entry <> current_entry || entry = `About `Current_proof || force then
+       if entry <> current_entry || entry = `About `Current_proof || entry =
+         `About `Coercions || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
           | `About `Us -> self#egg ()
+          | `About `Coercions -> self#coerchgraph ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
@@ -969,6 +996,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#mathOrListNotebook#goto_page 2;
       Lazy.force load_easter_egg
 
+    method private coerchgraph () =
+      win#mathOrListNotebook#goto_page 3;
+      load_coerchgraph ()
+
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with