X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=5de25e45b13b784bca64eb50c5fafbe7d7341f99;hb=ea1aa65dfc4a9ecad0793ca9ba708172dddd6fa0;hp=e2eb22d5b8f05371ac9f456597360b35668f2c74;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index e2eb22d5b..5de25e45b 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -154,6 +154,15 @@ type selected_term =
   | SelTerm of Cic.term * string option (* term, parent hypothesis (if any) *)
   | SelHyp of string * Cic.context (* hypothesis, context *)
 
+let hrefs_of_elt elt =
+  let localName = href_ds in
+  if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
+    let text =
+      (elt#getAttributeNS ~namespaceURI:xlink_ns ~localName)#to_string in
+    Some (HExtlib.split text)
+  else
+    None
+
 class clickableMathView obj =
 let text_width = 80 in
 object (self)
@@ -166,17 +175,24 @@ object (self)
   method private set_cic_info info = _cic_info <- info
   method private cic_info = _cic_info
 
+  val normal_cursor = Gdk.Cursor.create `LEFT_PTR
+  val href_cursor = Gdk.Cursor.create `HAND1
+
   initializer
     self#set_font_size !current_font_size;
     ignore (self#connect#selection_changed self#choose_selection_cb);
     ignore (self#event#connect#button_press self#button_press_cb);
     ignore (self#event#connect#button_release self#button_release_cb);
     ignore (self#event#connect#selection_clear self#selection_clear_cb);
+    ignore (self#connect#element_over self#element_over_cb);
     ignore (self#coerce#misc#connect#selection_get self#selection_get_cb)
 
   val mutable button_press_x = -1.
   val mutable button_press_y = -1.
   val mutable selection_changed = false
+  val mutable href_statusbar_msg:
+    (GMisc.statusbar_context * Gtk.statusbar_message) option = None
+    (* <statusbar ctxt, statusbar msg> *)
 
   method private selection_get_cb ctxt ~info ~time =
     let text =
@@ -208,21 +224,46 @@ object (self)
       self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
     false
 
+  method private element_over_cb (elt_opt, _, _, _) =
+    let win () = self#misc#window in
+    let leave_href () =
+      Gdk.Window.set_cursor (win ()) normal_cursor;
+      HExtlib.iter_option (fun (ctxt, msg) -> ctxt#remove msg)
+        href_statusbar_msg
+    in
+    match elt_opt with
+    | Some elt ->
+        (match hrefs_of_elt elt with
+        | Some ((_ :: _) as hrefs) ->
+            Gdk.Window.set_cursor (win ()) href_cursor;
+            let msg_text = (* now create statusbar msg and store it *)
+              match hrefs with
+              | [ href ] -> sprintf "Hyperlink to %s" href
+              | _ -> sprintf "Hyperlinks to: %s" (String.concat ", " hrefs) in
+            let ctxt = (get_gui ())#main#statusBar#new_context ~name:"href" in
+            let msg = ctxt#push msg_text in
+            href_statusbar_msg <- Some (ctxt, msg)
+        | _ -> 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
@@ -230,9 +271,13 @@ object (self)
       GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
     let check = add_menu_item ~label:"Check" () in
     let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
+    let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in
     menu#append reductions_menu_item;
+    menu#append tactics_menu_item;
     let reductions = GMenu.menu () in
+    let tactics = GMenu.menu () in
     reductions_menu_item#set_submenu reductions;
+    tactics_menu_item#set_submenu tactics;
     let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
     let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in
     let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
@@ -275,25 +320,20 @@ object (self)
           (match self#get_element_at x y with
           | None -> ()
           | Some elt ->
-              let localName = href_ds in
-              if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
-                self#invoke_href_callback
-                  (elt#getAttributeNS ~namespaceURI:xlink_ns
-                    ~localName)#to_string
-                  gdk_button
-              else
-                ignore (self#action_toggle elt));
+              (match hrefs_of_elt elt with
+              | Some hrefs -> self#invoke_href_callback hrefs gdk_button
+              | None -> ignore (self#action_toggle elt)))
     end;
     false
 
-  method private invoke_href_callback href_value gdk_button =
+  method private invoke_href_callback hrefs gdk_button =
     let button = GdkEvent.Button.button gdk_button in
     if button = left_button then
       let time = GdkEvent.Button.time gdk_button in
       match href_callback with
       | None -> ()
       | Some f ->
-          (match HExtlib.split href_value with
+          (match hrefs with
           | [ uri ] ->  f uri
           | uris ->
               let menu = GMenu.menu () in
@@ -301,7 +341,8 @@ object (self)
                 (fun uri ->
                   let menu_item =
                     GMenu.menu_item ~label:uri ~packing:menu#append () in
-                  connect_menu_item menu_item (fun () -> f uri))
+                  connect_menu_item menu_item 
+                  (fun () -> try f uri with Not_found -> assert false))
                 uris;
               menu#popup ~button ~time)
 
@@ -379,14 +420,17 @@ 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 =
     let script = MatitaScript.current () in
     let metasenv =
       if script#onGoingProof () then script#proofMetasenv else [] in
+    (*
     let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
       Cic2acic.asequent_of_sequent metasenv cic_sequent in
     let _, _, _, annterm = acic_sequent in
@@ -395,6 +439,9 @@ object (self)
     let pped_ast = TermContentPres.pp_ast ast in
     let markup = CicNotationPres.render ids_to_uris pped_ast in
     BoxPp.render_to_string text_width markup
+    *)
+    ApplyTransformation.txt_of_cic_sequent_conclusion 
+      text_width metasenv cic_sequent
 
   method private pattern_of term context unsh_sequent =
     let context_len = List.length context in
@@ -538,6 +585,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
   object (self)
     inherit scriptAccessor
 
+    method cicMathView = cicMathView  (** clickableMathView accessor *)
+
     val mutable pages = 0
     val mutable switch_page_callback = None
     val mutable page2goal = []  (* associative list: page no -> goal no *)
@@ -725,7 +774,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 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
@@ -740,17 +791,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       | h::_ when String.lowercase h = q' -> i
       | _::tl -> aux (i+1) tl
     in
+    win#queryInputText#set_text input;
     combo#set_active (aux 0 queries);
-    win#queryInputText#set_text input
   in
   let set_whelp_query txt =
     let query, arg = 
       try
         let q = Pcre.extract ~rex:whelp_query_RE txt in
-        q.(1), q.(2)
-      with Invalid_argument _ -> failwith "Malformed Whelp query"
+        q.(1), q.(3)
+      with Not_found -> failwith "Malformed Whelp query"
     in
-    activate_combo_query arg query
+    activate_combo_query arg query;
   in
   let toplevel = win#toplevel in
   let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
@@ -762,11 +813,12 @@ 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
@@ -783,9 +835,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       activate_combo_query "" "locate";
       win#whelpBarComboVbox#add combo#coerce;
       let start_query () = 
-        let query = String.lowercase (List.nth queries combo#active) in
-        let input = win#queryInputText#text in
-        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
+       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);