- changed command line interface of cicbrowser so that everything which could be...

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 2a87554d8f76bb2bf405e3b46e6ec8a539cd6263..38c161424850decc0e3fddde508bcb78ade0c0f2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -98,7 +98,7 @@ let _ =
   script#addObserver sequents_observer;
   script#addObserver browser_observer
 
-  (** <DEBUGGING> *)
+  (** {{{ Debugging *)
 let _ =
   if BuildTimeConf.debug then begin
     gui#main#debugMenu#misc#show ();
@@ -136,7 +136,7 @@ let _ =
     addDebugItem "dump metasenv"
       (fun _ ->
          if script#onGoingProof () then
-           MatitaLog.debug (CicMetaSubst.ppmetasenv script#proofMetasenv []));
+           MatitaLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
     addDebugItem "dump coercions Db" (fun _ ->
       List.iter
         (fun (s,t,u) -> 
@@ -155,8 +155,7 @@ let _ =
          let nb = gui#main#hintNotebook in
          nb#goto_page ((nb#current_page + 1) mod 3));
   end
-
-  (** </DEBUGGING> *)
+  (** Debugging }}} *)
 
 let _ =
   at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
@@ -164,12 +163,12 @@ let _ =
   if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
     Helm_registry.set "matita.mode" "cicbrowser";
     let browser = MatitaMathView.cicBrowser () in
-    let entry =
+    let uri =
       try
-        `Uri (UriManager.uri_of_string Sys.argv.(1))
-      with Invalid_argument _ -> `Dir "cic:/"
+        String.concat " " (List.tl (Array.to_list Sys.argv))
+      with Failure _ -> "cic:/"
     in
-    browser#load entry
+    browser#loadInput uri
   end else begin  (* matita *)
     Helm_registry.set "matita.mode" "matita";
     (try
@@ -181,3 +180,4 @@ let _ =
     GtkThread.main ()
   with Sys.Break -> ()
 
+(* vim:set foldmethod=marker: *)