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;
+ NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ grafite_status#dump
| _ -> clean_current_baseuri grafite_status
;;
tree_store#get ~row:iter ~column:interp_no_col
end
+exception UseLibrary;;
let rec interactive_error_interp ~all_passes
(source_buffer:GSourceView.source_buffer) notify_exn offset errorll filename
String.concat "\n"
("" ::
List.map
- (fun k,value ->
- DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k
- (value,(fun _ _ _ -> Cic.Implicit None))
- DisambiguateTypes.Environment.empty))
+ (fun k,desc ->
+ let alias =
+ match k with
+ | DisambiguateTypes.Id id ->
+ LexiconAst.Ident_alias (id, desc)
+ | DisambiguateTypes.Symbol (symb, i)->
+ LexiconAst.Symbol_alias (symb, i, desc)
+ | DisambiguateTypes.Num i ->
+ LexiconAst.Number_alias (i, desc)
+ in
+ LexiconAstPp.pp_alias alias)
diff) ^ "\n"
in
source_buffer#insert
return ()
);
connect_button dialog#disambiguationErrorsMoreErrors
- (fun _ -> return () ;
- interactive_error_interp ~all_passes:true source_buffer
- notify_exn offset errorll filename);
+ (fun _ -> return () ; raise UseLibrary);
connect_button dialog#disambiguationErrorsCancelButton fail;
dialog#disambiguationErrors#show ();
GtkThread.main ()
Helm_registry.get_opt_default Helm_registry.int
~default:BuildTimeConf.default_font_size "matita.font_size"
in
+ let similarsymbols_tag_name = "similarsymbolos" in
+ let similarsymbols_tag = `NAME similarsymbols_tag_name in
let source_buffer = source_view#source_buffer in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
val mutable font_size = default_font_size
- val mutable next_ligatures = []
+ val mutable similarsymbols = []
+ val mutable similarsymbols_orig = []
val clipboard = GData.clipboard Gdk.Atom.clipboard
val primary = GData.clipboard Gdk.Atom.primary
+
+ method private reset_similarsymbols =
+ similarsymbols <- [];
+ similarsymbols_orig <- [];
+ try source_buffer#delete_mark similarsymbols_tag
+ with GText.No_such_mark _ -> ()
initializer
let s () = MatitaScript.current () in
source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
connect_menu_item main#findReplMenuItem show_find_Repl;
connect_menu_item main#externalEditorMenuItem self#externalEditor;
- connect_menu_item main#ligatureButton self#nextLigature;
+ connect_menu_item main#ligatureButton self#nextSimilarSymbol;
+ ignore(source_buffer#connect#after#insert_text
+ ~callback:(fun iter str ->
+ 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 _ =
let thread_main =
fun () ->
lock_world ();
+ let saved_use_library= !MultiPassDisambiguator.use_library in
try
+ MultiPassDisambiguator.use_library := !all_disambiguation_passes;
f ();
+ MultiPassDisambiguator.use_library := saved_use_library;
unlock_world ()
with
| MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
~all_passes:!all_disambiguation_passes source_buffer
notify_exn offset errorll (s())#filename
with
- exc -> notify_exn exc);
+ | UseLibrary ->
+ MultiPassDisambiguator.use_library := true;
+ (try f ()
+ with
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+ interactive_error_interp ~all_passes:true source_buffer
+ notify_exn offset errorll (s())#filename
+ | exc ->
+ notify_exn exc);
+ | exc -> notify_exn exc);
+ 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 (lem …);\n");
+ (fun () -> source_buffer#insert "apply rule (lem #premises name …);\n");
connect_button main#butDischarge
(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 *)
notify_exn exn
else raise exn);
(* script *)
- ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
| 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;
method pastePattern () =
source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)
- method private nextLigature () =
- let iter = source_buffer#get_iter_at_mark `INSERT in
- let write_ligature len s =
+ method private expand_virtual_if_any iter tok =
+ try
+ let len = MatitaGtkMisc.utf8_string_length tok in
+ let last_word =
+ let prev = iter#copy#backward_chars len in
+ prev#get_slice ~stop:(prev#copy#backward_find_char
+ (fun x -> Glib.Unichar.isspace x || x = Glib.Utf8.first_char "\\"))
+ 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)
+ (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 =
+ let s = Glib.Utf8.from_unichar s 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 len);
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
+ source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars 1);
+ source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s;
+ (try source_buffer#delete_mark similarsymbols_tag
+ with GText.No_such_mark _ -> ());
+ ignore(source_buffer#create_mark ~name:similarsymbols_tag_name
+ (source_buffer#get_iter_at_mark `INSERT));
in
- let get_ligature word =
- let len = String.length word in
- let aux_tex () =
- try
- for i = len - 1 downto 0 do
- if HExtlib.is_alpha word.[i] then ()
- else
- (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1))
- done;
- None
- with Found i ->
- if i = ~-1 then None else Some (String.sub word i (len - i))
- in
- let aux_ligature () =
- try
- for i = len - 1 downto 0 do
- if CicNotationLexer.is_ligature_char word.[i] then ()
- else raise (Found (i+1))
- done;
- raise (Found 0)
- with
- | Found i ->
- (try
- Some (String.sub word i (len - i))
- with Invalid_argument _ -> None)
- in
- match aux_tex () with
- | Some macro -> macro
- | None -> (match aux_ligature () with Some l -> l | None -> word)
+ let new_similarsymbol =
+ try
+ let iter_ins = source_buffer#get_iter_at_mark `INSERT in
+ let iter_lig = source_buffer#get_iter_at_mark similarsymbols_tag in
+ not (iter_ins#equal iter_lig)
+ with GText.No_such_mark _ -> true
in
- (match next_ligatures with
- | [] -> (* find ligatures and fill next_ligatures, then try again *)
- let last_word =
- iter#get_slice
- ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace)
+ if new_similarsymbol then
+ (if not(self#expand_virtual_if_any (source_buffer#get_iter_at_mark `INSERT) "")then
+ let last_symbol =
+ let i = source_buffer#get_iter_at_mark `INSERT in
+ Glib.Utf8.first_char (i#get_slice ~stop:(i#copy#backward_chars 1))
in
- let ligature = get_ligature last_word in
- (match CicNotationLexer.lookup_ligatures ligature with
- | [] -> ()
- | hd :: tl ->
- write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd;
- next_ligatures <- tl @ [ hd ])
- | hd :: tl ->
- write_ligature 1 hd;
- next_ligatures <- tl @ [ hd ])
+ (match Virtuals.similar_symbols last_symbol with
+ | [] -> ()
+ | 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 =
+ 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 ->
+ 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
method private externalEditor () =
let cmd = Helm_registry.get "matita.external_editor" in
let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
(HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
in
- prerr_endline ("txt:" ^ txt);
dialog#uriChoiceLabel#set_label txt;
List.iter model#easy_append uris;
let return v =
let _ =
(* disambiguator callbacks *)
- MultiPassDisambiguator.set_choose_uris_callback
+ Disambiguate.set_choose_uris_callback
(fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
- MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+ 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;
projects / helm.git / blobdiff