end
let clean_current_baseuri grafite_status =
- LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
+ LibraryClean.clean_baseuris [grafite_status#baseuri]
-let save_moo lexicon_status grafite_status =
+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.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+ grafite_status#proof_status = GrafiteTypes.No_proof
in
match script#bos, script#eos, no_pstatus with
| true, _, _ -> ()
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname
- grafite_status.GrafiteTypes.moo_content_rev;
+ GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
- lexicon_status.LexiconEngine.lexicon_content_rev
+ grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
+ NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ grafite_status#dump
| _ -> clean_current_baseuri grafite_status
;;
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
connect_menu_item main#ligatureButton self#nextSimilarSymbol;
ignore(source_buffer#connect#after#insert_text
~callback:(fun iter str ->
- if main#menuitemAutoAltL#active && str = " " then
- ignore(self#expand_virtual_if_any iter " ")));
+ if main#menuitemAutoAltL#active && (str = " " || str = "\n") then
+ ignore(self#expand_virtual_if_any iter str)));
ignore (findRepl#findEntry#connect#activate find_forward);
(* interface lockers *)
let lock_world _ =
MultiPassDisambiguator.use_library := saved_use_library;
unlock_world ()
| exc ->
- notify_exn exc;
+ (try notify_exn exc with Sys.Break as e -> notify_exn e);
unlock_world ()
in
(*thread_main ();*)
else main#tacticsButtonsHandlebox#misc#hide ())
~check:main#menuitemPalette;
connect_button main#butImpl_intro
- (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+ (fun () -> source_buffer#insert "apply rule (⇒#i […] (…));\n");
connect_button main#butAnd_intro
(fun () -> source_buffer#insert
- "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (∧#i (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butOr_intro_left
- (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∨#i_l (…));\n");
connect_button main#butOr_intro_right
- (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∨#i_r (…));\n");
connect_button main#butNot_intro
- (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+ (fun () -> source_buffer#insert "apply rule (¬#i […] (…));\n");
connect_button main#butTop_intro
- (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+ (fun () -> source_buffer#insert "apply rule (⊤#i);\n");
connect_button main#butImpl_elim
(fun () -> source_buffer#insert
- "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (⇒#e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butAnd_elim_left
- (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∧#e_l (…));\n");
connect_button main#butAnd_elim_right
- (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∧#e_r (…));\n");
connect_button main#butOr_elim
(fun () -> source_buffer#insert
- "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
+ "apply rule (∨#e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
connect_button main#butNot_elim
(fun () -> source_buffer#insert
- "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butBot_elim
- (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+ (fun () -> source_buffer#insert "apply rule (⊥#e (…));\n");
connect_button main#butRAA
(fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
connect_button main#butUseLemma
(fun () -> source_buffer#insert "apply rule (discharge […]);\n");
connect_button main#butForall_intro
- (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∀#i {…} (…));\n");
connect_button main#butForall_elim
- (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∀#e {…} (…));\n");
connect_button main#butExists_intro
- (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∃#i {…} (…));\n");
connect_button main#butExists_elim
(fun () -> source_buffer#insert
- "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
(* TO BE REMOVED *)
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;
else saveAsScript ()
in
let abandon_script () =
- let lexicon_status = (s ())#lexicon_status in
let grafite_status = (s ())#grafite_status in
if source_view#buffer#modified then
(match ask_unsaved main#toplevel with
| `YES -> saveScript ()
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- save_moo lexicon_status grafite_status
+ save_moo grafite_status
in
let loadScript () =
let script = s () in
match ask_unsaved main#toplevel with
| `YES ->
saveScript ();
- save_moo script#lexicon_status script#grafite_status;
+ save_moo script#grafite_status;
GMain.Main.quit ()
| `NO -> GMain.Main.quit ()
| `CANCEL -> ()
else
- (save_moo script#lexicon_status script#grafite_status;
+ (save_moo script#grafite_status;
GMain.Main.quit ()));
connect_button main#scriptAdvanceButton advance;
connect_button main#scriptRetractButton retract;
(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
(* 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
val similar_memory = Hashtbl.create 97
+ val mutable old_used_memory = false
method private nextSimilarSymbol () =
let write_similarsymbol s =
| [] -> ()
| eqclass ->
similarsymbols_orig <- eqclass;
+ let is_used =
+ try Hashtbl.find similar_memory similarsymbols_orig
+ with Not_found ->
+ let is_used = List.map (fun x -> x,false) eqclass in
+ Hashtbl.add similar_memory eqclass is_used;
+ is_used
+ in
let hd, next, tl =
- match
- try Hashtbl.find similar_memory similarsymbols_orig
- with Not_found -> Hashtbl.add similar_memory eqclass eqclass; eqclass
- with a::b::c -> a,b,c | _ -> assert false
+ let used, unused =
+ List.partition (fun s -> List.assoc s is_used) eqclass
+ in
+ match used @ unused with a::b::c -> a,b,c | _ -> assert false
in
let hd, tl =
if hd = last_symbol then next, tl @ [hd] else hd, (next::tl)
in
+ old_used_memory <- List.assoc hd is_used;
+ let is_used =
+ (hd,true) :: List.filter (fun (x,_) -> x <> hd) is_used
+ in
+ Hashtbl.replace similar_memory similarsymbols_orig is_used;
write_similarsymbol hd;
similarsymbols <- tl @ [ hd ]))
else
match similarsymbols with
| [] -> ()
| hd :: tl ->
- Hashtbl.replace similar_memory similarsymbols_orig similarsymbols;
+ let is_used = Hashtbl.find similar_memory similarsymbols_orig in
+ let last = HExtlib.list_last tl in
+ let old_used_for_last = old_used_memory in
+ old_used_memory <- List.assoc hd is_used;
+ let is_used =
+ (hd, true) :: (last,old_used_for_last) ::
+ List.filter (fun (x,_) -> x <> last && x <> hd) is_used
+ in
+ Hashtbl.replace similar_memory similarsymbols_orig is_used;
similarsymbols <- tl @ [ hd ];
write_similarsymbol hd
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
projects / helm.git / blobdiff