X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=ade02fb8087cb377f604810c9f805f4d6cb827f5;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=19eeaf0d7743d7f8788e703c5f0f595ce1fb2fbd;hpb=8d961585c4ff785d558d5b4c84adf656595ca487;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 19eeaf0d7..ade02fb80 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -167,7 +167,8 @@ let hrefs_of_elt elt = let rec has_maction (elt :Gdome.element) = (* fix this comparison *) - if elt#get_tagName#to_string = "m:maction" then + if elt#get_tagName#to_string = "m:maction" || + elt#get_tagName#to_string = "b:action" then true else match elt#get_parentNode with @@ -592,6 +593,19 @@ object (self) end; self#load_root ~root:mathml#get_documentElement + method nload_sequent metasenv subst metano = + let sequent = List.assoc metano metasenv in + let mathml = + ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent) + in + 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:mathml ()) + end; + self#load_root ~root:mathml#get_documentElement + method load_object obj = let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) let (mathml, @@ -615,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 = @@ -641,7 +676,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) - val mutable _metasenv = [] + val mutable _metasenv = `Old [] val mutable scrolledWin: GBin.scrolled_window option = None (* scrolled window to which the sequentViewer is currently attached *) val logo = (GMisc.image @@ -680,13 +715,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- []; + _metasenv <- `Old []; self#script#setGoal None method load_sequents { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } = - _metasenv <- metasenv; + _metasenv <- `Old metasenv; pages <- 0; let win goal_switch = let w = @@ -763,9 +798,92 @@ 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 } + = + _metasenv <- `New (metasenv,subst); + 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 = List.map fst metasenv 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 ~page ~goal_switch)) + method private render_page ~page ~goal_switch = (match goal_switch with - | Stack.Open goal -> cicMathView#load_sequent _metasenv goal + | Stack.Open goal -> + (match _metasenv with + `Old menv -> cicMathView#load_sequent menv goal + | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal) | Stack.Closed goal -> let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); @@ -967,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 @@ -1117,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; @@ -1227,6 +1353,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 @@ -1267,6 +1397,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