X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=a42500bd6bf16fd524efa2906d38f5cb18dd4a5f;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=d04fbcadab4b8bcace82958733d197b007742cc4;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index d04fbcada..a42500bd6 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -72,23 +72,10 @@ let clean_current_baseuri grafite_status = 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 ;; @@ -333,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 @@ -863,14 +850,16 @@ 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 -> 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); @@ -887,18 +876,8 @@ class gui () = 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; @@ -1008,8 +987,6 @@ class gui () = (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 @@ -1379,8 +1356,7 @@ class gui () = 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; @@ -1415,11 +1391,10 @@ let interactive_uri_choice ~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 @@ -1445,7 +1420,7 @@ let interactive_uri_choice | _ -> ())); 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; @@ -1454,20 +1429,20 @@ let interactive_uri_choice 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 (); @@ -1659,6 +1634,5 @@ let _ = Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) - GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; ignore (GMain.Main.init ())