X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=4bbaaddea52c08dc92738b0bf6503f4b097e5cf4;hb=517d7f0de0881a651d5b2f5adcc4063fe6332312;hp=b9affc23645e4d65ad8df81cfb306a85a7d53765;hpb=84c9131c30a4a991c595f61620794b1b75a5a16d;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index b9affc236..4bbaaddea 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -26,18 +26,7 @@ open Printf open MatitaTypes - -let list_map_fail f = - let rec aux = function - | [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Exit -> - (aux tl) - in - aux +open MatitaGtkMisc let add_trailing_slash = let rex = Pcre.regexp "/$" in @@ -57,6 +46,12 @@ object (self) end let cicBrowsers = ref [] +let gui_instance = ref None +let set_gui gui = gui_instance := Some gui +let get_gui () = + match !gui_instance with + | None -> assert false + | Some gui -> gui let default_font_size () = Helm_registry.get_opt_default Helm_registry.int @@ -66,110 +61,282 @@ 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 (distance < 4.) -class clickableMathView obj = - let href = Gdome.domString "href" in - let xref = Gdome.domString "xref" 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 +let href_ds = Gdome.domString "href" +let xref_ds = Gdome.domString "xref" + +(* ids_to_terms should not be passed here, is just for debugging *) +let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types = + let find_parent id ids = + let rec aux id = +(* (prerr_endline (sprintf "id %s = %s" id + (try + CicPp.ppterm (Hashtbl.find ids_to_terms id) + with Not_found -> "NONE"))); *) + if List.mem id ids then Some id + else + (match + (try Hashtbl.find ids_to_father_ids id with Not_found -> None) + with + | None -> None + | Some id' -> aux id') + in + aux id + in + let return_father id ids = + match find_parent id ids with + | None -> assert false + | Some parent_id -> parent_id + in + let mk_ids terms = List.map CicUtil.id_of_annterm terms in + let inner_types = + Hashtbl.fold + (fun _ types acc -> + match types.Cic2acic.annexpected with + None -> types.Cic2acic.annsynthesized :: acc + | Some ty -> ty :: types.Cic2acic.annsynthesized :: acc + ) ids_to_inner_types [] in + match annobj with + | Cic.AConstant (_, _, _, Some bo, ty, _, _) + | Cic.AVariable (_, _, Some bo, ty, _, _) + | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) -> + return_father id (mk_ids (ty :: bo :: inner_types)) + | Cic.AConstant (_, _, _, None, ty, _, _) + | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids (ty::inner_types)) + | Cic.AInductiveDefinition _ -> + assert false (* TODO *) - 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. - - method private button_press gdk_button = +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 = _cic_info + + 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) + + val mutable button_press_x = -1. + val mutable button_press_y = -1. + val mutable selection_changed = false + + method private selection_get_cb ctxt ~info ~time = +(* prerr_endline "selection_get_cb"; *) + (match self#get_selections with + | [] -> () + | node :: _ -> ctxt#return (self#string_of_node node)) + + method private selection_clear_cb sel_event = +(* prerr_endline "selection_clear_cb"; *) + self#remove_selections; + false + + method private button_press_cb gdk_button = +(* prerr_endline "button_press_cb"; *) + 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; - false + 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 = +(* prerr_endline "popup_contextual_menu"; *) + 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 gdk_button = + 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 near (button_press_x, button_press_y) - (button_release_x, button_release_y) - then - let x = int_of_float button_press_x in - let y = int_of_float button_press_y in - (match self#get_element_at x y with - | None -> () - | Some elt -> - let namespaceURI = DomMisc.xlink_ns in - let localName = href in - if elt#hasAttributeNS ~namespaceURI ~localName then - self#invoke_href_callback - (elt#getAttributeNS ~namespaceURI ~localName)#to_string - gdk_button - else - ignore (self#action_toggle elt))); - 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#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref 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" *) + if selection_changed then + () + else (* selection _not_ changed *) + if near (button_press_x, button_press_y) + (button_release_x, button_release_y) + then + let x = int_of_float button_press_x in + let y = int_of_float button_press_y in + (match self#get_element_at x y with + | None -> () + | Some elt -> + let namespaceURI = DomMisc.xlink_ns in + let localName = href_ds in + if elt#hasAttributeNS ~namespaceURI ~localName then + self#invoke_href_callback + (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 + 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 begin + self#set_selection (Some elt); + self#coerce#misc#add_selection_target + ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary; + 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 private get_term_by_id context cic_info id = + let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in + 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 private find_obj_conclusion id = + match self#cic_info with + | None + | Some (_, _, _, _, None) -> assert false + | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> + let id = + find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types + in + (try Hashtbl.find ids_to_terms id 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 id = get_id node in + let script = MatitaScript.instance () in + let metasenv = script#proofMetasenv in + let context = script#proofContext in + let metasenv, context, conclusion = + if script#onGoingProof () then + script#proofMetasenv, script#proofContext, script#proofConclusion + else + [], [], + let t = self#find_obj_conclusion id in + MatitaLog.debug (CicPp.ppterm t); + t + in +(* TODO: code for patterns + let conclusion = (MatitaScript.instance ())#proofConclusion in + let conclusion_pattern = + ProofEngineHelpers.pattern_of ~term:conclusion cic_terms + in +*) + let string_of_cic_sequent cic_sequent = + let acic_sequent, _, _, ids_to_inner_sorts, _ = + Cic2acic.asequent_of_sequent metasenv cic_sequent + in + let _, _, _, annterm = acic_sequent in + let ast, ids_to_uris = + CicNotationRew.ast_of_acic ids_to_inner_sorts annterm in - match gdome_elt with - | Some elt -> aux elt - | None -> self#set_selection None + 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 cic_info = + match self#cic_info with Some info -> info | None -> assert false + in + let cic_sequent = + match self#get_term_by_id context cic_info id with + | `Term t -> + let context' = + match + ProofEngineHelpers.locate_in_conjecture t + (~-1, context, conclusion) + with + [context,_] -> context + | _ -> assert false (* since it uses physical equality *) + in + ~-1, context', t + | `Hyp context -> ~-1, context, Cic.Rel 1 + in + string_of_cic_sequent cic_sequent - method update_font_size = - self#set_font_size !current_font_size - - 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 @@ -179,62 +346,47 @@ let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = ~font_size:None ~log_verbosity:None)) [] -class sequentViewer obj = - object(self) +class cicMathView obj = +object (self) + inherit clickableMathView obj - inherit clickableMathView obj + val mutable current_mathml = None - val mutable current_infos = None - - method get_selected_terms = - let selections = self#get_selections in - list_map_fail - (fun node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:DomMisc.helm_ns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - | Some (ids_to_terms,_,_) -> - (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit) - | None -> assert false) (* "ERROR: No current term!!!" *) - selections - - method get_selected_hypotheses = - let selections = self#get_selections in - list_map_fail - (fun node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:DomMisc.helm_ns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - | Some (_,_,ids_to_hypotheses) -> - (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit) - | None -> assert false) (* "ERROR: No current term!!!" *) - selections - method load_sequent metasenv metano = let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) = + let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in - current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); + self#set_cic_info + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); 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 -class sequentsViewer ~(notebook:GPack.notebook) - ~(sequentViewer:sequentViewer) () -= + method load_object obj = + let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) + let (mathml, + (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, ids_to_inner_types))) + = + ApplyTransformation.mml_of_cic_object obj + in + self#set_cic_info + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); + (match current_mathml with + | Some current_mathml when use_diff -> + self#freeze; + XmlDiff.update_dom ~from:current_mathml mathml; + self#thaw + | _ -> + let name = "cic_browser.xml" in + MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); + ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + self#load_root ~root:mathml#get_documentElement; + current_mathml <- Some mathml); +end + +class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = object (self) inherit scriptAccessor @@ -246,6 +398,17 @@ class sequentsViewer ~(notebook:GPack.notebook) val mutable _metasenv = [] val mutable scrolledWin: GBin.scrolled_window option = None (* scrolled window to which the sequentViewer is currently attached *) + val logo = (GMisc.image ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") () :> GObj.widget) + + val logo_with_qed = (GMisc.image ~file:"logo/matita_small.png" () :> GObj.widget) + + method load_logo = + notebook#set_show_tabs false; + notebook#append_page logo + + method load_logo_with_qed = + notebook#set_show_tabs false; + notebook#append_page logo_with_qed method private tab_label metano = (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce @@ -254,11 +417,12 @@ class sequentsViewer ~(notebook:GPack.notebook) (match scrolledWin with | Some w -> (* removing page from the notebook will destroy all contained widget, - * we do not want the sequentViewer to be destroyed as well *) - w#remove sequentViewer#coerce; + * we do not want the cicMathView to be destroyed as well *) + w#remove cicMathView#coerce; scrolledWin <- None | None -> ()); - for i = 1 to pages do notebook#remove_page 0 done; + for i = 0 to pages do notebook#remove_page 0 done; + notebook#set_show_tabs true; pages <- 0; page2goal <- []; goal2page <- []; @@ -284,9 +448,16 @@ class sequentsViewer ~(notebook:GPack.notebook) in let reparent () = scrolledWin <- Some w; - match sequentViewer#misc#parent with - | None -> w#add sequentViewer#coerce - | Some _ -> sequentViewer#misc#reparent w#coerce + match cicMathView#misc#parent with + | None -> w#add cicMathView#coerce + | Some parent -> + let parent = + match cicMathView#misc#parent with + None -> assert false + | Some p -> GContainer.cast_container p + in + parent#remove cicMathView#coerce; + w#add cicMathView#coerce in goal2win <- (metano, reparent) :: goal2win; w#coerce @@ -310,10 +481,10 @@ class sequentsViewer ~(notebook:GPack.notebook) self#render_page ~page ~goal)) method private render_page ~page ~goal = - sequentViewer#load_sequent _metasenv goal; + cicMathView#load_sequent _metasenv goal; try List.assoc goal goal2win (); - sequentViewer#set_selection None + cicMathView#set_selection None with Not_found -> assert false method goto_sequent goal = @@ -341,11 +512,11 @@ type 'widget constructor = unit -> 'widget -let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let cicMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + (new cicMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] @@ -358,19 +529,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 _ -> - true - | _ -> false - class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = @@ -387,8 +545,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 - let gui = MatitaGui.instance () in - let win = gui#newBrowserWin () in + let gui = get_gui () in + let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in let combo,_ = GEdit.combo_box_text ~strings:queries () in let activate_combo_query input q = @@ -411,7 +569,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) activate_combo_query arg query in let toplevel = win#toplevel in - let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in + let mathView = cicMathView ~packing:win#scrolledBrowser#add () in let fail message = MatitaGtkMisc.report_error ~title:"Cic browser" ~message ~parent:toplevel () @@ -444,7 +602,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore(combo#connect#changed ~callback:start_query); win#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png"); win#mathOrListNotebook#set_show_tabs false; - win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive false; ignore (win#browserUri#entry#connect#activate (handle_error' (fun () -> @@ -452,7 +609,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> self#load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked - (handle_error' self#refresh)); + (handle_error' (self#refresh ~force:true))); ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); ignore (win#browserForwardButton#connect#clicked (handle_error' self#forward)); @@ -474,14 +631,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) toplevel#show () val mutable current_entry = `About `Blank - val mutable current_infos = None - val mutable current_mathml = None val model = new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview 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 *) @@ -531,9 +688,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (* loads a uri which can be a cic uri or an about:* uri * @param uri string *) - method private _load entry = + method private _load ?(force=false) entry = try - if entry <> current_entry || reloadable entry then begin + if entry <> current_entry || entry = `About `Current_proof || force then + begin (match entry with | `About `Current_proof -> self#home () | `About `Blank -> self#blank () @@ -597,28 +755,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) current_entry <- entry method private _loadObj obj = - self#_showMath; - (* this must be _before_ loading the document, since - * if the widget is not mapped (hidden by the notebook) - * the document is not rendered *) - let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) - let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses,_,_))) = - ApplyTransformation.mml_of_cic_object obj - in - current_infos <- Some (ids_to_terms, ids_to_father_ids, - ids_to_conjectures, ids_to_hypotheses); - (match current_mathml with - | Some current_mathml when use_diff -> - mathView#freeze; - XmlDiff.update_dom ~from:current_mathml mathml; - mathView#thaw - | _ -> - let name = "cic_browser.xml" in - prerr_endline ("cic_browser: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); - mathView#load_root ~root:mathml#get_documentElement; - current_mathml <- Some mathml); + (* showMath must be done _before_ loading the document, since if the + * widget is not mapped (hidden by the notebook) the document is not + * rendered *) + self#_showMath; + mathView#load_object obj method private _loadTermCic term metasenv = let context = self#script#proofContext in @@ -671,15 +812,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method win = win method history = history method currentEntry = current_entry - method refresh () = - if reloadable current_entry then self#_load current_entry + method refresh ~force () = self#_load ~force current_entry end -let sequentsViewer ~(notebook:GPack.notebook) - ~(sequentViewer:sequentViewer) () -= - new sequentsViewer ~notebook ~sequentViewer () +let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = + new sequentsViewer ~notebook ~cicMathView () let cicBrowser () = let size = BuildTimeConf.browser_history_size in @@ -699,18 +837,18 @@ 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 -let default_sequentViewer () = sequentViewer ~show:true () -let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer +let default_cicMathView () = cicMathView ~show:true () +let cicMathView_instance = MatitaMisc.singleton default_cicMathView let default_sequentsViewer () = - let gui = MatitaGui.instance () in - let sequentViewer = sequentViewer_instance () in - sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () + let gui = get_gui () in + let cicMathView = cicMathView_instance () in + sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView () let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer let mathViewer () = @@ -719,7 +857,7 @@ let mathViewer () = if reuse then (match !cicBrowsers with | [] -> cicBrowser () - | b :: _ -> (b :> cicBrowser)) + | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) else (cicBrowser ()) @@ -729,9 +867,31 @@ let mathViewer () = (self#get_browser reuse)#load entry end -let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers +let refresh_all_browsers () = + List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; - (sequentViewer_instance ())#update_font_size + (cicMathView_instance ())#update_font_size + +let get_math_views () = + ((cicMathView_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 ())