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

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index 4fdc704e2..d84203aa4 100644
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -82,22 +82,17 @@ let _ =
   sequents_viewer#load_logo;
   cic_math_view#set_href_callback
     (Some (fun uri ->
-      let uri =
-       try
-        `Uri (UriManager.uri_of_string uri)
-       with
-        UriManager.IllFormedUri _ ->
-         `NRef (NReference.reference_of_string uri)
-      in
-      (MatitaMathView.cicBrowser ())#load uri));
+      let uri = `NRef (NReference.reference_of_string uri) in
+       (MatitaMathView.cicBrowser ())#load uri));
   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 +100,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
@@ -150,7 +128,7 @@ let _ =
     in
     addDebugItem "dump aliases" (fun _ ->
       let status = script#grafite_status in
-      LexiconEngine.dump_aliases prerr_endline "" status);
+      GrafiteDisambiguate.dump_aliases prerr_endline "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->
       let status = script#lexicon_status in
@@ -162,45 +140,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 +153,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);