X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=f00ea1a0fe89be0f6859ce7d91141579f5314534;hb=779859f7a9e317e378d258897c289f447adea7ad;hp=9c259a1cbdc58297d902974a20b8caa77014e8e5;hpb=a970a6b5d44947e466b94ff3df4fa66d85d0d9ca;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 9c259a1cb..f00ea1a0f 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -629,6 +629,27 @@ object (self) end; self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); + + method load_nobject obj = + let mathml = ApplyTransformation.nmml_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 let tab_label meta_markup = @@ -777,9 +798,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal (Some (goal_of_switch goal_switch)); self#render_page ~page ~goal_switch)) - method nload_sequents - { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack } - = + method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit + = fun status -> + let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; let win goal_switch = @@ -804,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = w#coerce in assert ( - let stack_goals = Stack.open_goals stack in + let stack_goals = Stack.open_goals status#stack in let proof_goals = List.map fst metasenv in if HExtlib.list_uniq (List.sort Pervasives.compare stack_goals) @@ -842,13 +863,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 -> + | 1, pos when Stack.head_tag status#stack = `BranchTag -> `Shift (pos, render_switch sw) | _ -> render_switch sw in add_tab markup sw) ~cont:add_switch ~todo:add_switch - stack; + status#stack; switch_page_callback <- Some (notebook#connect#switch_page ~callback:(fun page -> let goal_switch = @@ -1064,7 +1085,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 () -> - self#load (`Uri (UriManager.uri_of_string uri))))); + let uri = + try + `Uri (UriManager.uri_of_string uri) + with + UriManager.IllFormedUri _ -> + `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 @@ -1214,6 +1242,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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; @@ -1306,16 +1335,23 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private home () = self#_showMath; - match self#script#grafite_status.proof_status with + 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 + 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 + 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 - | _ -> self#blank () + | _ -> + match self#script#grafite_status#ng_mode with + `ProofMode -> self#_loadNObj self#script#grafite_status#obj + | _ -> self#blank () (** loads a cic uri from the environment * @param uri UriManager.uri *) @@ -1324,6 +1360,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 obj + method private _loadUnivs uri = let uri = UriManager.strip_xpointer uri in let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -1364,6 +1404,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_object obj + method private _loadNObj 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_nobject obj + method private _loadTermCic term metasenv = let context = self#script#proofContext in let dummyno = CicMkImplicit.new_meta metasenv [] in