Coercion hiding implemented. Notes:

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index f00ea1a0fe89be0f6859ce7d91141579f5314534..255998c4f436884ab1e105136577bcb79528cf0c 100644 (file)
--- 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 =
@@ -630,8 +634,10 @@ object (self)
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);
 
-  method load_nobject obj =
-    let mathml = ApplyTransformation.nmml_of_cic_object obj in
+  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));
@@ -718,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 =
@@ -796,7 +802,7 @@ 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 : 'status. #NTacStatus.tac_status as 'status -> unit
     = fun status ->
@@ -876,14 +882,18 @@ 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 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);
@@ -892,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
@@ -901,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
 
@@ -1350,7 +1361,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           self#_loadObj obj
       | _ ->
         match self#script#grafite_status#ng_mode with
-           `ProofMode -> self#_loadNObj self#script#grafite_status#obj
+           `ProofMode ->
+             self#_loadNObj self#script#grafite_status
+             self#script#grafite_status#obj
          | _ -> self#blank ()
 
       (** loads a cic uri from the environment
@@ -1362,7 +1375,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private _loadNReference (NReference.Ref (uri,_)) =
       let obj = NCicEnvironment.get_checked_obj uri in
-      self#_loadNObj obj
+      self#_loadNObj self#script#grafite_status obj
 
     method private _loadUnivs uri =
       let uri = UriManager.strip_xpointer uri in
@@ -1404,12 +1417,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       mathView#load_object obj
 
-    method private _loadNObj 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 obj
+      mathView#load_nobject status obj
 
     method private _loadTermCic term metasenv =
       let context = self#script#proofContext in