From 07dde6f87105c18b28fc784b7d596a5d242e1225 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Apr 2004 16:33:02 +0000 Subject: [PATCH] snapshot --- helm/matita/.depend | 13 +++-- helm/matita/Makefile.in | 3 +- helm/matita/configure.ac | 1 + helm/matita/matita.glade | 25 +++++++-- helm/matita/matita.ml | 76 ++++++++++++++++---------- helm/matita/matitaDisambiguator.ml | 82 +++++++++++++++++++++++++++++ helm/matita/matitaDisambiguator.mli | 40 ++++++++++++++ helm/matita/matitaGeneratedGui.ml | 34 ++++++------ helm/matita/matitaGeneratedGui.mli | 21 +++++--- helm/matita/matitaGtkMisc.ml | 66 +++++++++++++++-------- helm/matita/matitaGtkMisc.mli | 20 ++++--- helm/matita/matitaGui.ml | 11 ++-- helm/matita/matitaGui.mli | 4 +- helm/matita/matitaProof.mli | 4 +- helm/matita/matitaTypes.ml | 46 +++++++++++++++- 15 files changed, 348 insertions(+), 98 deletions(-) create mode 100644 helm/matita/matitaDisambiguator.ml create mode 100644 helm/matita/matitaDisambiguator.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index c369a7b52..6a625f62b 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,13 +1,16 @@ +matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi +matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi -matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi -matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmi +matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmo matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi matitaGui.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGui.cmi matitaGui.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmx matitaGui.cmi -matita.cmo: matitaGtkMisc.cmi matitaGui.cmi -matita.cmx: matitaGtkMisc.cmx matitaGui.cmx +matita.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaGui.cmi matitaProof.cmi +matita.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaGui.cmx matitaProof.cmx matitaProof.cmo: matitaTypes.cmo matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaProof.cmi -matitaGtkMisc.cmi: matitaGeneratedGui.cmi +matitaDisambiguator.cmi: matitaTypes.cmo +matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo matitaGui.cmi: matitaGeneratedGui.cmi matitaProof.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index fb9f9cf5b..d8265a27a 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -17,7 +17,8 @@ CMOS = \ matitaGtkMisc.cmo \ matitaGui.cmo \ matitaTypes.cmo \ - matitaProof.cmo + matitaProof.cmo \ + matitaDisambiguator.cmo CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) all: matita diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 2b8f535f0..86b0529fc 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -34,6 +34,7 @@ helm-cic_transformations \ helm-registry \ helm-tactics \ helm-xml \ +helm-disambiguator \ " for r in $FINDLIB_REQUIRES do diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 497470299..23ebec8b3 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -485,7 +485,7 @@ - + DUMMY GTK_WINDOW_TOPLEVEL GTK_WIN_POS_CENTER @@ -506,7 +506,7 @@ GTK_BUTTONBOX_END - + True True True @@ -518,7 +518,7 @@ - + True True True @@ -538,7 +538,24 @@ - + + True + DUMMY + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 59076c94e..cd8f6f7ab 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -25,12 +25,17 @@ open MatitaGtkMisc -exception Not_implemented of string -let not_implemented feature = raise (Not_implemented feature) +(** {2 Internal status} *) - (** exceptions whose content should be presented to the user *) -exception Failure of string -let error s = raise (Failure s) + (* TODO Zack: may be current_proofs if we want an MDI interface *) +let (current_proof: MatitaProof.proof option ref) = ref None + +(** {2 Settings} *) + +let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" +let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def" + +(** {2 Initialization} *) let _ = Helm_registry.load_from "matita.conf.xml" let _ = GMain.Main.init () @@ -38,31 +43,46 @@ let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file") (** quit program, possibly asking for confirmation *) let quit () = GMain.Main.quit () -let _ = gui#setQuitCallback quit -let _ = gui#main#debugMenu#misc#hide () + +let _ = + gui#setQuitCallback quit; + gui#main#debugMenu#misc#hide (); + ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> + if (!current_proof <> None) && + not (ask_confirmation ~gui + ~msg:("Starting a new proof will abort current one,\n" ^ + "are you sure you want to continue?") + ()) + then + () (* abort new proof process *) + else + prerr_endline "nuova prova" + (* TODO Zack: FINQUI ora mi serve il disambiguatore *) + )) (** *) -if BuildTimeConf.debug then begin - gui#main#debugMenu#misc#show (); - let addDebugItem ~label callback = - let item = GMenu.menu_item ~label () in - gui#main#debugMenu_menu#append item; - ignore (item#connect#activate callback); - in - addDebugItem "interactive user uri choice" (fun _ -> - try - let uris = - interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE - ~title:"titolo" ~msg:"messaggio" ~nonvars_button:true - ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con"; - "cic:/cinque.var"] - in - List.iter prerr_endline uris - with No_choice -> error "no choice"); - addDebugItem "toggle auto disambiguation" (fun _ -> - Helm_registry.set_bool "matita.auto_disambiguation" - (not (Helm_registry.get_bool "matita.auto_disambiguation"))) -end +let _ = + if BuildTimeConf.debug then begin + gui#main#debugMenu#misc#show (); + let addDebugItem ~label callback = + let item = GMenu.menu_item ~label () in + gui#main#debugMenu_menu#append item; + ignore (item#connect#activate callback) + in + addDebugItem "interactive user uri choice" (fun _ -> + try + let uris = + interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE + ~msg:"messaggio" ~nonvars_button:true + ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con"; + "cic:/cinque.var"] + in + List.iter prerr_endline uris + with MatitaTypes.No_choice -> MatitaTypes.error "no choice"); + addDebugItem "toggle auto disambiguation" (fun _ -> + Helm_registry.set_bool "matita.auto_disambiguation" + (not (Helm_registry.get_bool "matita.auto_disambiguation"))) + end (** *) let _ = GtkThread.main () diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml new file mode 100644 index 000000000..183e775d0 --- /dev/null +++ b/helm/matita/matitaDisambiguator.ml @@ -0,0 +1,82 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class parserr () = + object + method parseTerm (stream: char Stream.t) = + CicTextualParser2.parse_term stream + + (* TODO Zack: implements methods below *) + method parseTactic (_: char Stream.t) : DisambiguateTypes.tactic = + MatitaTypes.not_implemented "parserr.parseTactic" + method parseTactical (_: char Stream.t) : DisambiguateTypes.tactical = + MatitaTypes.not_implemented "parserr.parseTactical" + method parseCommand (_: char Stream.t) : DisambiguateTypes.command = + MatitaTypes.not_implemented "parserr.parseCommand" + method parseScript (_: char Stream.t) : DisambiguateTypes.script = + MatitaTypes.not_implemented "parserr.parseScript" + end + +class disambiguator + ~parserr ~mqiconn ~(chooseUris: MatitaTypes.choose_uris_callback) + ~(chooseInterp: MatitaTypes.choose_interp_callback) () + = + let disambiguate_term = + let module Callbacks = + struct + let interactive_user_uri_choice + ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg + ~id uris + = + chooseUris ~selection_mode ~title ~msg + ~nonvars_button:enable_button_for_non_vars uris + + let interactive_interpretation_choice = chooseInterp + let input_or_locate_uri ~(title:string) = + (* TODO Zack: I try to avoid using this callback. I therefore assume + * that the presence of an identifier that can't be resolved via + * "locate" query is a syntax error *) + MatitaTypes.not_implemented + "MatitaDisambiguator: input_or_locate_uri callback" + end + in + let module Disambiguator = Disambiguate.Make (Callbacks) in + Disambiguator.disambiguate_term + in + object (self) + val mutable parserr: parserr = parserr + method parserr = parserr + method setParserr p = parserr <- p + + method disambiguateTermAst + ~context ~metasenv ?(env = DisambiguateTypes.Environment.empty) termAst + = + disambiguate_term mqiconn context metasenv termAst ~aliases:env + + method disambiguateTerm ~context ~metasenv ?env stream = + self#disambiguateTermAst ~context ~metasenv ?env + (parserr#parseTerm stream) + end + diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli new file mode 100644 index 000000000..ce89b6e08 --- /dev/null +++ b/helm/matita/matitaDisambiguator.mli @@ -0,0 +1,40 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class parserr: unit -> + object + inherit MatitaTypes.parserr + end + +class disambiguator: + parserr:MatitaTypes.parserr -> (** parser *) + mqiconn:MQIConn.handle -> (** mathql database connection *) + chooseUris:MatitaTypes.choose_uris_callback -> + chooseInterp:MatitaTypes.choose_interp_callback -> + unit -> + object + inherit MatitaTypes.disambiguator + end + diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index e110e1d92..e8d10d9ce 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -241,30 +241,34 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end -class genericDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"GenericDialog" ?domain () in +class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = new GWindow.dialog (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata)) + (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val genericDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + val confirmationDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = new GWindow.dialog (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata)) - method genericDialog = genericDialog + (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) + method confirmationDialog = confirmationDialog val dialog_vbox1 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata)) method dialog_vbox1 = dialog_vbox1 - val cancelbutton1 = + val confirmationDialogCancelButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"cancelbutton1" ~info:"GtkButton" xmldata)) - method cancelbutton1 = cancelbutton1 - val okbutton1 = + (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata)) + method confirmationDialogCancelButton = confirmationDialogCancelButton + val confirmationDialogOkButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"okbutton1" ~info:"GtkButton" xmldata)) - method okbutton1 = okbutton1 + (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata)) + method confirmationDialogOkButton = confirmationDialogOkButton + val confirmationDialogLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata)) + method confirmationDialogLabel = confirmationDialogLabel method reparent parent = dialog_vbox1#misc#reparent parent; toplevel#destroy () @@ -445,9 +449,9 @@ let check_all ?(show=false) () = let aboutWin = new aboutWin () in if show then aboutWin#toplevel#show (); aboutWin#check_widgets (); - let genericDialog = new genericDialog () in - if show then genericDialog#toplevel#show (); - genericDialog#check_widgets (); + let confirmationDialog = new confirmationDialog () in + if show then confirmationDialog#toplevel#show (); + confirmationDialog#check_widgets (); let toolBarWin = new toolBarWin () in if show then toolBarWin#toplevel#show (); toolBarWin#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 017b3cae6..c4f2a31cc 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -1,3 +1,5 @@ +(* Automatically generated from matitaGeneratedGui.ml by make *) + class mainWin : ?file:string -> ?domain:string -> @@ -149,25 +151,28 @@ class toolBarWin : method vbox1 : GPack.box method xml : Glade.glade_xml Gtk.obj end -class genericDialog : +class confirmationDialog : ?file:string -> ?domain:string -> ?autoconnect:bool -> unit -> object - val cancelbutton1 : GButton.button + val confirmationDialog : + [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val confirmationDialogCancelButton : GButton.button + val confirmationDialogLabel : GMisc.label + val confirmationDialogOkButton : GButton.button val dialog_vbox1 : GPack.box - val genericDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog - val okbutton1 : GButton.button val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit - method cancelbutton1 : GButton.button method check_widgets : unit -> unit - method dialog_vbox1 : GPack.box - method genericDialog : + method confirmationDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog - method okbutton1 : GButton.button + method confirmationDialogCancelButton : GButton.button + method confirmationDialogLabel : GMisc.label + method confirmationDialogOkButton : GButton.button + method dialog_vbox1 : GPack.box method reparent : GObj.widget -> unit method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog method xml : Glade.glade_xml Gtk.obj diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index a87700941..80f5676cd 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -82,16 +82,17 @@ let is_var_uri s = let non p x = not (p x) -exception No_choice - class type gui = - object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog end + object + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newConfirmationDialog : + title:string -> msg:string -> unit -> + MatitaGeneratedGui.confirmationDialog + end let interactive_user_uri_choice -(* ~(gui: MatitaGeneratedGui.uriChoiceDialog>) *) - ~(gui:#gui) - ~(selection_mode:Gtk.Tags.selection_mode) ~title ~msg ?(nonvars_button=false) - uris + ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "") + ?(msg = "") ?(nonvars_button=false) uris = let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in if (selection_mode <> `SINGLE) && @@ -99,33 +100,56 @@ let interactive_user_uri_choice then Lazy.force nonvars_uris else begin - let win = gui#newUriDialog () in - win#uriChoiceTreeView#selection#set_mode selection_mode; - let model = new stringListModel win#uriChoiceTreeView in + let dialog = gui#newUriDialog () in + dialog#uriChoiceTreeView#selection#set_mode selection_mode; + let model = new stringListModel dialog#uriChoiceTreeView in let choices = ref None in let nonvars = ref false in - win#uriChoiceDialog#set_title title; - win#uriChoiceLabel#set_text msg; + dialog#uriChoiceDialog#set_title title; + dialog#uriChoiceLabel#set_text msg; List.iter model#easy_append uris; - win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; + dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; let return v = choices := v; - win#uriChoiceDialog#destroy (); + dialog#uriChoiceDialog#destroy (); GMain.Main.quit () in - ignore (win#uriChoiceConstantsButton#connect#clicked (fun _ -> + ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ -> return (Some (Lazy.force nonvars_uris)))); - ignore (win#uriChoiceAutoButton#connect#clicked (fun _ -> + ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ -> Helm_registry.set_bool "matita.auto_disambiguation" true; return (Some (Lazy.force nonvars_uris)))); - ignore (win#uriChoiceSelectedButton#connect#clicked (fun _ -> + ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ -> match model#easy_selection () with | [] -> () | uris -> return (Some uris))); - ignore (win#uriChoiceAbortButton#connect#clicked (fun _ -> return None)); - ignore (win#uriChoiceDialog#event#connect#delete (fun _ -> true)); - win#uriChoiceDialog#show (); + ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None)); + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + dialog#uriChoiceDialog#show (); GtkThread.main (); - (match !choices with None -> raise No_choice | Some uris -> uris) + (match !choices with + | None -> raise MatitaTypes.No_choice + | Some uris -> uris) end +let interactive_interp_choice ~(gui:#gui) choices = + (* TODO Zack implement interactive_interp_choice *) + MatitaTypes.warning + "'interactive_interp_choice' not implemented: returning 1st interpretation"; + [0] + +let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = + let dialog = gui#newConfirmationDialog ~title ~msg () in + let result = ref None in + let return r _ = + result := Some r; + dialog#confirmationDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#confirmationDialogOkButton#connect#clicked (return true)); + ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false)); + ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true)); + dialog#confirmationDialog#show (); + GtkThread.main (); + (match !result with None -> assert false | Some r -> r) + diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 6ad12a756..aef9e52f7 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -51,15 +51,19 @@ class stringListModel: class type gui = object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newConfirmationDialog : + title:string -> msg:string -> unit -> + MatitaGeneratedGui.confirmationDialog end -exception No_choice +(** {3 Dialogs} *) - (** @raise No_choice *) -val interactive_user_uri_choice: - gui:#gui -> - selection_mode:Gtk.Tags.selection_mode -> title:string -> msg:string -> - ?nonvars_button:bool -> - string list -> - string list + (** @raise MatitaTypes.No_choice *) +val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback + + (** @raise MatitaTypes.No_choice *) +val interactive_interp_choice: gui:#gui -> MatitaTypes.choose_interp_callback + + (** @return true if user hit "ok" button, false if user hit "cancel" button *) +val ask_confirmation: gui:#gui -> ?title:string -> ?msg:string -> unit -> bool diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 7161aa9e8..f5d873d19 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -49,7 +49,6 @@ class gui file = let toolbar = new toolBarWin ~file () in let main = new mainWin ~file () in let about = new aboutWin ~file () in - let dialog = new genericDialog ~file () in let fileSel = new fileSelectionWin ~file () in let proof = new proofWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) @@ -60,7 +59,7 @@ class gui file = (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in - [ c about; c dialog; c fileSel; c main; c proof; c toolbar ]); + [ c about; c fileSel; c main; c proof; c toolbar ]); (* show/hide commands *) toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; toggle_visibility proof#proofWin main#showProofMenuItem; @@ -85,7 +84,6 @@ class gui file = method toolbar = toolbar method main = main method about = about - method dialog = dialog method fileSel = fileSel method proof = proof @@ -99,6 +97,13 @@ class gui file = dialog#check_widgets (); dialog + method newConfirmationDialog ~title ~msg () = + let dialog = new confirmationDialog ~file () in + dialog#confirmationDialog#set_title title; + dialog#confirmationDialogLabel#set_label msg; + dialog#check_widgets (); + dialog + method private addKeyBinding key callback = List.iter (fun evbox -> add_key_binding key callback evbox) keyBindingBoxes diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index f7faab8c5..87a5c05de 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -41,7 +41,6 @@ class gui : (** {2 Access to low-level GTK widgets} *) method about : MatitaGeneratedGui.aboutWin - method dialog : MatitaGeneratedGui.genericDialog method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin method proof : MatitaGeneratedGui.proofWin @@ -53,6 +52,9 @@ class gui : method newUriDialog : unit -> MatitaGeneratedGui.uriChoiceDialog method newInterpDialog : unit -> MatitaGeneratedGui.interpChoiceDialog + method newConfirmationDialog : + title:string -> msg:string -> unit -> + MatitaGeneratedGui.confirmationDialog end diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli index e74efdf7d..e9df2c140 100644 --- a/helm/matita/matitaProof.mli +++ b/helm/matita/matitaProof.mli @@ -55,8 +55,8 @@ class proof: uri:UriManager.uri -> typ:Cic.term -> (** {2 tactic commands builders} *) -(* TODO these are just some examples, a lot of other tactics/tacticals must be - * added here *) +(* TODO Zack: these are just some examples, a lot of other tactics/tacticals + * must be added here *) val intros: ?namer:MatitaTypes.namer -> proofStatus -> MatitaTypes.command diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index b26c2f677..acae4c9df 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -23,8 +23,16 @@ * http://helm.cs.unibo.it/ *) - (** no current proof is available *) -exception No_proof +exception Not_implemented of string +let not_implemented feature = raise (Not_implemented feature) + + (** exceptions whose content should be presented to the user *) +exception Failure of string +let error s = raise (Failure s) +let warning s = prerr_endline ("MATITA WARNING: " ^ s) + +exception No_proof (** no current proof is available *) +exception No_choice (** no choice was made by the user *) class type observer = (* "observer" pattern *) @@ -49,7 +57,41 @@ class type command = method undo: unit -> unit end +class type parserr = (* "parser" is a keyword :-( *) + object + method parseTerm: char Stream.t -> DisambiguateTypes.term + method parseTactic: char Stream.t -> DisambiguateTypes.tactic + method parseTactical: char Stream.t -> DisambiguateTypes.tactical + method parseCommand: char Stream.t -> DisambiguateTypes.command + method parseScript: char Stream.t -> DisambiguateTypes.script + end + +class type disambiguator = + object + method parserr: parserr + method setParserr: parserr -> unit + + method disambiguateTerm: + context:Cic.context -> metasenv:Cic.metasenv -> + ?env:DisambiguateTypes.environment -> + char Stream.t -> + (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list + method disambiguateTermAst: + context:Cic.context -> metasenv:Cic.metasenv -> + ?env:DisambiguateTypes.environment -> + DisambiguateTypes.term -> + (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list + end + (** {2 shorthands} *) type namer = ProofEngineTypes.mk_fresh_name_type +type choose_uris_callback = + selection_mode:Gtk.Tags.selection_mode -> + ?title:string -> ?msg:string -> ?nonvars_button:bool -> + string list -> + string list + +type choose_interp_callback = (string * string) list list -> int list + -- 2.39.2