From: Stefano Zacchiroli Date: Fri, 23 Apr 2004 14:54:46 +0000 (+0000) Subject: snapshot X-Git-Tag: V_0_0_9~75 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cc465115cdeea9819f43a5ad219b07c4f928c43a snapshot --- diff --git a/helm/matita/.depend b/helm/matita/.depend index 6a625f62b..fcfd2734b 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -6,8 +6,10 @@ 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: buildTimeConf.cmo matitaGtkMisc.cmi matitaGui.cmi matitaProof.cmi -matita.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaGui.cmx matitaProof.cmx +matita.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaGui.cmi matitaProof.cmi \ + matitaTypes.cmo +matita.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaGui.cmx matitaProof.cmx \ + matitaTypes.cmx matitaProof.cmo: matitaTypes.cmo matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaProof.cmi matitaDisambiguator.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index d8265a27a..79b3b0f75 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -14,9 +14,9 @@ OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) CMOS = \ buildTimeConf.cmo \ matitaGeneratedGui.cmo \ + matitaTypes.cmo \ matitaGtkMisc.cmo \ matitaGui.cmo \ - matitaTypes.cmo \ matitaProof.cmo \ matitaDisambiguator.cmo CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) @@ -36,7 +36,7 @@ matita.opt: $(CMXS) matita.ml $(OCAMLOPT) -linkpkg -o $@ $^ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade - $(LABLGLADECC) $< > $@ + $(LABLGLADECC) $< > matitaGeneratedGui.ml $(OCAMLC) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli %.cmi: %.mli @@ -50,7 +50,7 @@ clean: rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o matita matita.opt distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli - rm -f config.log config.status configure Makefile buildTimeConf.ml + rm -f config.log config.status Makefile buildTimeConf.ml rm -f matita.glade.bak matita.gladep.bak rm -rf autom4te.cache/ diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 86b0529fc..82ac6a721 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -35,6 +35,7 @@ helm-registry \ helm-tactics \ helm-xml \ helm-disambiguator \ +helm-mathql_interpreter \ " for r in $FINDLIB_REQUIRES do diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 751fed97d..dae03f998 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -4,4 +4,26 @@ matita.glade true +
+ mathql_db_map.txt +
+ mowgli.cs.unibo.it + mowgli + + + helm +
+ dbname=mowgli host=mowgli.cs.unibo.it user=helm + + + + + + + + + + + +
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 23ebec8b3..353f01ef9 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1016,4 +1016,85 @@ + + True + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index cd8f6f7ab..530e477a8 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -40,6 +40,13 @@ let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def" let _ = Helm_registry.load_from "matita.conf.xml" let _ = GMain.Main.init () let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file") +let parserr = new MatitaDisambiguator.parserr () +let mqiconn = MQIConn.init () +let disambiguator = + new MatitaDisambiguator.disambiguator ~parserr ~mqiconn + ~chooseUris:(interactive_user_uri_choice ~gui) + ~chooseInterp:(interactive_interp_choice ~gui) + () (** quit program, possibly asking for confirmation *) let quit () = GMain.Main.quit () @@ -56,8 +63,12 @@ let _ = then () (* abort new proof process *) else - prerr_endline "nuova prova" - (* TODO Zack: FINQUI ora mi serve il disambiguatore *) + let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in + let (env, metasenv, term) = + disambiguator#disambiguateTerm (Stream.of_string input) + in + prerr_endline ("nuova prova: " ^ CicPp.ppterm term) + (* TODO Zack: FINQUI *) )) (** *) @@ -65,8 +76,9 @@ 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; + let item = + GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label () + in ignore (item#connect#activate callback) in addDebugItem "interactive user uri choice" (fun _ -> @@ -78,10 +90,15 @@ let _ = "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"))) + with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice"); + addDebugItem "toggle auto disambiguation" (fun _ -> + Helm_registry.set_bool "matita.auto_disambiguation" + (not (Helm_registry.get_bool "matita.auto_disambiguation"))); + addDebugItem "mono line text input" (fun _ -> + prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ())); + addDebugItem "multi line text input" (fun _ -> + prerr_endline + (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ())); end (** *) diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 183e775d0..51e60bb18 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -70,13 +70,19 @@ class disambiguator method parserr = parserr method setParserr p = parserr <- p - method disambiguateTermAst - ~context ~metasenv ?(env = DisambiguateTypes.Environment.empty) termAst + val mutable _env = DisambiguateTypes.Environment.empty + method env = _env + method setEnv e = _env <- e + + method disambiguateTermAst ?(context = []) ?(metasenv = []) ?(env = _env) + termAst = - disambiguate_term mqiconn context metasenv termAst ~aliases:env + match disambiguate_term mqiconn context metasenv termAst ~aliases:env with + | [ x ] -> x + | _ -> assert false - method disambiguateTerm ~context ~metasenv ?env stream = - self#disambiguateTermAst ~context ~metasenv ?env + method disambiguateTerm ?context ?metasenv ?env stream = + self#disambiguateTermAst ?context ?metasenv ?env (parserr#parseTerm stream) end diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index e8d10d9ce..4219d7030 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -437,9 +437,45 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () toplevel#destroy () method check_widgets () = () end +class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"TextDialog" ?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:"TextDialog" ~info:"GtkDialog" xmldata)) + method toplevel = toplevel + val textDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + new GWindow.dialog (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + method textDialog = textDialog + val textDialogVBox = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"TextDialogVBox" ~info:"GtkVBox" xmldata)) + method textDialogVBox = textDialogVBox + val textDialogCancelButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata)) + method textDialogCancelButton = textDialogCancelButton + val textDialogOkButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata)) + method textDialogOkButton = textDialogOkButton + val textDialogLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata)) + method textDialogLabel = textDialogLabel + method reparent parent = + textDialogVBox#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end let check_all ?(show=false) () = ignore (GMain.Main.init ()); + let textDialog = new textDialog () in + if show then textDialog#toplevel#show (); + textDialog#check_widgets (); let interpChoiceDialog = new interpChoiceDialog () in if show then interpChoiceDialog#toplevel#show (); interpChoiceDialog#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index c4f2a31cc..f8bb3dc6f 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -1,5 +1,3 @@ -(* Automatically generated from matitaGeneratedGui.ml by make *) - class mainWin : ?file:string -> ?domain:string -> @@ -285,4 +283,28 @@ class interpChoiceDialog : method vbox3 : GPack.box method xml : Glade.glade_xml Gtk.obj end +class textDialog : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val textDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val textDialogCancelButton : GButton.button + val textDialogLabel : GMisc.label + val textDialogOkButton : GButton.button + val textDialogVBox : GPack.box + 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 check_widgets : unit -> unit + method reparent : GObj.widget -> unit + method textDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method textDialogCancelButton : GButton.button + method textDialogLabel : GMisc.label + method textDialogOkButton : GButton.button + method textDialogVBox : GPack.box + method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method xml : Glade.glade_xml Gtk.obj + end val check_all : ?show:bool -> unit -> unit diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 80f5676cd..e24bf27c1 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -85,11 +85,12 @@ let non p x = not (p x) class type gui = object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newConfirmationDialog : - title:string -> msg:string -> unit -> - MatitaGeneratedGui.confirmationDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newTextDialog: unit -> MatitaGeneratedGui.textDialog end +exception Cancel + let interactive_user_uri_choice ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "") ?(msg = "") ?(nonvars_button=false) uris @@ -114,6 +115,7 @@ let interactive_user_uri_choice dialog#uriChoiceDialog#destroy (); GMain.Main.quit () in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ -> return (Some (Lazy.force nonvars_uris)))); ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ -> @@ -124,11 +126,10 @@ let interactive_user_uri_choice | [] -> () | uris -> return (Some uris))); 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 MatitaTypes.No_choice + | None -> raise Cancel | Some uris -> uris) end @@ -139,17 +140,48 @@ let interactive_interp_choice ~(gui:#gui) choices = [0] let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = - let dialog = gui#newConfirmationDialog ~title ~msg () in + let dialog = gui#newConfirmationDialog () in + dialog#confirmationDialog#set_title title; + dialog#confirmationDialogLabel#set_label msg; let result = ref None in let return r _ = result := Some r; dialog#confirmationDialog#destroy (); GMain.Main.quit () in + ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true)); 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) +let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = + let dialog = gui#newTextDialog () in + dialog#textDialog#set_title title; + dialog#textDialogLabel#set_label msg; + let result = ref None in + let return r = + result := r; + dialog#textDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); + if multiline then begin (* multiline input required: use a TextView widget *) + let win = + GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER + ~vpolicy:`ALWAYS ~packing:dialog#textDialogVBox#add () + in + let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in + ignore (dialog#textDialogOkButton#connect#clicked (fun _ -> + return (Some (view#buffer#get_text ())))) + end else begin (* monoline input required: use a TextEntry widget *) + let entry = GEdit.entry ~packing:dialog#textDialogVBox#add () in + ignore (dialog#textDialogOkButton#connect#clicked (fun _ -> + return (Some entry#text))) + end; + ignore (dialog#textDialogCancelButton#connect#clicked (fun _ -> return None)); + dialog#textDialog#show (); + GtkThread.main (); + (match !result with None -> raise Cancel | Some r -> r) + diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index aef9e52f7..5bb6fa09d 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -49,21 +49,28 @@ class stringListModel: (** {2 Matita GUI components} *) class type gui = - object + object (* minimal gui object requirements *) method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newConfirmationDialog : - title:string -> msg:string -> unit -> - MatitaGeneratedGui.confirmationDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newTextDialog: unit -> MatitaGeneratedGui.textDialog end -(** {3 Dialogs} *) + (** {3 Dialogs} *) + +exception Cancel (* raised when no answer is given by the user *) - (** @raise MatitaTypes.No_choice *) + (** @raise Cancel *) val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback - (** @raise MatitaTypes.No_choice *) + (** @raise Cancel *) 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 + (** @param multiline (default: false) if true a TextView widget will be used + * for prompting the user otherwise a TextEntry widget will be + * @return the string given by the user *) +val ask_text: + gui:#gui -> ?title:string -> ?msg:string -> ?multiline:bool -> unit -> string + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index f5d873d19..017f39555 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -97,10 +97,13 @@ class gui file = dialog#check_widgets (); dialog - method newConfirmationDialog ~title ~msg () = + method newConfirmationDialog () = let dialog = new confirmationDialog ~file () in - dialog#confirmationDialog#set_title title; - dialog#confirmationDialogLabel#set_label msg; + dialog#check_widgets (); + dialog + + method newTextDialog () = + let dialog = new textDialog ~file () in dialog#check_widgets (); dialog diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 87a5c05de..f7845f2e5 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -50,11 +50,10 @@ class gui : * methods below create a new window on each invocation. You should * remember to destroy windows after use *) - method newUriDialog : unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog : unit -> MatitaGeneratedGui.interpChoiceDialog - method newConfirmationDialog : - title:string -> msg:string -> unit -> - MatitaGeneratedGui.confirmationDialog + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newTextDialog: unit -> MatitaGeneratedGui.textDialog end diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index acae4c9df..bfdb99904 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -32,7 +32,6 @@ 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 *) @@ -71,16 +70,22 @@ class type disambiguator = method parserr: parserr method setParserr: parserr -> unit + method env: DisambiguateTypes.environment + method setEnv: DisambiguateTypes.environment -> unit + + (* TODO Zack: as long as matita doesn't support MDI inteface, + * disambiguateTerm will return a single term *) + (** @param env defaults to self#env *) method disambiguateTerm: - context:Cic.context -> metasenv:Cic.metasenv -> + ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> char Stream.t -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list + (DisambiguateTypes.environment * Cic.metasenv * Cic.term) method disambiguateTermAst: - context:Cic.context -> metasenv:Cic.metasenv -> + ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> DisambiguateTypes.term -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list + (DisambiguateTypes.environment * Cic.metasenv * Cic.term) end (** {2 shorthands} *)