Huge commit with several changes:

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 9c259a1cbdc58297d902974a20b8caa77014e8e5..ade02fb8087cb377f604810c9f805f4d6cb827f5 100644 (file)
--- 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 =
@@ -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;
@@ -1324,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
@@ -1364,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