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
[ 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
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
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;
(* 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
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
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