X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=d04fbcadab4b8bcace82958733d197b007742cc4;hb=e7f64fe2cc67f3514131c8831f87311ff600d005;hp=7b5a929cb9466d517acebb527d6ead0baeacf5bb;hpb=290350836dd1727b3e3cdd4ee71e666a39cc4a09;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 7b5a929cb..d04fbcada 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -67,11 +67,11 @@ class console ~(buffer: GText.buffer) () = end let clean_current_baseuri grafite_status = - LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status] + LibraryClean.clean_baseuris [grafite_status#baseuri] let save_moo grafite_status = let script = MatitaScript.current () in - let baseuri = GrafiteTypes.get_baseuri grafite_status in + let baseuri = grafite_status#baseuri in let no_pstatus = grafite_status#proof_status = GrafiteTypes.No_proof in @@ -87,9 +87,9 @@ let save_moo grafite_status = in GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname - (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - (GrafiteTypes.get_estatus grafite_status)#dump + grafite_status#lstatus.LexiconEngine.lexicon_content_rev; + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + grafite_status#dump | _ -> clean_current_baseuri grafite_status ;; @@ -205,7 +205,7 @@ class interpErrorModel = exception UseLibrary;; let rec interactive_error_interp ~all_passes - (source_buffer:GSourceView.source_buffer) notify_exn offset errorll filename + (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename = (* hook to save a script for each disambiguation error *) if false then @@ -374,12 +374,12 @@ class gui () = [ main#mainWinEventBox ] in let console = new console ~buffer:main#logTextView#buffer () in - let (source_view: GSourceView.source_view) = - GSourceView.source_view + let (source_view: GSourceView2.source_view) = + GSourceView2.source_view ~auto_indent:true - ~insert_spaces_instead_of_tabs:true ~tabs_width:2 - ~margin:80 ~show_margin:true - ~smart_home_end:true + ~insert_spaces_instead_of_tabs:true ~tab_width:2 + ~right_margin_position:80 ~show_right_margin:true + ~smart_home_end:`AFTER ~packing:main#scriptScrolledWin#add () in @@ -575,11 +575,15 @@ class gui () = source_view#misc#grab_focus () in connect_menu_item main#undoMenuItem safe_undo; +(*CSC: XXX ignore(source_view#source_buffer#connect#can_undo ~callback:main#undoMenuItem#misc#set_sensitive); +*) main#undoMenuItem#misc#set_sensitive true; connect_menu_item main#redoMenuItem safe_redo; +(*CSC: XXX ignore(source_view#source_buffer#connect#can_redo ~callback:main#redoMenuItem#misc#set_sensitive); +*) main#redoMenuItem#misc#set_sensitive true; ignore(source_view#connect#after#populate_popup ~callback:(fun pre_menu -> let menu = new GMenu.menu pre_menu in @@ -883,13 +887,18 @@ class gui () = else raise exn); (* script *) let _ = - match GSourceView.source_language_from_file BuildTimeConf.lang_file with + 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 language file %s" - BuildTimeConf.lang_file) - | Some matita_lang -> + 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 true + source_buffer#set_highlight_syntax true in let disableSave () = (s())#assignFileName None; @@ -995,6 +1004,10 @@ class gui () = (fun _ -> let c = MatitaMathView.cicBrowser () in c#load (`About `Coercions)); + connect_menu_item main#showHintsDbMenuItem + (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 @@ -1019,8 +1032,11 @@ class gui () = (* focus *) self#sourceView#misc#grab_focus (); (* main win dimension *) - let width = Gdk.Screen.width () in - let height = Gdk.Screen.height () in + let width = Gdk.Screen.width ~screen:(Gdk.Screen.default ()) () in + let height = Gdk.Screen.height ~screen:(Gdk.Screen.default ()) () in + (* hack for xinerama, no proper support of monitors from lablgtk *) + let width = if width > 1600 then width / 2 else width in + let height = if height > 1200 then height / 2 else height in let main_w = width * 90 / 100 in let main_h = height * 80 / 100 in let script_w = main_w * 6 / 10 in @@ -1116,12 +1132,11 @@ class gui () = let inplaceof, symb = Virtuals.symbol_of_virtual last_word in self#reset_similarsymbols; let s = Glib.Utf8.from_unichar symb in - let iter = source_buffer#get_iter_at_mark `INSERT in assert(Glib.Utf8.validate s); source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars (MatitaGtkMisc.utf8_string_length inplaceof + len)); - source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + source_buffer#insert ~iter (if inplaceof.[0] = '\\' then s else (s ^ tok)); true with Virtuals.Not_a_virtual -> false @@ -1285,8 +1300,8 @@ class gui () = self#main#saveMenuItem#misc#set_sensitive true method console = console - method sourceView: GSourceView.source_view = - (source_view: GSourceView.source_view) + method sourceView: GSourceView2.source_view = + (source_view: GSourceView2.source_view) method fileSel = fileSel method findRepl = findRepl method main = main