rc-1

[helm.git] / matita / matitaWiki.ml

diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml
index c7c5e8838c74defd6a6687aa0b6b938e866a39c5..3c5607bd7df9ff1bf458d61f5f0dac65a3aea604 100644 (file)
--- a/matita/matitaWiki.ml
+++ b/matita/matitaWiki.ml
@@ -167,6 +167,8 @@ 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))
           | _ -> ()
@@ -231,10 +233,10 @@ let main () =
       | End_of_file -> ()
       | GrafiteEngine.Drop -> clean_exit 1
     );
-    let proof_status,moo_content_rev,metadata,lexicon_content_rev = 
+    let proof_status,moo_content_rev,lexicon_content_rev = 
       match !lexicon_status,!grafite_status with
       | ss::_, s::_ ->
-         s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+         s.proof_status, s.moo_content_rev,
           ss.LexiconEngine.lexicon_content_rev
       | _,_ -> assert false
     in
@@ -259,12 +261,7 @@ let main () =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       let metadata_fname =
-        LibraryMisc.metadata_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true
-       in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LibraryNoDb.save_metadata metadata_fname metadata;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
        exit 0
      end