X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=c559358c575934b67883baad1e9bd4286881fd32;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=60b112d982cca6bf9e6c75ae77d935d6f3114195;hpb=31c099c46eba26ee5ace403fb2cc0a68616bb887;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 60b112d98..c559358c5 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 ();
@@ -274,46 +273,25 @@ let _ =
   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: *)