X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=a70063f5fe19508501f0609ab22d7da6927e4078;hb=3fa45cd94f60af6b221a10ac198e2a1cf17b041d;hp=5d22f85d579f8aa9f15b2e1e27a7ab061f1e8f5c;hpb=48b1c073868dcddf01140775cb0e5ac524fdbf14;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5d22f85d5..a70063f5f 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -149,6 +149,31 @@ let _ =
             (MatitaScript.current ())#proofMetasenv));
         prerr_endline ("stack: " ^ Continuationals.Stack.pp
           (GrafiteTypes.get_stack (MatitaScript.current ())#grafite_status)));
+     addDebugItem "Print current proof term" 
+       (fun _ -> 
+        HLog.debug
+          (CicPp.ppterm 
+            (match 
+            (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+            with
+            | GrafiteTypes.No_proof -> (Cic.Implicit None)
+            | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,p,_ = p in p
+            | Intermediate _ -> assert false)));
+     addDebugItem "Print current proof (natural language) to stderr" 
+       (fun _ -> 
+        prerr_endline 
+          (ObjPp.obj_to_string 120 
+            (match 
+            (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+            with
+            | GrafiteTypes.No_proof -> assert false
+            | Incomplete_proof i -> 
+                let _,m,p,ty = i.GrafiteTypes.proof in 
+                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[])
+            | Proof (_,m,p,ty) -> 
+                Cic.CurrentProof ("current proof",m,p,ty,[],[])
+            | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
       (fun _ ->
         HLog.debug (string_of_int
@@ -170,27 +195,25 @@ let _ =
         CicNotation.set_active_notations
           (List.map fst (CicNotation.get_all_notations ())));
     addDebugSeparator ();
+    addDebugItem "enable multiple disambiguation passes (default)"
+      (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+    addDebugItem "enable only one disambiguation pass"
+      (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+    addDebugSeparator ();
     addDebugItem "enable coercions hiding"
-      (fun _ -> TermAcicContent.hide_coercions := true);
+      (fun _ -> Acic2content.hide_coercions := true);
     addDebugItem "disable coercions hiding"
-      (fun _ -> TermAcicContent.hide_coercions := false);
+      (fun _ -> Acic2content.hide_coercions := false);
+    addDebugItem "show coercions graph" (fun _ ->
+      let c = MatitaMathView.cicBrowser () in
+      c#load (`About `Coercions));
     addDebugItem "dump coercions Db" (fun _ ->
       List.iter
-        (fun (s,t,u) -> 
+      (fun (s,t,ul) -> 
           HLog.debug
-            (UriManager.name_of_uri u ^ ":"
+           ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":"
              ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
         (CoercDb.to_list ()));
-    addDebugItem "show coercions graph" (fun _ ->
-      let str = CoercGraph.generate_dot_file () in
-      let filename, oc = Filename.open_temp_file "xx" ".dot" in
-      output_string oc str;
-      close_out oc;
-      let ps = Filename.temp_file "yy" ".png" in
-      ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
-      ignore (Unix.system ("/usr/bin/display " ^ ps));
-      Sys.remove ps;
-      Sys.remove filename);
     addDebugSeparator ();
     let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
 (*     addDebugItem "save (sequent) MathML to matita.xml"
@@ -229,6 +252,18 @@ let _ =
   end;
   try
     GtkThread.main ()
-  with Sys.Break -> ()
+  with Sys.Break ->
+   Sys.set_signal Sys.sigint
+    (Sys.Signal_handle
+      (fun _ ->
+        prerr_endline "Still cleaning the library: don't be impatient!"));
+   prerr_endline "Matita is cleaning up. Please wait.";
+   try
+    let baseuri =
+     GrafiteTypes.get_string_option
+      (MatitaScript.current ())#grafite_status "baseuri"
+    in
+     LibraryClean.clean_baseuris [baseuri]
+   with GrafiteTypes.Option_error _ -> ()
 
 (* vim:set foldmethod=marker: *)