X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FmatitaMathView.ml;h=9990805ad7614ce2ab407700bb8f27363a3ae2d5;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=71e7cb55334540bbbf61640ecf5b2f2d4b5fcec7;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 71e7cb553..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,13 +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 ( - domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ()) +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 @@ -129,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 *) @@ -176,10 +180,41 @@ let rec has_maction (elt :Gdome.element) = has_maction (new Gdome.element_of_node node) | _ -> false ;; +*) class clickableMathView obj = let text_width = 80 in object (self) + inherit GSourceView2.source_view obj + + method has_selection = (assert false : bool) + method strings_of_selection = (assert false : (paste_kind * string) list) + 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 _ -> () : 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) + (* 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 _ -> () : 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 val mutable href_callback: (string -> unit) option = None @@ -557,16 +592,26 @@ IDIOTA: PRIMA SI FA LA LOCATE, POI LA PATTERN_OF. MEGLIO UN'UNICA pattern_of CHE paste_kind, HExtlib.unopt (self#string_of_selection ~paste_kind)) [ `Term; `Pattern ] with Failure _ -> failwith "no selection" - +*) end +open GtkSourceView2 + let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = + SourceView.make_params [] ~cont:( + GtkText.View.make_params ~cont:( + GContainer.pack_container ~create:(fun pl -> + let obj = SourceView.new_ () in + Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl; + new clickableMathView obj))) + (* MATITA1.0 GtkBase.Widget.size_params - ~cont:(OgtkMathViewProps.pack_return (fun p -> - OgtkMathViewProps.set_params - (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~cont:(OgtkSourceView2Props.pack_return (fun p -> + OgtkSourceView2Props.set_params + (new clickableMathView (GtkSourceView2Props.MathView_GMetaDOM.create p)) ~font_size:None ~log_verbosity:None)) [] + *) class cicMathView obj = object (self) @@ -574,70 +619,28 @@ object (self) val mutable current_mathml = None - method load_sequent metasenv metano = - let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml, unsh_sequent, - (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) - = - ApplyTransformation.mml_of_cic_sequent 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)); - 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:mathml ()) - end; - self#load_root ~root:mathml#get_documentElement - 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 - let mathml = - ApplyTransformation.nmml_of_cic_sequent status metasenv subst - (metano,sequent) + let txt = + ApplyTransformation.ntxt_of_cic_sequent + ~map_unicode_to_tex:false 80 status metasenv subst (metano,sequent) in - if BuildTimeConf.debug then begin + (* 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:mathml ()) - end; - 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 (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 -> - self#freeze; - XmlDiff.update_dom ~from:current_mathml mathml; - self#thaw - | _ -> - 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:mathml#get_documentElement; - current_mathml <- Some mathml); + end;*) + self#load_root ~root:txt method load_nobject : - 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit + 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit = fun status obj -> - let mathml = ApplyTransformation.nmml_of_cic_object status obj in + let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false + 80 status obj in (* self#set_cic_info (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); @@ -648,13 +651,13 @@ object (self) self#thaw | _ -> *) - if BuildTimeConf.debug then begin + (* 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:mathml#get_documentElement; + end;*) + self#load_root ~root:txt; (*current_mathml <- Some mathml*)(*)*); end @@ -724,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; @@ -885,24 +808,24 @@ 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 -> let doc = Lazy.force closed_goal_mathml in - cicMathView#load_root ~root:doc#get_documentElement); + cicMathView#load_root ~root:doc); (try cicMathView#set_selection None; 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 @@ -917,33 +840,55 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 + ?hadjustment:GData.adjustment -> + ?vadjustment:GData.adjustment -> + ?font_size:int -> + ?log_verbosity:int -> + ?auto_indent:bool -> + ?highlight_current_line:bool -> + ?indent_on_tab:bool -> + ?indent_width:int -> + ?insert_spaces_instead_of_tabs:bool -> + ?right_margin_position:int -> + ?show_line_marks:bool -> + ?show_line_numbers:bool -> + ?show_right_margin:bool -> + ?smart_home_end:SourceView2Enums.source_smart_home_end_type -> + ?tab_width:int -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?accepts_tab:bool -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> unit -> + 'widget let cicMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = + SourceView.make_params [] ~cont:( + GtkText.View.make_params ~cont:( + GContainer.pack_container ~create:(fun pl -> + let obj = SourceView.new_ () in + Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl; + new cicMathView obj))) +(* MATITA 1.0 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 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 ] @@ -951,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 @@ -1003,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 = @@ -1065,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 @@ -1084,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; @@ -1132,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 () @@ -1203,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 = @@ -1255,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 @@ -1284,26 +1126,16 @@ 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) method private blank () = self#_showMath; - mathView#load_root (Lazy.force empty_mathml)#get_documentElement + mathView#load_root "" method private _loadCheck term = failwith "not implemented _loadCheck"; @@ -1317,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" @@ -1331,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 @@ -1338,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 (); @@ -1385,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 = @@ -1446,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 @@ -1467,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 @@ -1498,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 = @@ -1513,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 @@ -1533,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} *) @@ -1601,6 +1369,7 @@ let mathViewer () = (self#get_browser reuse)#load entry method screenshot status sequents metasenv subst (filename as ofn) = + () (*MATITA 1.0 let w = GWindow.window ~title:"screenshot" () in let width = 500 in let height = 2000 in @@ -1659,6 +1428,7 @@ let mathViewer () = List.iter (fun x,_ -> Sys.remove x) filenames; List.iter Sys.remove (List.flatten items); w#destroy (); + *) end let refresh_all_browsers () =