X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.ml;h=99fa10acbf769c5c719bbc7e5852348e7d38e749;hb=83d2e9c93f39464715e10fab6ebdb4be97c37b08;hp=4fdc704e220a8593610a18635bf9f72a37304e23;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index 4fdc704e2..99fa10acb 100644
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -93,11 +93,12 @@ let _ =
   let browser_observer _ = MatitaMathView.refresh_all_browsers () in
   let sequents_observer grafite_status =
     sequents_viewer#reset;
-    match grafite_status#proof_status with
-    | Incomplete_proof ({ stack = stack } as incomplete_proof) ->
-        sequents_viewer#load_sequents grafite_status incomplete_proof;
+    match grafite_status#ng_mode with
+       `ProofMode ->
+        sequents_viewer#nload_sequents grafite_status;
         (try
-          script#setGoal (Some (Continuationals.Stack.find_goal stack));
+          script#setGoal
+           (Some (Continuationals.Stack.find_goal grafite_status#stack));
           let goal =
            match script#goal with
               None -> assert false
@@ -105,24 +106,7 @@ let _ =
           in
            sequents_viewer#goto_sequent grafite_status goal
         with Failure _ -> script#setGoal None);
-    | Proof proof -> sequents_viewer#load_logo_with_qed
-    | No_proof ->
-       (match grafite_status#ng_mode with
-           `ProofMode ->
-            sequents_viewer#nload_sequents grafite_status;
-            (try
-              script#setGoal
-               (Some (Continuationals.Stack.find_goal grafite_status#stack));
-              let goal =
-               match script#goal with
-                  None -> assert false
-                | Some n -> n
-              in
-               sequents_viewer#goto_sequent grafite_status goal
-            with Failure _ -> script#setGoal None);
-         | `CommandMode -> sequents_viewer#load_logo
-       )
-    | Intermediate _ -> assert false (* only the engine may be in this state *)
+     | `CommandMode -> sequents_viewer#load_logo
   in
   script#addObserver sequents_observer;
   script#addObserver browser_observer
@@ -162,45 +146,9 @@ let _ =
          (fun x l -> (LexiconAstPp.pp_command x)::l)
          (filter status.LexiconEngine.lexicon_content_rev) [])));
 *)
-    addDebugItem "print metasenv goals and stack to stderr"
-      (fun _ ->
-        prerr_endline ("metasenv goals: " ^ String.concat " "
-          (List.map (fun (g, _, _) -> string_of_int g)
-            (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#proof_status
-            with
-            | GrafiteTypes.No_proof -> (Cic.Implicit None)
-            | Incomplete_proof i -> 
-                 let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in 
-                 Lazy.force p
-            | Proof p -> let _,_,_subst,p,_, _ = p in Lazy.force p
-            | Intermediate _ -> assert false)));
-     addDebugItem "Print current proof (natural language) to stderr" 
-       (fun _ -> 
-        prerr_endline 
-          (ApplyTransformation.txt_of_cic_object 120 [] 
-            ~map_unicode_to_tex:(Helm_registry.get_bool
-              "matita.paste_unicode_as_tex")
-            (match 
-            (MatitaScript.current ())#grafite_status#proof_status
-            with
-            | GrafiteTypes.No_proof -> assert false
-            | Incomplete_proof i -> 
-                let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in 
-                Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs)
-            | Proof (_,m,_subst,p,ty, attrs) -> 
-                Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)
-            | Intermediate _ -> assert false)));
     addDebugSeparator ();
     addDebugCheckbox "high level pretty printer" ~init:true
-      (fun mi () -> CicMetaSubst.use_low_level_ppterm_in_context := mi#active);
+      (fun mi () -> assert false (* MATITA 1.0 *));
     addDebugSeparator ();
     addDebugItem "always show all disambiguation errors"
       (fun _ -> MatitaGui.all_disambiguation_passes := true);
@@ -211,13 +159,11 @@ let _ =
       (fun mi () -> MultiPassDisambiguator.only_one_pass := mi#active);
     addDebugCheckbox "tactics logging" 
       (fun mi () -> NTacStatus.debug := mi#active);
-    addDebugCheckbox "auto logging"
-      (fun mi () -> NAuto.debug := mi#active);
     addDebugCheckbox "disambiguation/refiner/unification/metasubst logging"
       (fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug :=
               mi#active; MultiPassDisambiguator.debug := mi#active; NCicMetaSubst.debug := mi#active);
     addDebugCheckbox "reduction logging"
-      (fun mi () -> NCicReduction.debug := mi#active; CicReduction.ndebug := mi#active);
+      (fun mi () -> NCicReduction.debug := mi#active);
     addDebugSeparator ();
     addDebugItem "Expand virtuals"
     (fun _ -> (MatitaScript.current ())#expandAllVirtuals);