X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=b39eb85313030bb475af71efe000d7f53b27e7ab;hb=910c252965fe17d6b5af92e4658e7d02bac82d58;hp=46926ea9b387e75a32d0d9c213030136459485d2;hpb=05078521aaff6f41f55114e5332663b1e9706824;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 46926ea9b..b39eb8531 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -65,7 +65,6 @@ let script =
         (fun ~title ~message -> 
             MatitaGtkMisc.ask_confirmation ~title ~message 
             ~parent:gui#main#toplevel ())
-      ~develcreator:gui#createDevelopment
       ()
   in
   gui#sourceView#source_buffer#begin_not_undoable_action ();
@@ -167,21 +166,23 @@ let _ =
             (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
+            | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,_subst,p,_, _ = p in p
             | Intermediate _ -> assert false)));
      addDebugItem "Print current proof (natural language) to stderr" 
        (fun _ -> 
         prerr_endline 
-          (ObjPp.obj_to_string 120 GrafiteAst.Declarative "" 
+          (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" 
+            ~map_unicode_to_tex:(Helm_registry.get_bool
+              "matita.paste_unicode_as_tex")
             (match 
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with
             | GrafiteTypes.No_proof -> assert false
             | Incomplete_proof i -> 
-                let _,m,p,ty, attrs = i.GrafiteTypes.proof in 
+                let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in 
                 Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
-            | Proof (_,m,p,ty, attrs) -> 
+            | Proof (_,m,_subst,p,ty, attrs) -> 
                 Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
             | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
@@ -214,22 +215,34 @@ let _ =
     );
     addDebugSeparator ();
 *)
+    addDebugItem "disable high level pretty printer"
+      (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true);
+    addDebugItem "enable high level pretty printer"
+      (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false);
+(* ZACK moved to the View menu
     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);
+    addDebugItem "always show all disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := true);
+    addDebugItem "prune disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := false);
     addDebugSeparator ();
+(* ZACK moved to the View menu
     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));
@@ -240,8 +253,13 @@ let _ =
       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))
+           ((String.concat ","
+              (List.map
+                (fun u,saturations,_ ->
+                  UriManager.name_of_uri u ^
+                   "(" ^ string_of_int saturations ^ ")")
+                ul)) ^ ":"
+             ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t))
         (CoercDb.to_list ()));
     addDebugSeparator ();
     let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
@@ -250,49 +268,30 @@ let _ =
         ~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *)
     addDebugItem "load (sequent) MathML from matita.xml"
       (fun _ -> (mview ())#load_uri ~filename:"matita.xml");
+    addDebugItem "autoWin"
+    (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
   end
   (** Debugging }}} *)
 
-  (** {2 Command line parsing} *)
-
-let set_matita_mode () =
-  let matita_mode =
-    if Filename.basename Sys.argv.(0) = "cicbrowser" || 
-       Filename.basename Sys.argv.(0) = "cicbrowser.opt"
-    then "cicbrowser"
-    else "matita"
-  in
-  Helm_registry.set "matita.mode" matita_mode
-
   (** {2 Main} *)
 
 let _ =
-  set_matita_mode ();
   at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in
-  if Helm_registry.get "matita.mode" = "cicbrowser" then  (* cicbrowser *)
-    let browser = MatitaMathView.cicBrowser () in
-    let uri = match args with [] -> "cic:/" | _ -> String.concat " " args in
-    browser#loadInput uri
-  else begin  (* matita *)
-    (try gui#loadScript (List.hd args) with Failure _ -> ());
-    gui#main#mainWin#show ();
-  end;
+  (try gui#loadScript (List.hd args) with Failure _ -> ());
+  gui#main#mainWin#show ();
   try
-    GtkThread.main ()
+   GtkThread.main ()
   with Sys.Break ->
    Sys.set_signal Sys.sigint
     (Sys.Signal_handle
       (fun _ ->
         prerr_endline "Still cleaning the library: don't be impatient!"));
    prerr_endline "Matita is cleaning up. Please wait.";
-   try
-    let baseuri =
-     GrafiteTypes.get_string_option
-      (MatitaScript.current ())#grafite_status "baseuri"
-    in
+   let baseuri = 
+     GrafiteTypes.get_baseuri (MatitaScript.current ())#grafite_status
+   in
      LibraryClean.clean_baseuris [baseuri]
-   with GrafiteTypes.Option_error _ -> ()
 
 (* vim:set foldmethod=marker: *)