updated dependences

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 44be731de19a21fabf5284193549ce80108d97ce..486866013dc2ed7c4129f22399f4ba0473e8cf6e 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -246,21 +246,24 @@ 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
+   match self#get_term_by_id cic_info id with
+   | SelTerm (t, father_hyp) ->
+       let sequent = self#sequent_of_id ~paste_kind:`Pattern id in
+       let text = self#string_of_cic_sequent sequent in
+       (match father_hyp with
+       | None -> None, [], Some text
+       | Some hyp_name -> None, [ hyp_name, text ], None)
+   | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
+
     (** @return a pattern structure which contains pretty printed terms *)
   method private tactic_text_pattern_of_selection =
     match self#get_selections with
     | [] -> assert false (* this method is invoked only if there's a sel. *)
-    | 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:`Pattern id in
-            let text = self#string_of_cic_sequent sequent in
-            (match father_hyp with
-            | None -> None, [], Some text
-            | Some hyp_name -> None, [ hyp_name, text ], None)
-        | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
+    | node :: _ -> self#tactic_text_pattern_of_node node
 
   method private popup_contextual_menu time =
     let menu = GMenu.menu () in
@@ -417,8 +420,10 @@ object (self)
   method private string_of_node ~(paste_kind:paste_kind) node =
     if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
     then
-      let id = id_of_node node in
-      self#string_of_cic_sequent (self#sequent_of_id ~paste_kind id)
+     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
     else string_of_dom_node node
 
   method private string_of_cic_sequent cic_sequent =
@@ -566,8 +571,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
@@ -689,7 +694,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
@@ -819,7 +825,18 @@ 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;
+      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
   in
   object (self)
     inherit scriptAccessor
@@ -935,12 +952,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
@@ -964,6 +983,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 2;
+      load_coerchgraph ()
+
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with