X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=9990805ad7614ce2ab407700bb8f27363a3ae2d5;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=4b9fa4646f4b3655c2b3f0a155f728c51a7c6843;hpb=bfcde2b08d72f1392ed61164c67d199360f0397f;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 4b9fa4646..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,10 +84,12 @@ 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 @@ -177,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 @@ -189,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) @@ -616,7 +620,7 @@ object (self) val mutable current_mathml = None 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 @@ -633,7 +637,7 @@ object (self) 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 txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -723,8 +727,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- `Old []; self#script#setGoal None - 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; @@ -804,7 +808,7 @@ 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 @@ -821,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 @@ -884,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 ] @@ -991,7 +995,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) object (self) inherit scriptAccessor - 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 () @@ -1017,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 | _ -> ()); @@ -1038,18 +1036,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 -> ()); self#_load (`About `Blank); toplevel#show () @@ -1059,7 +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 -> Some uri + | `NRef uri -> Some uri | _ -> None val model = @@ -1110,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 @@ -1142,10 +1129,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `NCic (term, ctx, metasenv, subst) -> self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir - | `HBugs `Tutors -> self#_loadHBugsTutors - | `Uri uri -> assert false (* MATITA 1.0 *) - | `NRef nref -> self#_loadNReference nref - | `Univs uri -> assert false (* MATITA 1.0 *)); + | `NRef nref -> self#_loadNReference nref); self#setEntry entry end) @@ -1170,7 +1154,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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" @@ -1234,7 +1218,7 @@ 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; @@ -1262,9 +1246,6 @@ 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 @@ -1310,7 +1291,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