let save_moo grafite_status =
let script = MatitaScript.current () in
let baseuri = grafite_status#baseuri in
- let no_pstatus =
- grafite_status#proof_status = GrafiteTypes.No_proof
- in
- match script#bos, script#eos, no_pstatus with
- | true, _, _ -> ()
- | _, 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)
+ match script#bos, script#eos with
+ | true, _ -> ()
+ | _, true ->
+ GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
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 -> Acic2content.hide_coercions := enabled);
+ ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
~callback:(fun enabled ->
Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
else raise exn);
(* script *)
let _ =
- let source_language_manager =
- GSourceView2.source_language_manager ~default:true in
- source_language_manager#set_search_path
- (BuildTimeConf.runtime_base_dir ::
- source_language_manager#search_path);
- match source_language_manager#language "grafite" with
- | None ->
- HLog.warn(sprintf "can't load a language file for \"grafite\" in %s"
- BuildTimeConf.runtime_base_dir)
- | Some x as matita_lang ->
- source_buffer#set_language matita_lang;
- source_buffer#set_highlight_syntax true
+ source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
+ source_buffer#set_highlight_syntax true
in
let disableSave () =
(s())#assignFileName None;
(fun _ ->
let c = MatitaMathView.cicBrowser () in
c#load (`About `Hints));
- connect_menu_item main#showAutoGuiMenuItem
- (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
connect_menu_item main#showTermGrammarMenuItem
(fun _ ->
let c = MatitaMathView.cicBrowser () in
method private updateFontSize () =
self#sourceView#misc#modify_font_by_name
- (sprintf "%s %d" BuildTimeConf.script_font font_size);
- MatitaAutoGui.set_font_size font_size
+ (sprintf "%s %d" BuildTimeConf.script_font font_size)
method increaseFontSize () =
font_size <- font_size + 1;
~id uris
=
let gui = instance () in
- let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
then
- Lazy.force nonvars_uris
+ uris
else begin
let dialog = gui#newUriDialog () in
if hide_uri_entry then
| _ -> ()));
dialog#uriChoiceDialog#set_title title;
dialog#uriChoiceLabel#set_text msg;
- List.iter model#easy_append (List.map UriManager.string_of_uri uris);
+ List.iter model#easy_append (List.map NReference.string_of_reference uris);
dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
let return v =
choices := v;
in
ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceConstantsButton (fun _ ->
- return (Some (Lazy.force nonvars_uris)));
+ return (Some uris));
if ok_action = `AUTO then
connect_button dialog#uriChoiceAutoButton (fun _ ->
Helm_registry.set_bool "matita.auto_disambiguation" true;
- return (Some (Lazy.force nonvars_uris)))
+ return (Some uris))
else
connect_button dialog#uriChoiceAutoButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
GtkThread.main ();