- LexiconAst merged into GrafiteAst

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 6f4e09bbc6e2d29e01e3c76776c1d5852401f6a0..a42500bd6bf16fd524efa2906d38f5cb18dd4a5f 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -75,17 +75,7 @@ let save_moo grafite_status =
   match script#bos, script#eos with
   | true, _ -> ()
   | _, true ->
-     let moo_fname = 
-       LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
-        ~writable:true in
-     let lexicon_fname =
-       LibraryMisc.lexicon_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true
-     in
-     GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
-     LexiconMarshal.save_lexicon lexicon_fname
-      grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
-     NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+     GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
       grafite_status#dump
   | _ -> clean_current_baseuri grafite_status 
 ;;
@@ -330,13 +320,13 @@ let rec interactive_error_interp ~all_passes
                   let alias =
                    match k with
                    | DisambiguateTypes.Id id ->
-                       LexiconAst.Ident_alias (id, desc)
+                       GrafiteAst.Ident_alias (id, desc)
                    | DisambiguateTypes.Symbol (symb, i)-> 
-                       LexiconAst.Symbol_alias (symb, i, desc)
+                       GrafiteAst.Symbol_alias (symb, i, desc)
                    | DisambiguateTypes.Num i ->
-                       LexiconAst.Number_alias (i, desc)
+                       GrafiteAst.Number_alias (i, desc)
                   in
-                   LexiconAstPp.pp_alias alias)
+                   GrafiteAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
             source_buffer#insert
@@ -860,12 +850,14 @@ class gui () =
           | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
-        ~callback:(function
-          | true ->
-              CicNotation.set_active_notations
-                (List.map fst (CicNotation.get_all_notations ()))
-          | false ->
-              CicNotation.set_active_notations []);
+        ~callback:(function b ->
+          let s = s () in
+          let status =
+           Interpretations.toggle_active_interpretations s#grafite_status b
+          in
+           assert false (* MATITA1.0 ???
+           s#set_grafite_status status*)
+         );
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
         ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem