X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=5272f07a71fd01e48c8242cb77f2bc6657f3fbbc;hb=9a7c77e5c29d764109a104aa629761ba90cb511c;hp=ac34052c134d5e3da486aa18c29ca8e5fde8c20e;hpb=33bdd7e8c67299d34f05ac587488dd324fc6ba42;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index ac34052c1..5272f07a7 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -67,13 +67,13 @@ class console ~(buffer: GText.buffer) () = 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, _, _ -> () @@ -85,10 +85,11 @@ let save_moo lexicon_status grafite_status = 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 + (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 +202,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 @@ -263,7 +265,7 @@ let rec interactive_error_interp ~all_passes | [loffset,[_,envs_and_diffs,msg,significant]] -> let _,env,diff = List.hd envs_and_diffs in notify_exn - (GrafiteDisambiguator.DisambiguationError + (MultiPassDisambiguator.DisambiguationError (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]])); | _::_ -> let dialog = new disambiguationErrors () in @@ -298,7 +300,7 @@ let rec interactive_error_interp ~all_passes ~start:source_buffer#start_iter ~stop:source_buffer#end_iter; notify_exn - (GrafiteDisambiguator.DisambiguationError + (MultiPassDisambiguator.DisambiguationError (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]])) )); let return _ = @@ -327,10 +329,17 @@ let rec interactive_error_interp ~all_passes String.concat "\n" ("" :: List.map - (fun k,value -> - DisambiguatePp.pp_environment - (DisambiguateTypes.Environment.add k value - 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 @@ -340,9 +349,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 () @@ -380,15 +387,24 @@ class gui () = 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 @@ -433,10 +449,18 @@ class gui () = in ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ())); connect_menu_item main#contentsMenuItem (fun () -> - let cmd = - sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir - in - ignore (Sys.command cmd)); + if 0 = Sys.command "which gnome-help" then + let cmd = + sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir + in + ignore (Sys.command cmd) + else + MatitaGtkMisc.report_error ~title:"help system error" + ~message:( + "The program gnome-help is not installed\n\n"^ + "To browse the user manal it is necessary to install "^ + "the gnome help syste (also known as yelp)") + ~parent:main#toplevel ()); connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = @@ -626,7 +650,11 @@ class gui () = 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 _ = @@ -676,20 +704,33 @@ 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 - | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> (try interactive_error_interp ~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 ();*) @@ -762,49 +803,49 @@ 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 - (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 *) @@ -841,7 +882,6 @@ class gui () = 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 -> @@ -874,14 +914,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 @@ -930,12 +969,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; @@ -1066,58 +1105,97 @@ class gui () = 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 @@ -1477,7 +1555,6 @@ let interactive_string_choice 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 = @@ -1561,8 +1638,10 @@ let interactive_interp_choice () text prefix_len choices = let _ = (* disambiguator callbacks *) - GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); - GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + 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 ()); + 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;