X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=b637eb8dc37b9b7a06bb547ecb63fa5f8bae4445;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=f9c617385a945e8a4facc9ee39517f6816729fc6;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f9c617385..b637eb8dc 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -25,7 +25,7 @@
 
 open Printf
 
-open MatitaTypes
+open GrafiteTypes
 open MatitaGtkMisc
 
 module Stack = Continuationals.Stack
@@ -270,13 +270,18 @@ object (self)
 
   method update_font_size = self#set_font_size !current_font_size
 
-  method private get_term_by_id context cic_info id =
-    let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in
+  method private get_term_by_id cic_info id =
+    let unsh_item, ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in
     try
       `Term (Hashtbl.find ids_to_terms id)
     with Not_found ->
       try
         let hyp = Hashtbl.find ids_to_hypotheses id in
+        let _, context, _ =
+          match unsh_item with
+          | Some seq -> seq
+          | None -> assert false
+        in
         let context' = MatitaMisc.list_tl_at hyp context in
         `Hyp context'
       with Not_found -> assert false
@@ -284,8 +289,8 @@ object (self)
   method private find_obj_conclusion id =
     match self#cic_info with
     | None
-    | Some (_, _, _, _, None) -> assert false
-    | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) ->
+    | Some (_, _, _, _, _, None) -> assert false
+    | Some (_, ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) ->
         let id =
          find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types
         in
@@ -305,16 +310,11 @@ object (self)
     in
     let id = get_id node in
     let script = MatitaScript.current () in
-    let metasenv = script#proofMetasenv in
-    let context = script#proofContext in
-    let metasenv, context, conclusion =
+    let metasenv =
       if script#onGoingProof () then
-        script#proofMetasenv, script#proofContext, script#proofConclusion
+        script#proofMetasenv
       else
-        [], [],
-        let t = self#find_obj_conclusion id in
-        MatitaLog.debug (CicPp.ppterm t);
-        t
+        []
     in
 (* TODO: code for patterns
     let conclusion = (MatitaScript.instance ())#proofConclusion in
@@ -323,30 +323,38 @@ object (self)
     in
 *)
     let string_of_cic_sequent cic_sequent =
-      let acic_sequent, _, _, ids_to_inner_sorts, _ =
+      let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
         Cic2acic.asequent_of_sequent metasenv cic_sequent
       in
       let _, _, _, annterm = acic_sequent in
       let ast, ids_to_uris =
-        CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
+        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
       in
-      let pped_ast = CicNotationRew.pp_ast ast in
+      let pped_ast = TermContentPres.pp_ast ast in
       let markup = CicNotationPres.render ids_to_uris pped_ast in
       BoxPp.render_to_string text_width markup
     in
-    let cic_info =
-      match self#cic_info with Some info -> info | None -> assert false
+    let cic_info, unsh_sequent =
+      match self#cic_info with
+      | Some ((Some unsh_sequent, _, _, _, _, _) as info) ->
+          info, unsh_sequent
+      | Some ((None, _, _, _, _, _) as info) ->
+          (* building a dummy sequent for obj *)
+          let t = self#find_obj_conclusion id in
+          HLog.debug (CicPp.ppterm t);
+          info, (~-1, [], t)
+      | None -> assert false
     in
     let cic_sequent =
-      match self#get_term_by_id context cic_info id with
+      match self#get_term_by_id cic_info id with
       | `Term t ->
           let context' =
-            match
-              ProofEngineHelpers.locate_in_conjecture t
-                (~-1, context, conclusion)
-            with
+            match ProofEngineHelpers.locate_in_conjecture t unsh_sequent with
               [context,_] -> context
-            | _ -> assert false (* since it uses physical equality *)
+            | _ ->
+(*                 prerr_endline (sprintf "%d\nt=%s\ncontext=%s"
+                  (List.length l) (CicPp.ppterm t) (CicPp.ppcontext context)); *)
+                assert false (* since it uses physical equality *)
           in
           ~-1, context', t
       | `Hyp context -> ~-1, context, Cic.Rel 1
@@ -379,14 +387,17 @@ object (self)
 
   method load_sequent metasenv metano =
     let sequent = CicUtil.lookup_meta metano metasenv in
-    let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) =
+    let (mathml, unsh_sequent,
+      (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ )))
+    =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     self#set_cic_info
-      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
+      (Some (Some unsh_sequent,
+        ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
         Hashtbl.create 1, None));
     let name = "sequent_viewer.xml" in
-    MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+    HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
     ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
 
@@ -398,7 +409,7 @@ object (self)
       ApplyTransformation.mml_of_cic_object obj
     in
     self#set_cic_info
-      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
+      (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;
@@ -406,7 +417,7 @@ object (self)
         self#thaw
     |  _ ->
         let name = "cic_browser.xml" in
-        MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+        HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
         ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);
@@ -602,7 +613,7 @@ let blank_uri = BuildTimeConf.blank_uri
 let current_proof_uri = BuildTimeConf.current_proof_uri
 
 type term_source =
-  [ `Ast of DisambiguateTypes.term
+  [ `Ast of CicNotationPt.term
   | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]
@@ -661,7 +672,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       f ()
     with exn ->
       if not (Helm_registry.get_bool "matita.debug") then
-        fail (MatitaExcPp.to_string exn)
+        fail (snd (MatitaExcPp.to_string exn))
       else raise exn
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
@@ -838,7 +849,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_loadList l
 
     method private setEntry entry =
-      win#browserUri#entry#set_text (string_of_entry entry);
+      win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
       current_entry <- entry
 
     method private _loadObj obj =
@@ -881,10 +892,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
           | txt ->
-              (try
-                entry_of_string txt
+             (try
+               MatitaTypes.entry_of_string txt
               with Invalid_argument _ ->
-                command_error (sprintf "unsupported uri: %s" txt))
+               raise
+                (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
         in
         self#_load entry;
         self#_historyAdd entry