snapshot

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index fad12b563772db8166e0c850c46fae22402211b2..7c9502bd414cc89b674d00a1d216a77baf8b4610 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -115,7 +115,8 @@ let proof_handler =
 
 let interpreter =
   let console = gui#console in
-  new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
+  new MatitaInterpreter.interpreter
+    ~disambiguator ~proof_handler ~console ~dbd ()
 
 (** {2 Script window handling} *)
 
@@ -137,8 +138,7 @@ let script_jump _ =
   let rec parse offset =
     if offset < len then begin
       if
-        interpreter#evalPhrase ~transparent:true
-          (String.sub raw_text offset (len - offset));
+        interpreter#evalPhrase (String.sub raw_text offset (len - offset))
       then begin
         let new_offset = interpreter#endOffset + offset in
         gui#lockScript (new_offset + locked_iter#offset);
@@ -164,8 +164,9 @@ let _ =
   gui#setQuitCallback quit;
   gui#setPhraseCallback interpreter#evalPhrase;
   gui#main#debugMenu#misc#hide ();
-  ignore (gui#main#newProofMenuItem#connect#activate
-    (gui#console#show ~msg:"theorem "));
+  ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+    gui#console#clear ();
+    gui#console#show ~msg:"theorem " ()));
   ignore (gui#main#openMenuItem#connect#activate (fun _ ->
     match gui#chooseFile () with
     | None -> ()
@@ -198,6 +199,9 @@ let _ =
   connect_button tbar#reflexivityButton (tac A.Reflexivity);
   connect_button tbar#symmetryButton (tac A.Symmetry);
   connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
+
+(*   connect_button tbar#simplifyButton FINQUI; *)
+
   connect_button tbar#assumptionButton (tac A.Assumption);
   connect_button tbar#cutButton (tac_w_term (A.Cut hole));
   connect_button tbar#autoButton (tac A.Auto)
@@ -218,8 +222,11 @@ let _ =
         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
     addDebugItem "dump proof status to stdout" (fun _ ->
       print_endline ((get_proof ())#toString));
-    addDebugItem "hide console" gui#console#hide;
-    addDebugItem "show console" gui#console#show;
+    addDebugItem "print selected terms" (fun () ->
+      let i = ref 0 in
+      List.iter
+        (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
+        sequent_viewer#get_selected_terms)
   end
 
   (** </DEBUGGING> *)