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)
- grafite_status#dump
+ GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ ~dependencies:grafite_status#dependencies grafite_status#dump
| _ -> clean_current_baseuri grafite_status
;;
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
| 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);
+ ~callback:(fun enabled -> Interpretations.hide_coercions := enabled);
MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
~callback:(fun enabled ->
Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);