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

- ported to new ppmetasenv (swapped arguments)

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: *)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 89481b287434a12284dedd67c24e76c08acee8e5..8c891b04355759f28ff7a8522329fed6dcb54293 100644 (file)
--- 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