From 51ce243d63b02d6ad690a5d2e1d79e34d548f86b Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 15 Sep 2005 09:17:50 +0000
Subject: [PATCH] - changed command line interface of cicbrowser so that
 everything which could be written in the "URL" bar can be provided on the
 cmdline as well (even without double-quoting) - ported to new ppmetasenv
 (swapped arguments)

---
 helm/matita/matita.ml       | 16 ++++++++--------
 helm/matita/matitaEngine.ml |  2 +-
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 2a87554d8..38c161424 100644
--- 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: *)
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 89481b287..8c891b043 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -711,7 +711,7 @@ let eval_command opts status cmd =
          if metasenv <> [] then
           command_error (
             "metasenv not empty while giving a definition with body: " ^
-            CicMetaSubst.ppmetasenv metasenv []);
+            CicMetaSubst.ppmetasenv [] metasenv);
          let status = MatitaSync.add_obj uri obj status in
           match obj with
              Cic.Constant _ -> status
-- 
2.39.2