Added a new section on the logical library.

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 710efdf021a118aada8820ede5c009b242a11495..b637eb8dc37b9b7a06bb547ecb63fa5f8bae4445 100644 (file)
--- 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
@@ -328,9 +328,9 @@ object (self)
       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
@@ -341,7 +341,7 @@ object (self)
       | Some ((None, _, _, _, _, _) as info) ->
           (* building a dummy sequent for obj *)
           let t = self#find_obj_conclusion id in
-          MatitaLog.debug (CicPp.ppterm t);
+          HLog.debug (CicPp.ppterm t);
           info, (~-1, [], t)
       | None -> assert false
     in
@@ -397,7 +397,7 @@ object (self)
         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
 
@@ -417,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);
@@ -613,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
   ]
@@ -672,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
@@ -849,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 =
@@ -892,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