* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open MatitaGeneratedGui
| `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 =
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
(* 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, [])));
(* 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
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 ()
| `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
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
(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 ()
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);
(** 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;
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;
projects / helm.git / blobdiff