X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=255998c4f436884ab1e105136577bcb79528cf0c;hb=156e5aad803c661dc2967b8f33642e89e8e878a1;hp=9c259a1cbdc58297d902974a20b8caa77014e8e5;hpb=a970a6b5d44947e466b94ff3df4fa66d85d0d9ca;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 9c259a1cb..255998c4f 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -593,10 +593,14 @@ object (self)
     end;
     self#load_root ~root:mathml#get_documentElement
 
-  method nload_sequent metasenv subst metano =
+  method nload_sequent:
+   'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
+     NCic.substitution -> int -> unit
+   = fun status metasenv subst metano ->
     let sequent = List.assoc metano metasenv in
     let mathml =
-     ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
+     ApplyTransformation.nmml_of_cic_sequent status metasenv subst
+      (metano,sequent)
     in
     if BuildTimeConf.debug then begin
       let name =
@@ -629,6 +633,29 @@ object (self)
         end;
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);
+
+  method load_nobject :
+   'status. #NCicCoercion.status as 'status -> NCic.obj -> unit
+   = fun status obj ->
+    let mathml = ApplyTransformation.nmml_of_cic_object status 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 =
@@ -697,9 +724,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- `Old []; 
       self#script#setGoal None
 
-    method load_sequents 
-      { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
-    =
+    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 =
@@ -775,11 +802,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
             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))
+          self#render_page status ~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 +831,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,27 +869,31 @@ 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 =
             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))
+          self#render_page status ~page ~goal_switch))
 
-    method private render_page ~page ~goal_switch =
+    method private render_page:
+     'status. #NCicCoercion.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
-           | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal)
+           | `New (menv,subst) ->
+               cicMathView#nload_sequent status menv subst goal)
       | Stack.Closed goal ->
           let doc = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root:doc#get_documentElement);
@@ -871,7 +902,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         List.assoc goal_switch goal2win ()
       with Not_found -> assert false)
 
-    method goto_sequent goal =
+    method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit
+     = fun status goal ->
       let goal_switch, page =
         try
           List.find
@@ -880,7 +912,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         with Not_found -> assert false
       in
       notebook#goto_page page;
-      self#render_page page goal_switch
+      self#render_page status ~page ~goal_switch
 
   end
 
@@ -1064,7 +1096,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 +1253,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 +1346,25 @@ 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
+             self#script#grafite_status#obj
+         | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)
@@ -1324,6 +1373,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 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
@@ -1364,6 +1417,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       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
+       * rendered *)
+      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