(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) open Printf open MatitaTypes open MatitaGtkMisc let add_trailing_slash = let rex = Pcre.regexp "/$" in fun s -> if Pcre.pmatch ~rex s then s else s ^ "/" let strip_blanks = let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in fun s -> (Pcre.extract ~rex s).(1) (** inherit from this class if you want to access current script *) class scriptAccessor = object (self) method private script = MatitaScript.instance () 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 ~default:BuildTimeConf.default_font_size "matita.font_size" let current_font_size = ref ~-1 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 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.) 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 *) 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; 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_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) 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 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 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 ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size:None ~log_verbosity:None)) [] class cicMathView obj = object (self) inherit clickableMathView obj val mutable current_mathml = None 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,_ ))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in 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 MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement 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 val mutable pages = 0 val mutable switch_page_callback = None val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) 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:"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 method reset = (match scrolledWin with | Some w -> (* removing page from the notebook will destroy all contained widget, * we do not want the cicMathView to be destroyed as well *) w#remove cicMathView#coerce; scrolledWin <- None | None -> ()); for i = 0 to pages do notebook#remove_page 0 done; notebook#set_show_tabs true; pages <- 0; page2goal <- []; goal2page <- []; goal2win <- []; _metasenv <- []; self#script#setGoal ~-1; (match switch_page_callback with | Some id -> GtkSignal.disconnect notebook#as_widget id; switch_page_callback <- None | None -> ()) method load_sequents (status: ProofEngineTypes.status) = let ((_, metasenv, _, _), goal) = status in let sequents_no = List.length metasenv in _metasenv <- metasenv; pages <- sequents_no; self#script#setGoal goal; let win metano = let w = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC ~shadow_type:`IN ~show:true () in let reparent () = scrolledWin <- Some w; 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 in let page = ref 0 in List.iter (fun (metano, _, _) -> page2goal <- (!page, metano) :: page2goal; goal2page <- (metano, !page) :: goal2page; incr page; notebook#append_page ~tab_label:(self#tab_label metano) (win metano)) metasenv; switch_page_callback <- Some (notebook#connect#switch_page ~callback:(fun page -> let goal = try List.assoc page page2goal with Not_found -> assert false in self#script#setGoal goal; self#render_page ~page ~goal)) method private render_page ~page ~goal = cicMathView#load_sequent _metasenv goal; try List.assoc goal goal2win (); cicMathView#set_selection None with Not_found -> assert false method goto_sequent goal = let page = try List.assoc goal goal2page with Not_found -> assert false in notebook#goto_page page; self#render_page page goal end (** constructors *) type 'widget constructor = ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> ?log_verbosity:int -> ?width:int -> ?height:int -> ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> 'widget let cicMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params (new cicMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = [ `Ast of DisambiguateTypes.term | `Cic of Cic.term * Cic.metasenv | `String of string ] class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = let term_RE = Pcre.regexp "^term:(.*)" in let whelp_RE = Pcre.regexp "^\\s*whelp" in let uri_RE = Pcre.regexp "^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 trailing_slash_RE = Pcre.regexp "/$" in let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" 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 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 = let q' = String.lowercase q in let rec aux i = function | [] -> failwith ("Whelp query '" ^ q ^ "' not found") | h::_ when String.lowercase h = q' -> i | _::tl -> aux (i+1) tl in 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" in activate_combo_query arg query in let toplevel = win#toplevel in let mathView = cicMathView ~packing:win#scrolledBrowser#add () in let fail message = MatitaGtkMisc.report_error ~title:"Cic browser" ~message ~parent:toplevel () in let tags = [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png"); "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ] in let handle_error f = try f () with exn -> fail (MatitaExcPp.to_string exn) in let handle_error' f = (fun () -> handle_error (fun () -> f ())) in object (self) inherit scriptAccessor (* Whelp bar queries *) initializer 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 (MatitaScript.instance ())#advance ~statement () in ignore(win#queryInputText#connect#activate ~callback:start_query); 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 () -> self#loadInput win#browserUri#entry#text))); ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> self#load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked (handle_error' (self#refresh ~force:true))); ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); ignore (win#browserForwardButton#connect#clicked (handle_error' self#forward)); ignore (win#toplevel#event#connect#delete (fun _ -> let my_id = Oo.id self in cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; if !cicBrowsers = [] && Helm_registry.get "matita.mode" = "cicbrowser" then GMain.quit (); false)); ignore(win#whelpResultTreeview#connect#row_activated ~callback:(fun _ _ -> handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri))))); self#_load (`About `Blank); toplevel#show () val mutable current_entry = `About `Blank 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 *) (* | [sel] -> win#browserUri#entry#text ^ sel |+ relative URI selected +| *) | [sel] -> lastDir ^ sel | _ -> assert false (** history RATIONALE * * All operations about history are done using _historyFoo. * Only toplevel functions (ATM load and loadInput) call _historyAdd. *) method private _historyAdd item = history#add item; win#browserBackButton#misc#set_sensitive true; win#browserForwardButton#misc#set_sensitive false method private _historyPrev () = let item = history#previous in if history#is_begin then win#browserBackButton#misc#set_sensitive false; win#browserForwardButton#misc#set_sensitive true; item method private _historyNext () = let item = history#next in if history#is_end then win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive true; item (** notebook RATIONALE * * Use only these functions to switch between the tabs *) method private _showList = win#mathOrListNotebook#goto_page 1 method private _showMath = win#mathOrListNotebook#goto_page 0 method private back () = try self#_load (self#_historyPrev ()) with MatitaMisc.History_failure -> () method private forward () = try self#_load (self#_historyNext ()) with MatitaMisc.History_failure -> () (* loads a uri which can be a cic uri or an about:* uri * @param uri string *) method private _load ?(force=false) entry = try if entry <> current_entry || entry = `About `Current_proof || force then begin (match entry with | `About `Current_proof -> self#home () | `About `Blank -> self#blank () | `About `Us -> () (* TODO implement easter egg here :-] *) | `Check term -> self#_loadCheck term | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Dir dir -> self#_loadDir dir | `Uri uri -> self#_loadUriManagerUri uri | `Whelp (query, results) -> set_whelp_query query; self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results)); self#setEntry entry end with exn -> fail (MatitaExcPp.to_string exn) method private blank () = self#_showMath; mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement method private _loadCheck term = failwith "not implemented _loadCheck"; self#_showMath method private home () = self#_showMath; match self#script#status.proof_status with | Proof (uri, metasenv, bo, ty) -> let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | Incomplete_proof ((uri, metasenv, bo, ty), _) -> let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | _ -> self#blank () (** loads a cic uri from the environment * @param uri UriManager.uri *) method private _loadUriManagerUri uri = let uri = UriManager.strip_xpointer uri in let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in self#_loadObj obj method private _loadDir dir = let content = Http_getter.ls dir in let l = List.fast_sort Pervasives.compare (List.map (function | Http_getter_types.Ls_section s -> "dir", s | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri) content) in lastDir <- dir; self#_loadList l method private setEntry entry = win#browserUri#entry#set_text (string_of_entry entry); current_entry <- entry method private _loadObj obj = (* 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 let dummyno = CicMkImplicit.new_meta metasenv [] in let sequent = (dummyno, context, term) in mathView#load_sequent (sequent :: metasenv) dummyno; self#_showMath method private _loadList l = model#list_store#clear (); List.iter (fun (tag, s) -> model#easy_append ~tag s) l; self#_showList (** { public methods, all must call _load!! } *) method load entry = handle_error (fun () -> self#_load entry; self#_historyAdd entry) (** this is what the browser does when you enter a string an hit enter *) method loadInput txt = let txt = strip_blanks txt in let fix_uri txt = UriManager.string_of_uri (UriManager.strip_xpointer (UriManager.uri_of_string txt)) in if is_whelp txt then begin set_whelp_query txt; (MatitaScript.instance ())#advance ~statement:(txt ^ ".") () end else begin let entry = match txt with | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt)) | txt when is_dir txt -> `Dir (add_trailing_slash txt) | txt -> (try entry_of_string txt with Invalid_argument _ -> command_error (sprintf "unsupported uri: %s" txt)) in self#_load entry; self#_historyAdd entry end (** {2 methods accessing underlying GtkMathView} *) method updateFontSize = mathView#set_font_size !current_font_size (** {2 methods used by constructor only} *) method win = win method history = history method currentEntry = current_entry method refresh ~force () = self#_load ~force current_entry end let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = new sequentsViewer ~notebook ~cicMathView () let cicBrowser () = let size = BuildTimeConf.browser_history_size in let rec aux history = let browser = new cicBrowser_impl ~history () in let win = browser#win in ignore (win#browserNewButton#connect#clicked (fun () -> let history = new MatitaMisc.browser_history ~memento:history#save size (`About `Blank) in let newBrowser = aux history in newBrowser#load browser#currentEntry)); (* (* attempt (failed) to close windows on CTRL-W ... *) MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL] GdkKeysyms._W (fun () -> win#toplevel#destroy ()); *) cicBrowsers := browser :: !cicBrowsers; (browser :> MatitaGuiTypes.cicBrowser) in let history = new MatitaMisc.browser_history size (`About `Blank) in aux history let default_cicMathView () = cicMathView ~show:true () let cicMathView_instance = MatitaMisc.singleton default_cicMathView let default_sequentsViewer () = 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 () = object(self) method private get_browser reuse = if reuse then (match !cicBrowsers with | [] -> cicBrowser () | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) else (cicBrowser ()) method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t method show_uri_list ?(reuse=false) ~entry l = (self#get_browser reuse)#load entry end let refresh_all_browsers () = List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; (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 ())