X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=ed739eefbebb8c9be4a9e5ab95f919166625a722;hb=ef3f78973c2fa3151c09681bcdb60107cd73c518;hp=5aa3d59e9c69edb491a4bd3c0189d33d16cf6489;hpb=4f04bf7d4032d301ce723fce357a27f92f003893;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5aa3d59e9..ed739eefb 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MatitaGeneratedGui @@ -61,24 +63,32 @@ class console ~(buffer: GText.buffer) () = | `Warning -> self#warning (s ^ "\n") end -let clean_current_baseuri status = +let clean_current_baseuri grafite_status = try - let baseuri = GrafiteTypes.get_string_option status "baseuri" in + let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in let basedir = Helm_registry.get "matita.basedir" in LibraryClean.clean_baseuris ~basedir [baseuri] with GrafiteTypes.Option_error _ -> () -let ask_and_save_moo_if_needed parent fname status = +let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = let basedir = Helm_registry.get "matita.basedir" in - let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in + let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in let save () = - let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in - GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev; - LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata + let metadata_fname = + LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in + let lexicon_fname = + LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri + in + GrafiteMarshal.save_moo moo_fname + grafite_status.GrafiteTypes.moo_content_rev; + LibraryNoDb.save_metadata metadata_fname + lexicon_status.LexiconEngine.metadata; + LexiconMarshal.save_lexicon lexicon_fname + lexicon_status.LexiconEngine.lexicon_content_rev in if (MatitaScript.current ())#eos && - status.GrafiteTypes.proof_status = GrafiteTypes.No_proof + grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof then begin let rc = @@ -98,10 +108,10 @@ let ask_and_save_moo_if_needed parent fname status = if b then save () else - clean_current_baseuri status + clean_current_baseuri grafite_status end else - clean_current_baseuri status + clean_current_baseuri grafite_status let ask_unsaved parent = MatitaGtkMisc.ask_confirmation @@ -544,18 +554,22 @@ class gui () = (* toolbar *) let module A = GrafiteAst in let hole = CicNotationPt.UserInput in - let loc = DisambiguateTypes.dummy_floc in + let loc = HExtlib.dummy_floc in let tac ast _ = if (MatitaScript.current ())#onGoingProof () then (MatitaScript.current ())#advance - ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast))) + ~statement:("\n" + ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast))) () in let tac_w_term ast _ = if (MatitaScript.current ())#onGoingProof () then let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) - ("\n" ^ GrafiteAstPp.pp_tactic ast) + ("\n" + ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ast) in let tbar = main in connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); @@ -593,7 +607,9 @@ class gui () = (* log *) HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := - (fun exn -> + (function + | MatitaScript.ActionCancelled -> () + | exn -> if not (Helm_registry.get_bool "matita.debug") then let floc, msg = MatitaExcPp.to_string exn in begin @@ -660,7 +676,8 @@ class gui () = console#message ("'"^f^"' saved.\n"); in let abandon_script () = - let status = (s ())#status in + 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 () @@ -668,7 +685,9 @@ class gui () = | `CANCEL -> raise MatitaTypes.Cancel); (match script_fname with | None -> () - | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status); + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname + lexicon_status grafite_status); in let loadScript () = let script = s () in @@ -708,15 +727,10 @@ class gui () = let top = locker (keep_focus top) in let bottom = locker (keep_focus bottom) in let jump = locker (keep_focus jump) in - let connect_key sym f = - connect_key main#mainWinEventBox#event - ~modifiers:[`CONTROL] ~stop:true sym f; - connect_key self#sourceView#event - ~modifiers:[`CONTROL] ~stop:true sym f - in (* quit *) self#setQuitCallback (fun () -> - let status = (MatitaScript.current ())#status in + let lexicon_status = (MatitaScript.current ())#lexicon_status in + let grafite_status = (MatitaScript.current ())#grafite_status in if source_view#buffer#modified then begin let rc = ask_unsaved main#toplevel in @@ -728,8 +742,8 @@ class gui () = (match script_fname with | None -> () | Some fname -> - ask_and_save_moo_if_needed - main#toplevel fname status); + ask_and_save_moo_if_needed main#toplevel + fname lexicon_status grafite_status); GMain.Main.quit () end | `NO -> GMain.Main.quit () @@ -739,10 +753,11 @@ class gui () = else begin (match script_fname with - | None -> clean_current_baseuri status; GMain.Main.quit () + | None -> clean_current_baseuri grafite_status; GMain.Main.quit () | Some fname -> try - ask_and_save_moo_if_needed main#toplevel fname status; + ask_and_save_moo_if_needed main#toplevel fname lexicon_status + grafite_status; GMain.Main.quit () with MatitaTypes.Cancel -> ()) end); @@ -823,24 +838,23 @@ class gui () = (** selections / clipboards handling *) - method private markup_selected = MatitaMathView.has_selection () - method private text_selected = + method markupSelected = MatitaMathView.has_selection () + method private textSelected = (source_buffer#get_iter_at_mark `INSERT)#compare (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 - method private something_selected = - self#markup_selected || self#text_selected - method private markup_stored = MatitaMathView.has_clipboard () - method private text_stored = clipboard#text <> None - method private something_stored = self#markup_stored || self#text_stored + method private somethingSelected = self#markupSelected || self#textSelected + method private markupStored = MatitaMathView.has_clipboard () + method private textStored = clipboard#text <> None + method private somethingStored = self#markupStored || self#textStored - method canCopy = self#something_selected - method canCut = self#text_selected - method canDelete = self#text_selected - method canPaste = self#something_stored - method canPastePattern = self#markup_stored + method canCopy = self#somethingSelected + method canCut = self#textSelected + method canDelete = self#textSelected + method canPaste = self#somethingStored + method canPastePattern = self#markupStored method copy () = - if self#text_selected + if self#textSelected then begin MatitaMathView.empty_clipboard (); source_view#buffer#copy_clipboard clipboard; @@ -1257,8 +1271,8 @@ let interactive_interp_choice () choices = let _ = (* disambiguator callbacks *) - MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); - MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); + GrafiteDisambiguator.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;