X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=87e9a44178a47a18b5bad6f9e9b3961e0825e71f;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=bbe8d2ed7247f60132ffa0f97e4c7e298959efc9;hpb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;p=helm.git

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index bbe8d2ed7..87e9a4417 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -66,13 +66,9 @@ let clean_exit n =
   match !grafite_status with
      [] -> exit n
    | grafite_status::_ ->
-      try
-       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+       let baseuri = GrafiteTypes.get_baseuri grafite_status in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
        exit n
-      with GrafiteTypes.Option_error("baseuri", "not found") ->
-       (* no baseuri ==> nothing to clean yet *)
-       exit n
 
 let terminate n =
  let terminator = String.make 1 (Char.chr 249) in
@@ -167,12 +163,14 @@ let rec interactive_loop () =
                  (List.map
                    (fun i ->
                      ApplyTransformation.txt_of_cic_sequent 80 metasenv
+                      ~map_unicode_to_tex:(Helm_registry.get_bool
+                        "matita.paste_unicode_as_tex")
                       (List.find (fun (j,_,_) -> j=i) metasenv)
                    ) open_goals))
           | _ -> ()
         in
          run_script str 
-           (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
+           (MatitaEngine.eval_from_stream ~first_statement_only:true 
            ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
          interactive_loop (Some (List.length !lexicon_status))
   with 
@@ -207,10 +205,9 @@ let main () =
    );
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
-  Helm_registry.set_int "matita.verbosity" 0;
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
-  grafite_status := [GrafiteSync.init ()];
+  grafite_status := [GrafiteSync.init "cic:/matita/tests/"];
   lexicon_status :=
    [CicNotation2.load_notation ~include_paths
      BuildTimeConf.core_notation_script] ;
@@ -247,10 +244,11 @@ let main () =
     else
      begin
        let baseuri =
-        GrafiteTypes.get_string_option
-         (match !grafite_status with
+        GrafiteTypes.get_baseuri 
+           (match !grafite_status with
              [] -> assert false
-           | s::_ -> s) "baseuri" in
+           | s::_ -> s)
+       in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri 
            ~must_exist:false ~baseuri ~writable:true