added gzip to log files

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index 5d22f85d579f8aa9f15b2e1e27a7ab061f1e8f5c..3c5bf8441555a33c98bd54d273616c4b018be067 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -149,6 +149,17 @@ 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 "ask record choice"
       (fun _ ->
         HLog.debug (string_of_int
@@ -170,6 +181,11 @@ 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);
     addDebugItem "disable coercions hiding"