X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita.ml;h=1645184264b6e446f35b196da1aae353daa7b1df;hb=ca160266c4955d0cbdb66e1a24f2239e2839e215;hp=2cbb9a9a1350cd2303712637c3705d42c22e21e3;hpb=1ac56131763867ef875c1ec8d09a1be088dc7080;p=helm.git

diff --git a/matita/matita.ml b/matita/matita.ml
index 2cbb9a9a1..164518426 100644
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -103,9 +103,10 @@ let _ =
     gui#main#debugMenu#misc#show ();
     let addDebugItem ~label callback =
       let item =
-        GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
-      in
-      ignore (item#connect#activate callback)
+        GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label () in
+      ignore (item#connect#activate callback) in
+    let addDebugSeparator () =
+      ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
       let oc = open_out "env.dump" in
@@ -124,9 +125,6 @@ let _ =
       List.iter (fun (u,_,_) -> 
         prerr_endline (UriManager.string_of_uri u)) 
         (CicEnvironment.list_obj ()));
-(*     addDebugItem "print selections" (fun () ->
-      let cicMathView = MatitaMathView.cicMathView_instance () in
-      List.iter HLog.debug (cicMathView#string_of_selections)); *)
     addDebugItem "dump script status" script#dump;
     addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
       Helm_registry.save_to "./foo.conf.xml");
@@ -134,24 +132,6 @@ let _ =
       (fun _ ->
          if script#onGoingProof () then
            HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
-    addDebugItem "dump coercions Db" (fun _ ->
-      List.iter
-        (fun (s,t,u) -> 
-          HLog.debug
-            (UriManager.name_of_uri u ^ ":"
-             ^ 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);
-        
     addDebugItem "print top-level grammar entries"
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
@@ -169,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
@@ -178,19 +183,44 @@ let _ =
             ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"];
             ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]]
           ()))); *)
-    addDebugItem "rotate light bulbs"
+(*     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in
-         nb#goto_page ((nb#current_page + 1) mod 3));
-    addDebugItem "print runtime dir"
-      (fun _ ->
-        prerr_endline BuildTimeConf.runtime_base_dir);
+         nb#goto_page ((nb#current_page + 1) mod 3)); *)
+    addDebugSeparator ();
     addDebugItem "disable all (pretty printing) notations"
       (fun _ -> CicNotation.set_active_notations []);
     addDebugItem "enable all (pretty printing) notations"
       (fun _ ->
         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 _ -> Acic2content.hide_coercions := true);
+    addDebugItem "disable coercions hiding"
+      (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,ul) -> 
+          HLog.debug
+           ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":"
+             ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
+        (CoercDb.to_list ()));
+    addDebugSeparator ();
+    let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
+(*     addDebugItem "save (sequent) MathML to matita.xml"
+      (fun _ -> ignore ((Gdome.domImplementation ())#saveDocumentToFile
+        ~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *)
+    addDebugItem "load (sequent) MathML from matita.xml"
+      (fun _ -> (mview ())#load_uri ~filename:"matita.xml");
   end
   (** Debugging }}} *)