open Printf
open MatitaTypes
+open MatitaGtkMisc
let add_trailing_slash =
let rex = Pcre.regexp "/$" in
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
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
(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
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
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
| `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 _ ->
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 *)
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);
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
if reuse then
(match !cicBrowsers with
| [] -> cicBrowser ()
- | b :: _ -> (b :> cicBrowser))
+ | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
else
(cicBrowser ())
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 ())
+
projects / helm.git / blobdiff