X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=07233700a29f15ae43da3e8f223f3652a18c39b4;hb=f740ba9bd597dad3d2edede01433fd31cbb79bb7;hp=4dc34cfa1e074fdaff1f5d047cd10c6e73127949;hpb=3705200c998538c28d8cd9d3ca557616837daf05;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 4dc34cfa1..07233700a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2002, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -25,177 +25,342 @@ open Printf -open MatitaCicMisc open MatitaTypes -(* List utility functions *) -exception Skip +let add_trailing_slash = + let rex = Pcre.regexp "/$" in + fun s -> + if Pcre.pmatch ~rex s then s + else s ^ "/" -let list_map_fail f = - let rec aux = - function - [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Skip -> - (aux tl) - in - aux +let strip_blanks = + let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in + fun s -> + (Pcre.extract ~rex s).(1) -class proof_viewer obj = - object(self) +(** inherit from this class if you want to access current script *) +class scriptAccessor = +object (self) + method private script = MatitaScript.instance () +end - inherit GMathViewAux.single_selection_math_view obj +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 -(* initializer self#set_log_verbosity 3 *) +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 () - val mutable current_infos = None - val mutable current_mathml = None + (* is there any lablgtk2 constant corresponding to the left mouse button??? *) +let left_button = 1 - method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = - let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) - in - current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses); - let mathml = - ApplyTransformation.mml_of_cic_object ~explode_all:true - (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types - in - match current_mathml with - | None -> - debug_print "no previous MathML"; - self#load_root ~root:mathml#get_documentElement ; - current_mathml <- Some mathml - | Some current_mathml -> - debug_print "Previous MathML available: xmldiffing ..."; - self#freeze ; - XmlDiff.update_dom ~from:current_mathml mathml ; - self#thaw - end +let near (x1, y1) (x2, y2) = + let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in + (distance < 4.) -class sequent_viewer obj = - object(self) +let href_ds = Gdome.domString "href" +let xref_ds = Gdome.domString "xref" - inherit GMathViewAux.multi_selection_math_view obj +class clickableMathView obj = + let text_width = 80 in + object (self) + inherit GMathViewAux.multi_selection_math_view obj - val mutable current_infos = None + val mutable href_callback: (string -> unit) option = None + method set_href_callback f = href_callback <- f - method get_selected_terms = - let selections = self#get_selections in - list_map_fail - (function node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~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,_,_) -> - let id = xpath in - (try - Hashtbl.find ids_to_terms id - with _ -> raise Skip) - | None -> assert false (* "ERROR: No current term!!!" *) - ) selections - - method get_selected_hypotheses = - let selections = self#get_selections in - list_map_fail - (function node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + 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) + (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 + (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 + 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 <> "" +(* 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 - match current_infos with - Some (_,_,ids_to_hypotheses) -> - let id = xpath in - (try - Hashtbl.find ids_to_hypotheses id - with _ -> raise Skip) - | None -> assert false (* "ERROR: No current term!!!" *) - ) selections - - method load_sequent metasenv metano = -(* - let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_hypotheses) = - Cic2acic.asequent_of_sequent metasenv conjecture - in + 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 + + 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 + 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 + in +(* TODO: code for patterns + (* TODO context shouldn't be empty *) + let cic_sequent = ~-1, [], conclusion_pattern in +*) + 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 + + 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 sequentViewer obj = +object (self) + inherit clickableMathView obj + + 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_hypotheses,_ ))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in - current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); - debug_print "load_sequent: dumping MathML to /tmp/prova"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ()); + 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); + ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement end - -class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () +class sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () = 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 *) + + 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 sequentViewer to be destroyed as well *) + w#remove sequentViewer#coerce; + scrolledWin <- None + | None -> ()); for i = 1 to pages do notebook#remove_page 0 done; 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 metasenv = + method load_sequents (status: ProofEngineTypes.status) = + let ((_, metasenv, _, _), goal) = status in let sequents_no = List.length metasenv in _metasenv <- metasenv; - debug_print (sprintf "sequents no: %d" sequents_no); pages <- sequents_no; - let widget = sequent_viewer#coerce in + 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 sequentViewer#misc#parent with + | None -> w#add sequentViewer#coerce + | Some parent -> + let parent = + match sequentViewer#misc#parent with + None -> assert false + | Some p -> GContainer.cast_container p + in + parent#remove sequentViewer#coerce; + w#add sequentViewer#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; - let tab_label = - (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce - in - notebook#append_page ~tab_label widget) + notebook#append_page ~tab_label:(self#tab_label metano) (win metano)) metasenv; switch_page_callback <- - (* TODO Zack the "#after" may probably be removed after Luca's fix for - * widget not loading documents before being realized *) - Some (notebook#connect#after#switch_page ~callback:(fun page -> - debug_print "switch_page callback"; + Some (notebook#connect#switch_page ~callback:(fun page -> let goal = try List.assoc page page2goal with Not_found -> assert false in - set_goal goal; - self#render_page goal)) + self#script#setGoal goal; + self#render_page ~page ~goal)) - method private render_page goal = - sequent_viewer#load_sequent _metasenv goal + method private render_page ~page ~goal = + sequentViewer#load_sequent _metasenv goal; + try + List.assoc goal goal2win (); + sequentViewer#set_selection None + with Not_found -> assert false method goto_sequent goal = let page = @@ -204,30 +369,415 @@ class sequents_viewer ~(notebook:GPack.notebook) with Not_found -> assert false in notebook#goto_page page; - self#render_page goal + self#render_page page goal end (** constructors *) -let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = - GtkBase.Widget.size_params - ~cont:(OgtkMathViewProps.pack_return (fun p -> - OgtkMathViewProps.set_params - (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) - ~font_size ~log_verbosity)) - [] +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 proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] -let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () +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 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) + () = - new sequents_viewer ~notebook ~sequent_viewer ~set_goal () + 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 = sequentViewer ~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)); + 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 mutable current_infos = None + val mutable current_mathml = None + + val model = + new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview + + val mutable lastDir = "" (* last loaded "directory" *) + + 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 entry = + try + if entry <> current_entry || reloadable entry 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 = + 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, ids_to_inner_sorts, ids_to_inner_types) as info))) + = + ApplyTransformation.mml_of_cic_object obj + in + current_infos <- Some info; + (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); + + 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 () = + if reloadable current_entry then self#_load current_entry + + end + +let sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () += + new sequentsViewer ~notebook ~sequentViewer () + +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 :> 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_sequentsViewer () = + let gui = get_gui () in + let sequentViewer = sequentViewer_instance () in + sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () +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 :> 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 ()) !cicBrowsers + +let update_font_sizes () = + List.iter (fun b -> b#updateFontSize) !cicBrowsers; + (sequentViewer_instance ())#update_font_size