X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=9990805ad7614ce2ab407700bb8f27363a3ae2d5;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=3364b55f32270aee5e57e65bd425fc08216bf10a;hpb=a22f5e32e698c3874ded926bd7dabc19719098f3;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 3364b55f3..9990805ad 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -65,6 +65,7 @@ let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in (distance < 4.) +(* let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML" let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" @@ -83,12 +84,15 @@ let empty_mathml = lazy ( let empty_boxml = lazy ( domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) ~qualifiedName:(Gdome.domString "box") ~doctype:None) + *) (** shown for goals closed by side effects *) let closed_goal_mathml = lazy "chiuso per side effect..." +(* (* 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 = + assert false (* MATITA 1.0 let find_parent id ids = let rec aux id = (* (prerr_endline (sprintf "id %s = %s" id @@ -128,6 +132,7 @@ let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types = return_father id (mk_ids (ty::inner_types)) | Cic.AInductiveDefinition _ -> assert false (* TODO *) + *) (** @return string content of a dom node having a single text child node, e.g. * bool *) @@ -175,6 +180,7 @@ let rec has_maction (elt :Gdome.element) = has_maction (new Gdome.element_of_node node) | _ -> false ;; +*) class clickableMathView obj = let text_width = 80 in @@ -183,23 +189,31 @@ object (self) method has_selection = (assert false : bool) method strings_of_selection = (assert false : (paste_kind * string) list) - method update_font_size = (assert false : unit) + method update_font_size = + self#misc#modify_font_by_name + (sprintf "%s %d" BuildTimeConf.script_font !current_font_size) method set_href_callback = (function _ -> () : (string -> unit) option -> unit) - method private set_cic_info = (function _ -> () : (Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t * + method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.hypothesis) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option) option -> unit) + (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit) (* dal widget di Luca *) method load_root ~root = self#buffer#delete ~start:(self#buffer#get_iter `START) ~stop:(self#buffer#get_iter `END); self#buffer#insert root method remove_selections = (() : unit) - method set_selection = (fun _ -> () : Gdome.element option -> unit) - method get_selections = (assert false : Gdome.element list) + method set_selection = (fun _ -> () : unit option -> unit) + method get_selections = (assert false : unit list) method set_font_size font_size = self#misc#modify_font_by_name (sprintf "%s %d" BuildTimeConf.script_font font_size) + initializer + self#set_font_size !current_font_size; + self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang); + self#source_buffer#set_highlight_syntax true; + self#set_editable false + (* MATITA1.0 inherit GMathViewAux.multi_selection_math_view obj @@ -605,29 +619,8 @@ object (self) val mutable current_mathml = None - method load_sequent metasenv metano = - let sequent = CicUtil.lookup_meta metano metasenv in - let (txt, unsh_sequent, - (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) - = - ApplyTransformation.txt_of_cic_sequent_all - ~map_unicode_to_tex:false 80 (*MATITA 1.0??*) metasenv sequent - in - self#set_cic_info - (Some (Some unsh_sequent, - ids_to_terms, ids_to_hypotheses, ids_to_father_ids, - Hashtbl.create 1, None)); - (*MATITA 1.0 - if BuildTimeConf.debug then begin - let name = - "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in - HLog.debug ("load_sequent: dumping MathML to ./" ^ name); - ignore (domImpl#saveDocumentToFile ~name ~doc:txt ()) - end; *) - self#load_root ~root:txt - method nload_sequent: - 'status. #NCicCoercion.status as 'status -> NCic.metasenv -> + 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -643,34 +636,8 @@ object (self) end;*) self#load_root ~root:txt - method load_object obj = - let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) - let (txt, - (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, ids_to_inner_types))) - = - ApplyTransformation.txt_of_cic_object_all ~map_unicode_to_tex:false - 80 [] obj - in - self#set_cic_info - (Some (None, 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 -> -assert false (*MATITA1.0 - self#freeze; - XmlDiff.update_dom ~from:current_mathml mathml; - self#thaw*) - | _ -> - (* MATITA1.0 if BuildTimeConf.debug then begin - let name = - "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in - HLog.debug ("cic_browser: dumping MathML to ./" ^ name); - ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) - end;*) - self#load_root ~root:txt; - current_mathml <- Some txt); - method load_nobject : - 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit + 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -760,88 +727,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- `Old []; self#script#setGoal None - method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a - = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack } - -> - _metasenv <- `Old metasenv; - pages <- 0; - let win goal_switch = - let w = - GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS - ~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 <- (goal_switch, reparent) :: goal2win; - w#coerce - in - assert ( - let stack_goals = Stack.open_goals stack in - let proof_goals = ProofEngineTypes.goals_of_proof proof in - if - HExtlib.list_uniq (List.sort Pervasives.compare stack_goals) - <> List.sort Pervasives.compare proof_goals - then begin - prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals)); - prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals)); - false - end - else true - ); - let render_switch = - function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i) - in - let page = ref 0 in - let added_goals = ref [] in - (* goals can be duplicated on the tack due to focus, but we should avoid - * multiple labels in the user interface *) - let add_tab markup goal_switch = - let goal = Stack.goal_of_switch goal_switch in - if not (List.mem goal !added_goals) then begin - ignore(notebook#append_page - ~tab_label:(tab_label markup) (win goal_switch)); - page2goal <- (!page, goal_switch) :: page2goal; - goal2page <- (goal_switch, !page) :: goal2page; - incr page; - pages <- pages + 1; - added_goals := goal :: !added_goals - end - in - let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in - Stack.iter (** populate notebook with tabs *) - ~env:(fun depth tag (pos, sw) -> - let markup = - match depth, pos with - | 0, 0 -> `Current (render_switch sw) - | 0, _ -> `Shift (pos, `Current (render_switch sw)) - | 1, pos when Stack.head_tag stack = `BranchTag -> - `Shift (pos, render_switch sw) - | _ -> render_switch sw - in - add_tab markup sw) - ~cont:add_switch ~todo:add_switch - stack; - switch_page_callback <- - Some (notebook#connect#switch_page ~callback:(fun page -> - let goal_switch = - try List.assoc page page2goal with Not_found -> assert false - in - self#script#setGoal (Some (goal_of_switch goal_switch)); - self#render_page status ~page ~goal_switch)) - - method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit - = fun status -> + method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit + = fun (status : #GrafiteTypes.status) -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; @@ -921,13 +808,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #NCicCoercion.status as 'status -> page:int -> + 'status. #ApplyTransformation.status as 'status -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page ~goal_switch -> (match goal_switch with | Stack.Open goal -> (match _metasenv with - `Old menv -> cicMathView#load_sequent menv goal + `Old menv -> assert false (* MATITA 1.0 *) | `New (menv,subst) -> cicMathView#nload_sequent status menv subst goal) | Stack.Closed goal -> @@ -938,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit + method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit = fun status goal -> let goal_switch, page = try @@ -1001,8 +888,7 @@ let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = - [ `Ast of CicNotationPt.term - | `Cic of Cic.term * Cic.metasenv + [ `Ast of NotationPt.term | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `String of string ] @@ -1010,35 +896,16 @@ type term_source = class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = - 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 metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in - let whelp_query_RE = Pcre.regexp - "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" - in - let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt 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 gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () 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 - win#queryInputText#set_text input; - combo#set_active (aux 0 queries); - in let searchText = GSourceView2.source_view ~auto_indent:false ~editable:false () in @@ -1062,15 +929,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore(win#entrySearch#connect#activate ~callback); ignore(win#buttonSearch#connect#clicked ~callback); in - let set_whelp_query txt = - let query, arg = - try - let q = Pcre.extract ~rex:whelp_query_RE txt in - q.(1), q.(3) - with Not_found -> 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 = @@ -1124,12 +982,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let status = (MatitaScript.current ())#grafite_status in NCicCoercion.generate_dot_file status fmt; Pp.trailer fmt; - Pp.header - ~name:"OLDCoercions" - ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] - ~edge_attrs:["fontsize", "10"] fmt; - CoercGraph.generate_dot_file fmt; - Pp.trailer fmt; Pp.raw "@." fmt; close_out oc; if tred then @@ -1143,33 +995,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) object (self) inherit scriptAccessor - (* Whelp bar queries *) - - val mutable gviz_graph = MetadataDeps.DepGraph.dummy - val mutable gviz_uri = UriManager.uri_of_string "cic:/dummy.con"; + val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec"; val dep_contextual_menu = GMenu.menu () initializer - activate_combo_query "" "locate"; - win#whelpBarComboVbox#add combo#coerce; - let start_query () = - let query = - try - String.lowercase (List.nth queries combo#active) - with Not_found -> assert false in - let input = win#queryInputText#text in - let statement = - if query = "locate" then - "whelp " ^ query ^ " \"" ^ input ^ "\"." - else - "whelp " ^ query ^ " (" ^ input ^ ")." - in - (MatitaScript.current ())#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; @@ -1191,68 +1021,23 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> - let uri = - try - `Uri (UriManager.uri_of_string uri) - with - UriManager.IllFormedUri _ -> - `NRef (NReference.reference_of_string uri) - in + let uri = `NRef (NReference.reference_of_string uri) in self#load uri))); gviz#connect_href (fun button_ev attrs -> let time = GdkEvent.Button.time button_ev in let uri = List.assoc "href" attrs in - gviz_uri <- UriManager.uri_of_string uri; + gviz_uri <- NReference.reference_of_string uri; match GdkEvent.Button.button button_ev with - | button when button = left_button -> self#load (`Uri gviz_uri) + | button when button = left_button -> self#load (`NRef gviz_uri) | button when button = right_button -> dep_contextual_menu#popup ~button ~time | _ -> ()); - connect_menu_item win#depGraphMenuItem (fun () -> - match self#currentCicUri with - | Some uri -> self#load (`Metadata (`Deps (`Fwd, uri))) - | None -> ()); - connect_menu_item win#invDepGraphMenuItem (fun () -> - match self#currentCicUri with - | Some uri -> self#load (`Metadata (`Deps (`Back, uri))) - | None -> ()); connect_menu_item win#browserCloseMenuItem (fun () -> let my_id = Oo.id self in cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; win#toplevel#misc#hide(); win#toplevel#destroy ()); - (* remove hbugs *) - (* - connect_menu_item win#hBugsTutorsMenuItem (fun () -> - self#load (`HBugs `Tutors)); - *) - win#hBugsTutorsMenuItem#misc#hide (); connect_menu_item win#browserUrlMenuItem (fun () -> win#browserUri#misc#grab_focus ()); - connect_menu_item win#univMenuItem (fun () -> - match self#currentCicUri with - | Some uri -> self#load (`Univs uri) - | None -> ()); - - (* fill dep graph contextual menu *) - let go_menu_item = - GMenu.image_menu_item ~label:"Browse it" - ~packing:dep_contextual_menu#append () in - let expand_menu_item = - GMenu.image_menu_item ~label:"Expand" - ~packing:dep_contextual_menu#append () in - let collapse_menu_item = - GMenu.image_menu_item ~label:"Collapse" - ~packing:dep_contextual_menu#append () in - dep_contextual_menu#append (go_menu_item :> GMenu.menu_item); - dep_contextual_menu#append (expand_menu_item :> GMenu.menu_item); - dep_contextual_menu#append (collapse_menu_item :> GMenu.menu_item); - connect_menu_item go_menu_item (fun () -> self#load (`Uri gviz_uri)); - connect_menu_item expand_menu_item (fun () -> - MetadataDeps.DepGraph.expand gviz_uri gviz_graph; - self#redraw_gviz ~center_on:gviz_uri ()); - connect_menu_item collapse_menu_item (fun () -> - MetadataDeps.DepGraph.collapse gviz_uri gviz_graph; - self#redraw_gviz ~center_on:gviz_uri ()); self#_load (`About `Blank); toplevel#show () @@ -1262,8 +1047,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** @return None if no object uri can be built from the current entry *) method private currentCicUri = match current_entry with - | `Uri uri - | `Metadata (`Deps (_, uri)) -> Some uri + | `NRef uri -> Some uri | _ -> None val model = @@ -1314,7 +1098,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _showList2 = win#mathOrListNotebook#goto_page 5 method private _showSearch = win#mathOrListNotebook#goto_page 6 method private _showGviz = win#mathOrListNotebook#goto_page 3 - method private _showHBugs = win#mathOrListNotebook#goto_page 4 method private back () = try @@ -1343,20 +1126,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `About `TeX -> self#tex () | `About `Grammar -> self#grammar () | `Check term -> self#_loadCheck term - | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `NCic (term, ctx, metasenv, subst) -> self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir - | `HBugs `Tutors -> self#_loadHBugsTutors - | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> - self#dependencies dir uri () - | `Uri uri -> self#_loadUriManagerUri uri - | `NRef nref -> self#_loadNReference nref - | `Univs uri -> self#_loadUnivs uri - | `Whelp (query, results) -> - set_whelp_query query; - self#_loadList (List.map (fun r -> "obj", - UriManager.string_of_uri r) results)); + | `NRef nref -> self#_loadNReference nref); self#setEntry entry end) @@ -1376,12 +1149,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) if Sys.command "which dot" = 0 then let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in let fmt = Format.formatter_of_out_channel oc in - MetadataDeps.DepGraph.render fmt gviz_graph; + (* MATITA 1.0 MetadataDeps.DepGraph.render fmt gviz_graph;*) close_out oc; gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile; (match center_on with | None -> () - | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri)); + | Some uri -> gviz#center_on_href (NReference.string_of_reference uri)); HExtlib.safe_remove tmpfile else MatitaGtkMisc.report_error ~title:"graphviz error" @@ -1390,6 +1163,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ~parent:win#toplevel () method private dependencies direction uri () = + assert false (* MATITA 1.0 let dbd = LibraryDb.instance () in let graph = match direction with @@ -1397,7 +1171,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `Back -> MetadataDeps.DepGraph.inverse_deps ~dbd uri in gviz_graph <- graph; (** XXX check this for memory consuption *) self#redraw_gviz ~center_on:uri (); - self#_showGviz + self#_showGviz *) method private coerchgraph tred () = load_coerchgraph tred (); @@ -1444,53 +1218,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showSearch method private grammar () = - self#_loadText (Print_grammar.ebnf_of_term ()); + self#_loadText (Print_grammar.ebnf_of_term self#script#grafite_status); method private home () = self#_showMath; - match self#script#grafite_status#proof_status with - | Proof (uri, metasenv, _subst, bo, ty, attrs) -> - let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = - Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) - in - self#_loadObj obj - | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } -> - let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = - Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) - in - self#_loadObj obj - | _ -> - match self#script#grafite_status#ng_mode with - `ProofMode -> - self#_loadNObj self#script#grafite_status - self#script#grafite_status#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 + match self#script#grafite_status#ng_mode with + `ProofMode -> + self#_loadNObj self#script#grafite_status + self#script#grafite_status#obj + | _ -> self#blank () method private _loadNReference (NReference.Ref (uri,_)) = let obj = NCicEnvironment.get_checked_obj uri in self#_loadNObj self#script#grafite_status obj - method private _loadUnivs uri = - let uri = UriManager.strip_xpointer uri in - let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - let _,us = CicUniv.do_rank u in - let l = - List.map - (fun u -> - [ CicUniv.string_of_universe u ; string_of_int (CicUniv.get_rank u)]) - us - in - self#_loadList2 l - method private _loadDir dir = let content = Http_getter.ls ~local:false dir in let l = @@ -1505,20 +1246,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) lastDir <- dir; self#_loadList l - method private _loadHBugsTutors = - self#_showHBugs - method private setEntry entry = win#browserUri#set_text (MatitaTypes.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 _loadNObj status obj = (* showMath must be done _before_ loading the document, since if the * widget is not mapped (hidden by the notebook) the document is not @@ -1526,13 +1257,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_nobject status 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 _loadTermNCic term m s c = let d = 0 in let m = (0,([],c,term))::m in @@ -1557,14 +1281,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** this is what the browser does when you enter a string an hit enter *) method loadInput txt = - let parse_metadata s = - let subs = Pcre.extract ~rex:metadata_RE s in - let uri = UriManager.uri_of_string ("cic:/" ^ subs.(3)) in - match subs.(1), subs.(2) with - | "deps", "forward" -> `Deps (`Fwd, uri) - | "deps", "backward" -> `Deps (`Back, uri) - | _ -> assert false - in let txt = HExtlib.trim_blanks txt in (* (* ZACK: what the heck? *) let fix_uri txt = @@ -1572,17 +1288,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (UriManager.strip_xpointer (UriManager.uri_of_string txt)) in *) - if is_whelp txt then begin - set_whelp_query txt; - (MatitaScript.current ())#advance ~statement:(txt ^ ".") () - end else begin let entry = match txt with | txt when is_uri txt -> - `Uri (UriManager.uri_of_string ((*fix_uri*) txt)) + `NRef (NReference.reference_of_string ((*fix_uri*) txt)) | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) - | txt when is_metadata txt -> `Metadata (parse_metadata txt) - | "hbugs:/tutors/" -> `HBugs `Tutors | txt -> (try MatitaTypes.entry_of_string txt @@ -1592,7 +1302,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in self#_load entry; self#_historyAdd entry - end (** {2 methods accessing underlying GtkMathView} *)