X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=f418abe6f8e658dc3b78eadc9610b9ed380a865a;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=5881c6d832b8c0730c71f17b9ba5bc048d161d0d;hpb=907f919aba0f21b18acff8a8e1c266ab92d10baf;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 5881c6d83..f418abe6f 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 @@ -187,17 +193,17 @@ object (self) 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) @@ -613,27 +619,6 @@ 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 -> NCic.substitution -> int -> unit @@ -651,32 +636,6 @@ 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 = fun status obj -> @@ -855,7 +814,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = (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 -> @@ -929,7 +888,7 @@ let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = - [ `Ast of CicNotationPt.term + [ `Ast of NotationPt.term | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `String of string ] @@ -1036,8 +995,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) object (self) inherit scriptAccessor - 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 () @@ -1063,20 +1021,14 @@ 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 | _ -> ()); @@ -1092,31 +1044,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 () @@ -1126,7 +1053,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 -> Some uri + | `NRef uri -> Some uri | _ -> None val model = @@ -1210,9 +1137,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir | `HBugs `Tutors -> self#_loadHBugsTutors - | `Uri uri -> self#_loadUriManagerUri uri - | `NRef nref -> self#_loadNReference nref - | `Univs uri -> self#_loadUnivs uri); + | `NRef nref -> self#_loadNReference nref); self#setEntry entry end) @@ -1232,12 +1157,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" @@ -1246,6 +1171,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 @@ -1253,7 +1179,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 (); @@ -1310,29 +1236,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 - 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 = @@ -1354,13 +1261,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 @@ -1402,7 +1302,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 -> (try