X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2FmatitaInit.ml;h=26f4b40ffe421a1867b85e6358137ea5730ae187;hb=441c4689edf514535218090c6ca70795d500b90a;hp=72c8600bb76a42fe13b968859319a7433db73f94;hpb=bb9aa02b52977c05fe678a4e15bfc64e27c2c5f5;p=helm.git

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index 72c8600bb..26f4b40ff 100644
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-open Printf
-
 type thingsToInitilaize = 
   ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
   
@@ -45,13 +43,14 @@ let already_configured s l =
 let conffile = ref BuildTimeConf.matita_conf
 
 let registry_defaults = [
-  "matita.debug",             "false";
-  "matita.external_editor",   "gvim -f -c 'go %p' %f";
-  "matita.preserve",          "false";
-  "matita.profile",           "true";
-  "matita.system",            "false";
-  "matita.verbosity",         "1";
-  "matita.bench",              "false";
+  "matita.debug",                "false";
+  "matita.external_editor",      "gvim -f -c 'go %p' %f";
+  "matita.preserve",             "false";
+  "matita.profile",              "true";
+  "matita.system",               "false";
+  "matita.verbosity",            "1";
+  "matita.bench",                "false";
+  "matita.paste_unicode_as_tex", "false"
     (** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
      * intuitively verbose *)
 ]
@@ -67,7 +66,6 @@ let fill_registry init_status =
     init_status
 
 let load_configuration init_status =
-  wants [ Registry ] init_status;
   if not (already_configured [ConfigurationFile] init_status) then
     begin
       Helm_registry.load_from !conffile;
@@ -137,44 +135,44 @@ let _ =
   List.iter
     (fun (name, s) -> Hashtbl.replace usages name s)
     [ "matitac", 
-        sprintf "MatitaC v%s
+        Printf.sprintf "MatitaC v%s
 Usage: matitac [ OPTION ... ] FILE
 Options:"
           BuildTimeConf.version;
       "gragrep",
-        sprintf "Grafite Grep v%s
+        Printf.sprintf "Grafite Grep v%s
 Usage: gragrep [ -r ] PATH
 Options:"
           BuildTimeConf.version;
       "matitaprover",
-        sprintf "Matita's prover v%s
+        Printf.sprintf "Matita's prover v%s
 Usage: matitaprover [ -tptppath ] FILE.p
 Options:"
           BuildTimeConf.version;
       "matita",
-        sprintf "Matita v%s
+        Printf.sprintf "Matita v%s
 Usage: matita [ OPTION ... ] [ FILE ... ]
 Options:"
           BuildTimeConf.version;
       "cicbrowser",
-        sprintf
+        Printf.sprintf
           "CIC Browser v%s
 Usage: cicbrowser [ URL | WHELP QUERY ]
 Options:"
           BuildTimeConf.version;
       "matitadep",
-        sprintf "MatitaDep v%s
+        Printf.sprintf "MatitaDep v%s
 Usage: matitadep [ OPTION ... ] FILE ...
 Options:"
           BuildTimeConf.version;
       "matitaclean",
-        sprintf "MatitaClean v%s
+        Printf.sprintf "MatitaClean v%s
 Usage: matitaclean all
        matitaclean [ (FILE | URI) ... ]
 Options:"
           BuildTimeConf.version;
       "matitamake",
-        sprintf "MatitaMake v%s
+        Printf.sprintf "MatitaMake v%s
 Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build)
   init
     Parameters: name (the name of the development, required)
@@ -211,7 +209,8 @@ Options:"
           BuildTimeConf.version;
     ]
 let default_usage =
-  sprintf "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
+  Printf.sprintf 
+    "Matita v%s\nUsage: matita [ ARG ]\nOptions:" BuildTimeConf.version
 
 let usage () =
   let basename = Filename.basename Sys.argv.(0) in
@@ -225,6 +224,7 @@ let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 
 let parse_cmdline init_status =
   if not (already_configured [CmdLine] init_status) then begin
+    wants [Registry] init_status;
     let includes = ref [] in
     let default_includes = [ 
       ".";
@@ -279,6 +279,9 @@ let parse_cmdline init_status =
             Arg.Unit (fun () -> Helm_registry.set_bool "matita.debug" true),
               ("Do not catch top-level exception "
               ^ "(useful for backtrace inspection)");
+	    "-onepass",
+	    Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
+	    "Enable only one disambiguation pass";    
           ]
         else []
       in
@@ -308,11 +311,16 @@ let die_usage () =
   print_endline (usage ());
   exit 1
 
+let conf_components = 
+  [ load_configuration; fill_registry; parse_cmdline]
+
+let other_components =
+  [ initialize_makelib; initialize_db; initialize_environment ]
+
 let initialize_all () =
   status := 
     List.fold_left (fun s f -> f s) !status
-    [ fill_registry; parse_cmdline; load_configuration; initialize_makelib;
-      initialize_db; initialize_environment ]
+    (conf_components @ other_components)
 (*     initialize_notation 
       (initialize_environment 
         (initialize_db 
@@ -320,14 +328,9 @@ let initialize_all () =
             (load_configuration
               (parse_cmdline !status))))) *)
 
-let load_configuration_file () =
-  status := load_configuration !status
-
-let parse_cmdline () =
-  status := parse_cmdline !status
+let parse_cmdline_and_configuration_file () =
+  status := List.fold_left (fun s f -> f s) !status conf_components
 
-let fill_registry () =
-  status := fill_registry !status
 ;;
 
 Inversion_principle.init ()