X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.ml;h=2731a5ac727d9a209ded7ba84d4d055a88d709e4;hb=e3369ffc8b690703cfafc7985f69db5fc140d749;hp=b145c157acf979449bf1d815b2d68cc992139189;hpb=907f919aba0f21b18acff8a8e1c266ab92d10baf;p=helm.git

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index b145c157a..2731a5ac7 100644
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -25,11 +25,6 @@
 
 (* $Id$ *)
 
-open Printf
-
-open MatitaGtkMisc
-open GrafiteTypes
-
 (** {2 Initialization} *)
 
 let _ = 
@@ -37,82 +32,17 @@ let _ =
     ["-tptppath",Arg.String 
       (fun s -> Helm_registry.set_string "matita.tptppath" s),
       "Where to find the Axioms/ and Problems/ directory"];
-  MatitaInit.initialize_all ()
+  MatitaInit.initialize_all ();
+  MatitaMisc.reset_font_size ()
 ;;
 
-(* let _ = Saturation.init () (* ALB to link paramodulation *) *)
-
-(** {2 GUI callbacks} *)
-
-let gui = MatitaGui.instance ()
-
-let script =
-  let s = 
-    MatitaScript.script 
-      ~source_view:gui#sourceView
-      ~mathviewer:(MatitaMathView.mathViewer ())
-      ~urichooser:(fun uris ->
-        try
-          MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
-          ~title:"Matita: URI chooser" 
-          ~msg:"Select the URI" ~hide_uri_entry:true
-          ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
-          ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
-          () ~id:"boh?" uris
-        with MatitaTypes.Cancel -> [])
-      ~set_star:gui#setStar
-      ~ask_confirmation:
-        (fun ~title ~message -> 
-            MatitaGtkMisc.ask_confirmation ~title ~message 
-            ~parent:gui#main#toplevel ())
-      ()
-  in
+let _ =
   Predefined_virtuals.load_predefined_virtuals ();
-  Predefined_virtuals.load_predefined_classes ();
-  gui#sourceView#source_buffer#begin_not_undoable_action ();
-  s#reset (); 
-  s#template (); 
-  gui#sourceView#source_buffer#end_not_undoable_action ();
-  s
+  Predefined_virtuals.load_predefined_classes ()
+;;
   
-  (* math viewers *)
-let _ =
-  let cic_math_view = MatitaMathView.cicMathView_instance () in
-  let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
-  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 browser_observer _ = MatitaMathView.refresh_all_browsers () in
-  let sequents_observer grafite_status =
-    sequents_viewer#reset;
-    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
-  in
-  script#addObserver sequents_observer;
-  script#addObserver browser_observer
-
   (** {{{ Debugging *)
-let _ =
+let init_debugging_menu gui =
   if BuildTimeConf.debug ||
      Helm_registry.get_bool "matita.debug_menu" 
   then begin
@@ -133,8 +63,8 @@ let _ =
       ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
     addDebugItem "dump aliases" (fun _ ->
-      let status = script#grafite_status in
-      LexiconEngine.dump_aliases prerr_endline "" status);
+      let status = (MatitaScript.current ())#status in
+      GrafiteDisambiguate.dump_aliases prerr_endline "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->
       let status = script#lexicon_status in
@@ -148,22 +78,24 @@ let _ =
 *)
     addDebugSeparator ();
     addDebugCheckbox "high level pretty printer" ~init:true
-      (fun mi () -> assert false (* MATITA 1.0 *));
-    addDebugSeparator ();
-    addDebugItem "always show all disambiguation errors"
-      (fun _ -> MatitaGui.all_disambiguation_passes := true);
-    addDebugItem "prune disambiguation errors"
-      (fun _ -> MatitaGui.all_disambiguation_passes := false);
+      (fun mi () -> ApplyTransformation.use_high_level_pretty_printer := mi#active);
     addDebugSeparator ();
+    addDebugCheckbox "prune errors"
+      (fun mi () -> MatitaGui.all_disambiguation_passes := not (mi#active));
+    (*MATITA 1.0: ??? addDebugItem "prune disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := false);*)
     addDebugCheckbox "multiple disambiguation passes" ~init:true
       (fun mi () -> MultiPassDisambiguator.only_one_pass := mi#active);
+    addDebugSeparator ();
     addDebugCheckbox "tactics logging" 
       (fun mi () -> NTacStatus.debug := mi#active);
+    addDebugCheckbox "disambiguation logging"
+      (fun mi () -> MultiPassDisambiguator.debug := mi#active; NCicDisambiguate.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);
+              mi#active; MultiPassDisambiguator.debug := mi#active; NCicDisambiguate.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);
@@ -176,19 +108,13 @@ let _ =
   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
-  (try gui#loadScript (List.hd args) with Failure _ -> ());
+  let gui = MatitaGui.instance () in
+  init_debugging_menu gui;
+  List.iter gui#loadScript (List.rev args);
   gui#main#mainWin#show ();
   try
    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.";
-   let baseuri = 
-    (MatitaScript.current ())#grafite_status#baseuri
-   in
-     LibraryClean.clean_baseuris [baseuri]
+  with Sys.Break -> ()
+;;
 
 (* vim:set foldmethod=marker: *)