X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=c5906e16a00581d647bfc1dae646c40732e8fa36;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=f0bd8acc027f42e076eb143a8b155ae2f7150fee;hpb=7a060397679753a0233139b1ba83ac83c2c49949;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index f0bd8acc0..c5906e16a 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -69,7 +69,7 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri grafite_status = LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status] -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 no_pstatus = @@ -88,7 +88,9 @@ let save_moo lexicon_status grafite_status = GrafiteMarshal.save_moo moo_fname grafite_status.GrafiteTypes.moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname - lexicon_status.LexiconEngine.lexicon_content_rev + (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 | _ -> clean_current_baseuri grafite_status ;; @@ -201,6 +203,7 @@ class interpErrorModel = 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 @@ -347,9 +350,7 @@ let rec interactive_error_interp ~all_passes 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 () @@ -396,11 +397,13 @@ class gui () = val mutable _only_directory = false val mutable font_size = default_font_size 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 _ -> () @@ -651,7 +654,8 @@ class gui () = connect_menu_item main#ligatureButton self#nextSimilarSymbol; ignore(source_buffer#connect#after#insert_text ~callback:(fun iter str -> - if false && str = " " then 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 _ = @@ -701,8 +705,11 @@ class gui () = 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) -> @@ -711,10 +718,20 @@ class gui () = ~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 ();*) @@ -787,33 +804,33 @@ class gui () = 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 @@ -822,14 +839,14 @@ class gui () = (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 *) @@ -898,14 +915,13 @@ class gui () = 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 @@ -954,12 +970,12 @@ class gui () = 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; @@ -1107,9 +1123,13 @@ class gui () = ~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)) - with Virtuals.Not_a_virtual -> () + (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 @@ -1130,25 +1150,51 @@ class gui () = with GText.No_such_mark _ -> true in 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 (match Virtuals.similar_symbols last_symbol with - | [] -> - let i = source_buffer#get_iter_at_mark `INSERT in - self#expand_virtual_if_any i "" - | hd :: next ::tl -> + | [] -> () + | 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 ] - | _ -> assert false) (* singleton eq classes are a non sense *) + 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