X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=710efdf021a118aada8820ede5c009b242a11495;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=1ad4b2cd10a79dd14348b67d157d4b4b7552beab;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1ad4b2cd1..710efdf02 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -62,9 +62,27 @@ let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in (distance < 4.) +let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" +let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" let href_ds = Gdome.domString "href" let xref_ds = Gdome.domString "xref" +let domImpl = Gdome.domImplementation () + + (** Gdome.element of a MathML document whose rendering should be blank. Used + * by cicBrowser to render "about:blank" document *) +let empty_mathml = lazy ( + domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None) + +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 ()) + (* 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 = let find_parent id ids = @@ -190,11 +208,11 @@ object (self) (match self#get_element_at x y with | None -> () | Some elt -> - let namespaceURI = DomMisc.xlink_ns in let localName = href_ds in - if elt#hasAttributeNS ~namespaceURI ~localName then + if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then self#invoke_href_callback - (elt#getAttributeNS ~namespaceURI ~localName)#to_string + (elt#getAttributeNS ~namespaceURI:xlink_ns + ~localName)#to_string gdk_button else ignore (self#action_toggle elt)); @@ -231,7 +249,7 @@ object (self) ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) in let rec aux elt = - if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns + if (elt#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds)#to_string <> "" then set_selection elt @@ -243,7 +261,7 @@ object (self) with GdomeInit.DOMCastException _ -> () in (match gdome_elt with - | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns + | Some elt when (elt#getAttributeNS ~namespaceURI:xlink_ns ~localName:href_ds)#to_string <> "" -> set_selection elt | Some elt -> aux elt @@ -252,13 +270,18 @@ object (self) method update_font_size = self#set_font_size !current_font_size - method private get_term_by_id context cic_info id = - let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in + method private get_term_by_id cic_info id = + let unsh_item, ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in try `Term (Hashtbl.find ids_to_terms id) with Not_found -> try let hyp = Hashtbl.find ids_to_hypotheses id in + let _, context, _ = + match unsh_item with + | Some seq -> seq + | None -> assert false + in let context' = MatitaMisc.list_tl_at hyp context in `Hyp context' with Not_found -> assert false @@ -266,37 +289,32 @@ object (self) method private find_obj_conclusion id = match self#cic_info with | None - | Some (_, _, _, _, None) -> assert false - | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> + | Some (_, _, _, _, _, None) -> assert false + | Some (_, ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> let id = find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types in (try Hashtbl.find ids_to_terms id with Not_found -> assert false) method private string_of_node node = - if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds then self#string_of_id_node node else string_of_dom_node node method private string_of_id_node node = let get_id (node: Gdome.element) = let xref_attr = - node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds in List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) in let id = get_id node in let script = MatitaScript.current () in - let metasenv = script#proofMetasenv in - let context = script#proofContext in - let metasenv, context, conclusion = + let metasenv = if script#onGoingProof () then - script#proofMetasenv, script#proofContext, script#proofConclusion + script#proofMetasenv else - [], [], - let t = self#find_obj_conclusion id in - MatitaLog.debug (CicPp.ppterm t); - t + [] in (* TODO: code for patterns let conclusion = (MatitaScript.instance ())#proofConclusion in @@ -305,7 +323,7 @@ object (self) in *) let string_of_cic_sequent cic_sequent = - let acic_sequent, _, _, ids_to_inner_sorts, _ = + let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = Cic2acic.asequent_of_sequent metasenv cic_sequent in let _, _, _, annterm = acic_sequent in @@ -316,19 +334,27 @@ object (self) let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup in - let cic_info = - match self#cic_info with Some info -> info | None -> assert false + let cic_info, unsh_sequent = + match self#cic_info with + | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> + info, unsh_sequent + | Some ((None, _, _, _, _, _) as info) -> + (* building a dummy sequent for obj *) + let t = self#find_obj_conclusion id in + MatitaLog.debug (CicPp.ppterm t); + info, (~-1, [], t) + | None -> assert false in let cic_sequent = - match self#get_term_by_id context cic_info id with + match self#get_term_by_id cic_info id with | `Term t -> let context' = - match - ProofEngineHelpers.locate_in_conjecture t - (~-1, context, conclusion) - with + match ProofEngineHelpers.locate_in_conjecture t unsh_sequent with [context,_] -> context - | _ -> assert false (* since it uses physical equality *) + | _ -> +(* prerr_endline (sprintf "%d\nt=%s\ncontext=%s" + (List.length l) (CicPp.ppterm t) (CicPp.ppcontext context)); *) + assert false (* since it uses physical equality *) in ~-1, context', t | `Hyp context -> ~-1, context, Cic.Rel 1 @@ -361,15 +387,18 @@ object (self) method load_sequent metasenv metano = let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) = + 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 (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, + (Some (Some unsh_sequent, + ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement method load_object obj = @@ -380,7 +409,7 @@ object (self) ApplyTransformation.mml_of_cic_object obj in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); + (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; @@ -389,7 +418,7 @@ object (self) | _ -> let name = "cic_browser.xml" in MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); end @@ -519,7 +548,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = let markup = match depth, pos with | 0, _ -> `Current (render_switch sw) - | 1, pos when Stack.head_tag stack = Stack.BranchTag -> + | 1, pos when Stack.head_tag stack = `BranchTag -> `Shift (pos, render_switch sw) | _ -> render_switch sw in @@ -538,7 +567,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = (match goal_switch with | Stack.Open goal -> cicMathView#load_sequent _metasenv goal | Stack.Closed goal -> - let doc = Lazy.force MatitaMisc.closed_goal_mathml in + let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); (try cicMathView#set_selection None; @@ -775,8 +804,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private blank () = self#_showMath; - mathView#load_root - (Lazy.force MatitaMisc.empty_mathml)#get_documentElement + mathView#load_root (Lazy.force empty_mathml)#get_documentElement method private _loadCheck term = failwith "not implemented _loadCheck";