X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=f81b2a2266677b43773d606608979792a604e412;hb=5c56a926588a63ceac31e6ddd6e3eeb02fadf3a9;hp=07233700a29f15ae43da3e8f223f3652a18c39b4;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 07233700a..f81b2a226 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -26,6 +26,7 @@
 open Printf
 
 open MatitaTypes
+open MatitaGtkMisc
 
 let add_trailing_slash =
   let rex = Pcre.regexp "/$" in
@@ -60,8 +61,11 @@ let increase_font_size () = incr current_font_size
 let decrease_font_size () = decr current_font_size
 let reset_font_size () = current_font_size := default_font_size ()
 
-  (* is there any lablgtk2 constant corresponding to the left mouse button??? *)
+  (* is there any lablgtk2 constant corresponding to the various mouse
+   * buttons??? *)
 let left_button = 1
+let middle_button = 2
+let right_button = 3
 
 let near (x1, y1) (x2, y2) =
   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
@@ -71,58 +75,77 @@ let href_ds = Gdome.domString "href"
 let xref_ds = Gdome.domString "xref"
 
 class clickableMathView obj =
-  let text_width = 80 in
-  object (self)
-    inherit GMathViewAux.multi_selection_math_view obj
-
-    val mutable href_callback: (string -> unit) option = None
-    method set_href_callback f = href_callback <- f
-
-    val mutable _cic_info = None
-    method private set_cic_info info = _cic_info <- info
-    method private cic_info =
-      match _cic_info with
-      | Some info -> info
-      | None -> assert false
-
-    initializer
-      self#set_font_size !current_font_size;
-      ignore (self#connect#selection_changed self#choose_selection);
-      ignore (self#event#connect#button_press self#button_press);
-      ignore (self#event#connect#button_release self#button_release);
-(*       ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
-        match gdome_elt with
-        | Some elt  |+ element is an hyperlink, use href_callback on it +|
-          when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href ->
-            (match href_callback with
-            | None -> ()
-            | Some f ->
-                let uri =
-                  elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href
-                in
-                f (uri#to_string))
-        | Some elt -> ignore (self#action_toggle elt)
-        | None -> ())) *)
-
-    val mutable button_press_x = -1.
-    val mutable button_press_y = -1.
-    val mutable selection_changed = false
-
-    method private button_press gdk_button =
-      if GdkEvent.Button.button gdk_button = left_button then begin
-        button_press_x <- GdkEvent.Button.x gdk_button;
-        button_press_y <- GdkEvent.Button.y gdk_button;
-        selection_changed <- false
-      end;
-      false
-
-    method private button_release gdk_button =
-      if GdkEvent.Button.button gdk_button = left_button then begin
-        let button_release_x = GdkEvent.Button.x gdk_button in
-        let button_release_y = GdkEvent.Button.y gdk_button in
-        (if near (button_press_x, button_press_y)
+let text_width = 80 in
+object (self)
+  inherit GMathViewAux.multi_selection_math_view obj
+
+  val mutable href_callback: (string -> unit) option = None
+  method set_href_callback f = href_callback <- f
+
+  val mutable _cic_info = None
+  method private set_cic_info info = _cic_info <- info
+  method private cic_info =
+    match _cic_info with
+    | Some info -> info
+    | None -> assert false
+
+  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#coerce#misc#connect#selection_get self#selection_get_cb);
+    self#coerce#misc#add_selection_target
+      ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary
+
+  val mutable button_press_x = -1.
+  val mutable button_press_y = -1.
+  val mutable selection_changed = false
+(*   val mutable ignore_next_selection_clear = false *)
+
+  method private selection_get_cb ctxt ~info ~time =
+    (match self#get_selections with
+    | [] -> ()
+    | node :: _ -> ctxt#return (self#string_of_node node))
+
+  method private selection_clear_cb sel_event =
+    self#remove_selections;
+    false
+
+  method private button_press_cb gdk_button =
+    let button = GdkEvent.Button.button gdk_button in
+    if  button = left_button then begin
+      button_press_x <- GdkEvent.Button.x gdk_button;
+      button_press_y <- GdkEvent.Button.y gdk_button;
+      selection_changed <- false
+    end else if button = right_button then
+      self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
+    false
+
+  method private popup_contextual_menu time =
+    match self#string_of_selection with
+    | None -> ()
+    | Some s ->
+        let clipboard = GData.clipboard Gdk.Atom.clipboard in
+        let menu = GMenu.menu () in
+        let copy_menu_item =
+          GMenu.image_menu_item
+            ~label:"_Copy" ~stock:`COPY ~packing:menu#append ()
+        in
+        connect_menu_item copy_menu_item (fun () -> clipboard#set_text s);
+        menu#popup ~button:right_button ~time
+
+  method private button_release_cb gdk_button =
+    let clipboard = GData.clipboard Gdk.Atom.primary in
+    if GdkEvent.Button.button gdk_button = left_button then begin
+      let button_release_x = GdkEvent.Button.x gdk_button in
+      let button_release_y = GdkEvent.Button.y gdk_button in
+      if selection_changed then
+        ()
+      else  (* selection _not_ changed *)
+        if near (button_press_x, button_press_y)
           (button_release_x, button_release_y)
-          && not selection_changed
         then
           let x = int_of_float button_press_x in
           let y = int_of_float button_press_y in
@@ -136,104 +159,86 @@ class clickableMathView obj =
                   (elt#getAttributeNS ~namespaceURI ~localName)#to_string
                   gdk_button
               else
-                ignore (self#action_toggle elt)));
-      end;
-      false
-
-    method private invoke_href_callback href_value 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 MatitaMisc.split href_value with
-            | [ uri ] ->  f uri
-            | uris ->
-                let menu = GMenu.menu () in
-                List.iter
-                  (fun uri ->
-                    let menu_item =
-                      GMenu.menu_item ~label:uri ~packing:menu#append ()
-                    in
-                    ignore (menu_item#connect#activate (fun () -> f uri)))
-                  uris;
-                menu#popup ~button ~time)
-
-    method private choose_selection gdome_elt =
-      let rec aux elt =
-        if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
-              ~localName:xref_ds)#to_string <> ""
+                ignore (self#action_toggle elt));
+    end;
+    false
+
+  method private invoke_href_callback href_value 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 MatitaMisc.split href_value with
+          | [ uri ] ->  f uri
+          | uris ->
+              let menu = GMenu.menu () in
+              List.iter
+                (fun uri ->
+                  let menu_item =
+                    GMenu.menu_item ~label:uri ~packing:menu#append ()
+                  in
+                  connect_menu_item menu_item (fun () -> f uri))
+                uris;
+              menu#popup ~button ~time)
+
+  method private choose_selection_cb gdome_elt =
+    let (gui: MatitaGuiTypes.gui) = get_gui () in
+    let clipboard = GData.clipboard Gdk.Atom.primary in
+    let rec aux elt =
+      if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
+            ~localName:xref_ds)#to_string <> ""
 (*         if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
-          && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
-              ~localName:xref_ds)#to_string <> "" *)
-        then
-          self#set_selection (Some elt)
-        else
-          try
-            (match elt#get_parentNode with
-            | None -> assert false
-            | Some p -> aux (new Gdome.element_of_node p))
-          with GdomeInit.DOMCastException _ -> ()
-(*             debug_print "trying to select above the document root" *)
-      in
-      (match gdome_elt with
-      | Some elt -> aux elt
-      | None   -> self#set_selection None);
-      selection_changed <- true
+        && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
+            ~localName:xref_ds)#to_string <> "" *)
+      then begin
+        self#set_selection (Some elt);
+        ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
+      end else
+        try
+          (match elt#get_parentNode with
+          | None -> assert false
+          | Some p -> aux (new Gdome.element_of_node p))
+        with GdomeInit.DOMCastException _ -> ()
+    in
+    (match gdome_elt with
+    | Some elt -> aux elt
+    | None -> self#set_selection None);
+    selection_changed <- true
 
-    method update_font_size = 
-      self#set_font_size !current_font_size
+  method update_font_size = self#set_font_size !current_font_size
 
-    method private get_term_by_id context id =
-      let ids_to_terms, ids_to_hypotheses = self#cic_info in
+  method private get_term_by_id context id =
+    let ids_to_terms, ids_to_hypotheses = self#cic_info in
+    try
+      `Term (Hashtbl.find ids_to_terms id)
+    with Not_found ->
       try
-        `Term (Hashtbl.find ids_to_terms id)
-      with Not_found ->
-        try
-          let hyp = Hashtbl.find ids_to_hypotheses id in
-          let context' = MatitaMisc.list_tl_at hyp context in
-          `Hyp context'
-        with Not_found -> assert false
-      
-    method string_of_selected_terms =
-      let get_id (node: Gdome.element) =
-        let xref_attr =
-          node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
-        in
-        xref_attr#to_string
-      in
-      let script = MatitaScript.instance () in
-      let metasenv = script#proofMetasenv in
-      let context = script#proofContext in
-      let conclusion = script#proofConclusion in
-      let cic_terms =
-        List.map
-          (fun node -> self#get_term_by_id context (get_id node))
-          self#get_selections
-      in
-(* TODO: code for patterns
-      let conclusion = (MatitaScript.instance ())#proofConclusion in
-      let conclusion_pattern =
-        ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
-      in
-*)
-      let dummy_goal = ~-1 in
-      let cic_sequent =
-        match cic_terms with
-        | [] -> assert false
-        | `Term t :: _ ->
-            let context' =
-              ProofEngineHelpers.locate_in_conjecture t
-                (dummy_goal, context, conclusion)
-            in
-            dummy_goal, context', t
-        | `Hyp context :: _ -> dummy_goal, context, Cic.Rel 1
+        let hyp = Hashtbl.find ids_to_hypotheses id in
+        let context' = MatitaMisc.list_tl_at hyp context in
+        `Hyp context'
+      with Not_found -> assert false
+    
+  method private string_of_node node =
+    let get_id (node: Gdome.element) =
+      let xref_attr =
+        node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
       in
+      xref_attr#to_string
+    in
+    let script = MatitaScript.instance () in
+    let metasenv = script#proofMetasenv in
+    let context = script#proofContext in
+    let conclusion = script#proofConclusion in
 (* TODO: code for patterns
-      (* TODO context shouldn't be empty *)
-      let cic_sequent = ~-1, [], conclusion_pattern in
+    let conclusion = (MatitaScript.instance ())#proofConclusion in
+    let conclusion_pattern =
+      ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
+    in
 *)
+    let dummy_goal = ~-1 in
+    let string_of_cic_sequent cic_sequent =
       let acic_sequent, _, _, ids_to_inner_sorts, _ =
         Cic2acic.asequent_of_sequent metasenv cic_sequent
       in
@@ -244,8 +249,29 @@ class clickableMathView obj =
       let pped_ast = CicNotationRew.pp_ast ast in
       let markup = CicNotationPres.render ids_to_uris pped_ast in
       BoxPp.render_to_string text_width markup
+    in
+    let term = self#get_term_by_id context (get_id node) in
+    let cic_sequent =
+      match term with
+      | `Term t ->
+          let context' =
+            ProofEngineHelpers.locate_in_conjecture t
+              (dummy_goal, context, conclusion)
+          in
+          dummy_goal, context', t
+      | `Hyp context -> dummy_goal, context, Cic.Rel 1
+    in
+    string_of_cic_sequent cic_sequent
 
-  end
+  method string_of_selections =
+    List.map self#string_of_node (List.rev self#get_selections)
+
+  method string_of_selection =
+    match self#get_selections with
+    | [] -> None
+    | node :: _ -> Some (self#string_of_node node)
+
+end
 
 let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
@@ -266,7 +292,7 @@ object (self)
     in
     self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses));
     let name = "sequent_viewer.xml" in
-    prerr_endline ("load_sequent: dumping MathML to ./" ^ name);
+    MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
     ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
@@ -404,13 +430,6 @@ type term_source =
   | `String of string
   ]
 
-class type cicBrowser =
-object
-  method load: MatitaTypes.mathViewer_entry -> unit
-  (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *)
-  method loadInput: string -> unit
-end
-
 let reloadable = function
   | `About `Current_proof
   | `Dir _ ->
@@ -528,6 +547,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     val mutable lastDir = ""  (* last loaded "directory" *)
 
+    method mathView = (mathView :> MatitaGuiTypes.clickableMathView)
+
     method private _getSelectedUri () =
       match model#easy_selection () with
       | [sel] when is_uri sel -> sel  (* absolute URI selected *)
@@ -661,7 +682,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           mathView#thaw
       |  _ ->
           let name = "cic_browser.xml" in
-          prerr_endline ("cic_browser: dumping MathML to ./" ^ name);
+          MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
           ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
           mathView#load_root ~root:mathml#get_documentElement;
           current_mathml <- Some mathml);
@@ -745,7 +766,7 @@ let cicBrowser () =
       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
 *)
     cicBrowsers := browser :: !cicBrowsers;
-    (browser :> cicBrowser)
+    (browser :> MatitaGuiTypes.cicBrowser)
   in
   let history = new MatitaMisc.browser_history size (`About `Blank) in
   aux history
@@ -765,7 +786,7 @@ let mathViewer () =
       if reuse then
         (match !cicBrowsers with
         | [] -> cicBrowser ()
-        | b :: _ -> (b :> cicBrowser))
+        | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
       else
         (cicBrowser ())
           
@@ -781,3 +802,24 @@ let update_font_sizes () =
   List.iter (fun b -> b#updateFontSize) !cicBrowsers;
   (sequentViewer_instance ())#update_font_size
 
+let get_math_views () =
+  ((sequentViewer_instance ()) :> MatitaGuiTypes.clickableMathView)
+  :: (List.map (fun b -> b#mathView) !cicBrowsers)
+
+let get_selections () =
+  if (MatitaScript.instance ())#onGoingProof () then
+    let rec aux =
+      function
+      | [] -> None
+      | mv :: tl ->
+          (match mv#string_of_selections with
+          | [] -> aux tl
+          | sels -> Some sels)
+    in
+    aux (get_math_views ())
+  else
+    None
+
+let reset_selections () =
+  List.iter (fun mv -> mv#remove_selections) (get_math_views ())
+