From 25d3d1c2613fd2b4e6a323289ca94fb7b75ebe5d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 13 Jun 2005 15:25:49 +0000 Subject: [PATCH] integrated lablgtksourceview --- helm/matita/buildTimeConf.ml.in | 6 +++- helm/matita/configure.ac | 7 ++--- helm/matita/matita.glade | 21 ++----------- helm/matita/matita.ml | 6 ++-- helm/matita/matitaGui.ml | 53 ++++++++++++++++++++++----------- helm/matita/matitaGui.mli | 1 + 6 files changed, 50 insertions(+), 44 deletions(-) diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 1715dd1f4..6b35fda1f 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -34,5 +34,9 @@ let phrase_sep = ".";; let blank_uri = "about:blank";; let current_proof_uri = "about:current_proof";; let default_script_font = "Monospace 10";; -let images_dir = "@IMAGES_DIR@";; +let runtime_base_dir = "@RT_BASE_DIR@";; + +let images_dir = runtime_base_dir ^ "/icons" +let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc" +let lang_file = runtime_base_dir ^ "/matita.lang" diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index e7cd49fad..e25e1c65c 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -42,6 +42,7 @@ FINDLIB_REQUIRES="\ $FINDLIB_CREQUIRES \ lablgtk2.glade \ lablgtkmathview \ +lablgtksourceview \ helm-xmldiff \ " for r in $FINDLIB_REQUIRES @@ -86,8 +87,7 @@ if test "$DEBUG" = "true"; then echo "debugging enabled" fi -MATITA_GTKRC="matita.gtkrc" -IMAGES_DIR="icons" +RT_BASE_DIR="." AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) @@ -97,8 +97,7 @@ AC_SUBST(FINDLIB_CREQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) -AC_SUBST(MATITA_GTKRC) -AC_SUBST(IMAGES_DIR) +AC_SUBST(RT_BASE_DIR) AC_OUTPUT([ buildTimeConf.ml diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index bea43910b..d1a39dd9d 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1906,7 +1906,7 @@ Copyright (C) 2005, False - + True True GTK_POLICY_AUTOMATIC @@ -1915,24 +1915,7 @@ Copyright (C) 2005, GTK_CORNER_TOP_LEFT - - 2 - True - True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 2 - 0 - 0 - - + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 97595d192..5433a898b 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -37,7 +37,7 @@ let _ = MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.clean_owner_environment (); MatitaDb.create_owner_environment (); - GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; (* loads gtk rc files *) + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) ignore (GMain.Main.init ()); (* environment trust *) @@ -60,7 +60,7 @@ let _ = let script = MatitaScript.script - ~buffer:gui#main#scriptTextView#buffer + ~buffer:gui#sourceView#buffer ~init:(Lazy.force MatitaEngine.initial_status) ~mathviewer:(MatitaMathView.mathViewer ()) ~urichooser:(fun uris -> @@ -69,7 +69,7 @@ let script = ~title:"Matita: URI chooser" ~msg:"Select the URI" ~hide_uri_entry:true ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT - ~copy_cb:(fun s -> gui#main#scriptTextView#buffer#insert ("\n"^s^"\n")) + ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n")) () ~id:"boh?" uris with MatitaTypes.Cancel -> []) () diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 899c4b41e..b6b3f5ea2 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -68,6 +68,16 @@ class gui () = [ main#mainWinEventBox ] in let console = new console ~buffer:main#logTextView#buffer () in + let (source_view: GSourceView.source_view) = + GSourceView.source_view + ~auto_indent:true + ~insert_spaces_instead_of_tabs:true ~tabs_width:2 + ~margin:80 ~show_margin:true + ~smart_home_end:true + ~packing:main#scriptScrolledWin#add + () + in + let source_buffer = source_view#source_buffer in object (self) val mutable chosen_file = None val mutable _ok_not_exists = false @@ -133,7 +143,7 @@ class gui () = in let tac_w_term ast _ = if (MatitaScript.instance ())#onGoingProof () then - let (buf: GText.buffer) = self#main#scriptTextView#buffer in + let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ TacticAstPp.pp_tactic ast) in @@ -169,6 +179,15 @@ class gui () = MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn))); (* script *) + let _ = + match GSourceView.source_language_from_file BuildTimeConf.lang_file with + | None -> + MatitaLog.warn (sprintf "can't load language file %s" + BuildTimeConf.lang_file) + | Some matita_lang -> + source_buffer#set_language matita_lang; + source_buffer#set_highlight true + in let s () = MatitaScript.instance () in let disableSave () = script_fname <- None; @@ -202,8 +221,8 @@ class gui () = in let newScript () = (s ())#reset (); disableSave () in let cursor () = - let buf = self#main#scriptTextView#buffer in - buf#place_cursor (buf#get_iter_at_mark (`NAME "locked")) + source_buffer#place_cursor + (source_buffer#get_iter_at_mark (`NAME "locked")) in let advance _ = (MatitaScript.instance ())#advance (); cursor () in let retract _ = (MatitaScript.instance ())#retract (); cursor () in @@ -213,7 +232,7 @@ class gui () = let connect_key sym f = connect_key self#main#mainWinEventBox#event ~modifiers:[`CONTROL] ~stop:true sym f; - connect_key self#main#scriptTextView#event + connect_key self#sourceView#event ~modifiers:[`CONTROL] ~stop:true sym f in connect_button self#main#scriptAdvanceButton advance; @@ -231,27 +250,27 @@ class gui () = connect_menu_item self#main#newMenuItem newScript; connect_key GdkKeysyms._period (fun () -> - let buf = self#main#scriptTextView#buffer in - buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n"; - advance ()); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + ".\n"; + advance ()); connect_key GdkKeysyms._Return (fun () -> - let buf = self#main#scriptTextView#buffer in - buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n"; - advance ()); + source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + "\n"; + advance ()); (* script monospace font stuff *) let font = Helm_registry.get_opt_default Helm_registry.get BuildTimeConf.default_script_font "matita.script_font" in (* let monospace_tag = - self#main#scriptTextView#buffer#create_tag [`FONT_DESC font] + source_buffer#create_tag [`FONT_DESC font] in *) - self#main#scriptTextView#misc#modify_font_by_name font; + self#sourceView#misc#modify_font_by_name font; (* let _ = - self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ -> - let start, stop = self#main#scriptTextView#buffer#bounds in - self#main#scriptTextView#buffer#apply_tag monospace_tag start stop) + source_buffer#connect#changed ~callback:(fun _ -> + let start, stop = source_buffer#bounds in + source_buffer#apply_tag monospace_tag start stop) in *) (* debug menu *) self#main#debugMenu#misc#hide (); @@ -260,7 +279,7 @@ class gui () = self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); self#main#hintHighImage#set_file (image_path "matita-bulb-high.png"); (* focus *) - self#main#scriptTextView#misc#grab_focus (); + self#sourceView#misc#grab_focus (); (* main win dimension *) let width = Gdk.Screen.width () in let height = Gdk.Screen.height () in @@ -283,7 +302,7 @@ class gui () = method console = console - + method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view) method about = about method fileSel = fileSel method main = main diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 674f3702c..42922140c 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -54,6 +54,7 @@ object (* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console + method sourceView: GSourceView.source_view (** {2 Dialogs instantiation} * methods below create a new window on each invocation. You should -- 2.39.2