X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=9990805ad7614ce2ab407700bb8f27363a3ae2d5;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=3f538ac4571b08d3dd185abfec2edb20eefcc6ce;hpb=f03ff6e69b44a4e89b92b21251cce9d247c4a4e4;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 3f538ac45..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 @@ -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) @@ -205,7 +211,8 @@ object (self) 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#source_buffer#set_highlight_syntax true; + self#set_editable false (* MATITA1.0 inherit GMathViewAux.multi_selection_math_view obj @@ -612,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 @@ -650,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 @@ -767,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; @@ -928,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 -> @@ -945,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 @@ -1008,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 ] @@ -1103,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 @@ -1122,10 +995,7 @@ 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 () @@ -1151,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 | _ -> ()); @@ -1172,39 +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 -> ()); - - (* 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 () @@ -1214,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 = @@ -1265,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 @@ -1294,14 +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 - | `Uri uri -> self#_loadUriManagerUri uri - | `NRef nref -> self#_loadNReference nref - | `Univs uri -> self#_loadUnivs uri); + | `NRef nref -> self#_loadNReference nref); self#setEntry entry end) @@ -1321,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" @@ -1335,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 @@ -1342,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 (); @@ -1389,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 = @@ -1450,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 @@ -1471,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 @@ -1512,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