X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaMathView.ml;h=486866013dc2ed7c4129f22399f4ba0473e8cf6e;hb=da415a61eb8ecfc58817196363fad86b35efe490;hp=aa1b16a2871da2dd07959af03b24da61fe19716e;hpb=890221127070350c2e33aa4685398b03258aa847;p=helm.git

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index aa1b16a28..486866013 100644
--- 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
@@ -769,8 +775,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
   in
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
-  let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
-  let do_not_execute_whelp_query = ref false in
+  let whelp_query_RE = Pcre.regexp
+    "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" 
+  in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
@@ -786,14 +793,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       | _::tl -> aux (i+1) tl
     in
     win#queryInputText#set_text input;
-    do_not_execute_whelp_query:=true;
     combo#set_active (aux 0 queries);
   in
   let set_whelp_query txt =
     let query, arg = 
       try
         let q = Pcre.extract ~rex:whelp_query_RE txt in
-        q.(1), q.(2)
+        q.(1), q.(3)
       with Not_found -> failwith "Malformed Whelp query"
     in
     activate_combo_query arg query;
@@ -808,17 +814,29 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
       "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
   in
+  let b = (not (Helm_registry.get_bool "matita.debug")) in
   let handle_error f =
     try
       f ()
     with exn ->
-      if not (Helm_registry.get_bool "matita.debug") then
+      if b then
         fail (snd (MatitaExcPp.to_string exn))
       else raise exn
   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
@@ -829,19 +847,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       activate_combo_query "" "locate";
       win#whelpBarComboVbox#add combo#coerce;
       let start_query () = 
-        if !do_not_execute_whelp_query then
-          do_not_execute_whelp_query := false
-        else
-          begin
-          let query = 
-            try
-              String.lowercase (List.nth queries combo#active) 
-            with Not_found -> assert false
-          in
-          let input = win#queryInputText#text in
-          let statement = "whelp " ^ query ^ " (" ^ input ^ ")." in
-          (MatitaScript.current ())#advance ~statement ()
-          end
+       let query = 
+         try
+           String.lowercase (List.nth queries combo#active) 
+         with Not_found -> assert false in
+       let input = win#queryInputText#text in
+       let statement = 
+         if query = "locate" then
+             "whelp " ^ query ^ " \"" ^ input ^ "\"." 
+           else
+             "whelp " ^ query ^ " (" ^ input ^ ")." 
+       in
+        (MatitaScript.current ())#advance ~statement ()
       in
       ignore(win#queryInputText#connect#activate ~callback:start_query);
       ignore(combo#connect#changed ~callback:start_query);
@@ -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