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
CMOS = \
buildTimeConf.cmo \
matitaGeneratedGui.cmo \
+ matitaTypes.cmo \
matitaGtkMisc.cmo \
matitaGui.cmo \
- matitaTypes.cmo \
matitaProof.cmo \
matitaDisambiguator.cmo
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
$(OCAMLOPT) -linkpkg -o $@ $^
matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
- $(LABLGLADECC) $< > $@
+ $(LABLGLADECC) $< > matitaGeneratedGui.ml
$(OCAMLC) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
%.cmi: %.mli
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/
helm-tactics \
helm-xml \
helm-disambiguator \
+helm-mathql_interpreter \
"
for r in $FINDLIB_REQUIRES
do
<key name="glade_file">matita.glade</key>
<key name="auto_disambiguation">true</key>
</section>
+ <section name="mathql_interpreter">
+ <key name="db_map">mathql_db_map.txt</key>
+ <section name="mysql_connection">
+ <key name="host">mowgli.cs.unibo.it</key>
+ <key name="database">mowgli</key>
+ <!-- <key name="port"></key> -->
+ <!-- <key name="password"></key> -->
+ <key name="user">helm</key>
+ </section>
+ <key name="postgresql_connection_string">dbname=mowgli host=mowgli.cs.unibo.it user=helm</key>
+ <!-- flags is a string of the following characters: -->
+ <!-- "P", "Q", "R", "S", "T", "W" -->
+ <!-- P selects the PostgreSQL database -->
+ <!-- The default database is MySQL -->
+ <!-- Q logs the low-level queries (in SQL) -->
+ <!-- R logs the result of the executed queries (in MathQL) -->
+ <!-- S logs the source of the executed queries (in MathQL) -->
+ <!-- T logs statistical information (query execution times) -->
+ <!-- W logs some warnings (for mathql experts only) -->
+ <!-- By default the above information is not logged -->
+ <key name="flags"></key>
+ </section>
</helm_registry>
</child>
</widget>
+<widget class="GtkDialog" id="TextDialog">
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">DUMMY</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="TextDialogVBox">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area5">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="TextDialogCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="TextDialogOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="TextDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+</widget>
+
</glade-interface>
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 ()
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 *)
))
(** <DEBUGGING> *)
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 _ ->
"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
(** </DEBUGGING> *)
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
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 ();
-(* Automatically generated from matitaGeneratedGui.ml by make *)
-
class mainWin :
?file:string ->
?domain:string ->
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
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
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 _ ->
| [] -> ()
| 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
[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)
+
(** {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
+
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
* 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
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 *)
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} *)
projects / helm.git / commitdiff