matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
-matitaGtkMisc.cmo: matitaGtkMisc.cmi
-matitaGtkMisc.cmx: matitaGtkMisc.cmi
+matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi
+matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmi
matitaGui.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGui.cmi
matitaGui.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmx matitaGui.cmi
-matita.cmo: matitaGeneratedGui.cmi matitaGui.cmi
-matita.cmx: matitaGeneratedGui.cmx matitaGui.cmx
-matitaGui.cmi: matitaGeneratedGui.cmi matitaGtkMisc.cmi
+matita.cmo: matitaGtkMisc.cmi matitaGui.cmi
+matita.cmx: matitaGtkMisc.cmx matitaGui.cmx
+matitaProof.cmo: matitaTypes.cmo matitaProof.cmi
+matitaProof.cmx: matitaTypes.cmx matitaProof.cmi
+matitaGtkMisc.cmi: matitaGeneratedGui.cmi
+matitaGui.cmi: matitaGeneratedGui.cmi
+matitaProof.cmi: matitaTypes.cmo
CAMLP4O = @CAMLP4O@
LABLGLADECC = @LABLGLADECC@
REQUIRES = @FINDLIB_REQUIRES@
+HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O)
OCAML_THREADS_FLAGS = -thread
buildTimeConf.cmo \
matitaGeneratedGui.cmo \
matitaGtkMisc.cmo \
- matitaGui.cmo
+ matitaGui.cmo \
+ matitaTypes.cmo \
+ matitaProof.cmo
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
all: matita
+
+ifeq ($(HAVE_OCAMLOPT),yes)
opt: matita.opt
+else
+opt:
+ @echo "Native code compilation is disabled"
+endif
matita: $(CMOS) matita.ml
$(OCAMLC) -linkpkg -o $@ $^
+(* 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/
+ *)
+
+let debug = @DEBUG@;;
+
AC_INIT(matita.ml)
+AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
+if test $HAVE_OCAMLC = "no"; then
+ AC_MSG_ERROR(could not find ocamlc)
+fi
+AC_CHECK_PROG(HAVE_OCAMLOPT, ocamlopt, yes, no)
+if test $HAVE_OCAMLOPT = "no"; then
+ AC_MSG_WARN(could not find ocamlopt: native code compilation disabled)
+fi
AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no)
if test $HAVE_OCAMLFIND = "yes"; then
OCAMLFIND="ocamlfind"
AC_MSG_ERROR(could not find camlp4o)
fi
-FINDLIB_REQUIRES="lablgtk2.glade helm-registry"
+FINDLIB_REQUIRES="\
+lablgtk2.glade \
+helm-cic_omdoc \
+helm-cic_transformations \
+helm-registry \
+helm-tactics \
+helm-xml \
+"
for r in $FINDLIB_REQUIRES
do
AC_MSG_CHECKING(for $r ocaml library)
fi
done
-AC_SUBST(OCAMLFIND)
+OCAMLFIND_COMMANDS=""
+AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no)
+if test $HAVE_OCAMLC_OPT = "yes"; then
+ if test "$OCAMLFIND_COMMANDS" = ""; then
+ OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt"
+ else
+ OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt"
+ fi
+fi
+AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no)
+if test $HAVE_OCAMLOPT_OPT = "yes"; then
+ if test "$OCAMLFIND_COMMANDS" = ""; then
+ OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt"
+ else
+ OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt"
+ fi
+fi
+if test "$OCAMLFIND_COMMANDS" != ""; then
+ OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND"
+fi
+AC_ARG_ENABLE(debug,
+ [ --enable-debug Turn on debugging],
+ [case "${enableval}" in
+ yes) DEBUG=true ;;
+ no) DEBUG=false ;;
+ *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;;
+ esac],
+ [DEBUG=true])
+if test "$DEBUG" = "true"; then
+ echo "debugging enabled"
+fi
+
AC_SUBST(CAMLP4O)
-AC_SUBST(LABLGLADECC)
+AC_SUBST(DEBUG)
AC_SUBST(FINDLIB_REQUIRES)
+AC_SUBST(HAVE_OCAMLOPT)
+AC_SUBST(LABLGLADECC)
+AC_SUBST(OCAMLFIND)
AC_OUTPUT([
buildTimeConf.ml
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image40">
+ <widget class="GtkImage" id="image76">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image41">
+ <widget class="GtkImage" id="image77">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image42">
+ <widget class="GtkImage" id="image78">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image43">
+ <widget class="GtkImage" id="image79">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image44">
+ <widget class="GtkImage" id="image80">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<widget class="GtkMenu" id="DebugMenu_menu">
<child>
- <widget class="GtkMenuItem" id="DebugMenuItem0">
+ <widget class="GtkMenuItem" id="separator2">
<property name="visible">True</property>
- <property name="label" translatable="yes">0</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="DebugMenuItem1">
- <property name="visible">True</property>
- <property name="label" translatable="yes">1</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="DebugMenuItem2">
- <property name="visible">True</property>
- <property name="label" translatable="yes">2</property>
- <property name="use_underline">True</property>
</widget>
</child>
</widget>
</child>
</widget>
-<widget class="GtkDialog" id="Debug">
- <property name="visible">True</property>
- <property name="title" translatable="yes">dialog1</property>
- <property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_NONE</property>
- <property name="modal">True</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="dialog-vbox5">
- <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="cancelbutton2">
- <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="okbutton2">
- <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>
- <placeholder/>
- </child>
- </widget>
- </child>
-</widget>
-
</glade-interface>
* http://helm.cs.unibo.it/
*)
+open MatitaGtkMisc
+
exception Not_implemented of string
let not_implemented feature = raise (Not_implemented feature)
let _ = GMain.Main.init ()
let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
-let interactive_user_uri_choice
- ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
- uris
-=
- let only_constant_choices =
- lazy
- (List.filter
- (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
- uris)
- in
- if (selection_mode <> `SINGLE) &&
- (Helm_registry.get_bool "matita.auto_disambiguation")
- then
- Lazy.force only_constant_choices
- else begin
- let win = gui#uriChoice in
- let choices = ref [] in
- let chosen = ref false in
- let use_only_constants = ref false in
- win#uriChoiceDialog#set_title title;
- win#uriChoiceLabel#set_text msg;
- gui#uriChoices#list_store#clear ();
- List.iter gui#uriChoices#easy_append uris;
- win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
- let bye = ref (fun () -> ()) in
- let id1 =
- win#uriChoiceConstantsButton#connect#clicked (fun _ ->
- use_only_constants := true;
- !bye ())
- in
- let id2 =
- win#uriChoiceAutoButton#connect#clicked (fun _ ->
- use_only_constants := true ;
- Helm_registry.set_bool "matita.auto_disambiguation" true;
- !bye ())
- in
- let id3 =
- win#uriChoiceSelectedButton#connect#clicked (fun _ ->
- choices := gui#uriChoices#easy_selection ();
- !bye ())
- in
- bye := (fun () ->
- win#uriChoiceDialog#misc#hide ();
- win#uriChoiceConstantsButton#misc#disconnect id1;
- win#uriChoiceAutoButton#misc#disconnect id2;
- win#uriChoiceSelectedButton#misc#disconnect id3;
- prerr_endline "quit";
- GMain.Main.quit ());
- win#uriChoiceDialog#show ();
- GtkThread.main ();
- if !use_only_constants then
- Lazy.force only_constant_choices
- else
- match !choices with
- | [] -> error "No choice"
- | choices -> choices
- end
-
-(*
-module DisambiguateCallbacks =
- struct
- let interactive_user_uri_choice =
- assert false (* TODO *)
-(* interactive_user_uri_choice *)
- let interactive_interpretation_choice choices =
- assert false (* TODO *)
- let input_or_locate_uri ~title =
- assert false (* TODO *)
- end
-*)
-
-let debugDialog () =
- let dialog =
- new MatitaGeneratedGui.debug
- ~file:(Helm_registry.get "matita.glade_file") ()
- in
- let retval = ref None in
- let return v =
- retval := Some v;
- dialog#debug#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#debug#event#connect#delete (fun _ -> true));
- ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1));
- ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2));
- dialog#debug#show ();
- GtkThread.main ();
- (match !retval with None -> assert false | Some v -> v)
-
-let _ =
- gui#main#debugMenuItem2#connect#activate (fun _ ->
- prerr_endline (string_of_int (debugDialog ())))
-
(** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
let _ = gui#setQuitCallback quit
-let _ =
- gui#main#debugMenuItem0#connect#activate (fun _ ->
- let uris =
- interactive_user_uri_choice
- ~selection_mode:`MULTIPLE
- ~nonvars_button:false
- ~title:"titolo"
- ~msg:"messaggio"
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
- in
- List.iter prerr_endline uris; print_newline ())
-let _ =
- gui#main#debugMenuItem1#connect#activate (fun _ ->
+let _ = gui#main#debugMenu#misc#hide ()
+
+ (** <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;
+ 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
+ (** </DEBUGGING> *)
-let _ =
-(* gui#uriChoices#easy_append "pippo"; *)
-(* gui#uriChoices#list_store#clear (); *)
- GtkThread.main ()
+let _ = GtkThread.main ()
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image40 =
+ val image76 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata))
- method image40 = image40
+ (Glade.get_widget_msg ~name:"image76" ~info:"GtkImage" xmldata))
+ method image76 = image76
val newMenu_menu =
new GMenu.menu (GtkMenu.Menu.cast
(Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
method openMenuItem = openMenuItem
- val image41 =
+ val image77 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata))
- method image41 = image41
+ (Glade.get_widget_msg ~name:"image77" ~info:"GtkImage" xmldata))
+ method image77 = image77
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image42 =
+ val image78 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata))
- method image42 = image42
+ (Glade.get_widget_msg ~name:"image78" ~info:"GtkImage" xmldata))
+ method image78 = image78
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image43 =
+ val image79 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata))
- method image43 = image43
+ (Glade.get_widget_msg ~name:"image79" ~info:"GtkImage" xmldata))
+ method image79 = image79
val separator1 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
method quitMenuItem = quitMenuItem
- val image44 =
+ val image80 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata))
- method image44 = image44
+ (Glade.get_widget_msg ~name:"image80" ~info:"GtkImage" xmldata))
+ method image80 = image80
val editMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
new GMenu.menu (GtkMenu.Menu.cast
(Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
method debugMenu_menu = debugMenu_menu
- val debugMenuItem0 =
+ val separator2 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata))
- method debugMenuItem0 = debugMenuItem0
- val debugMenuItem1 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata))
- method debugMenuItem1 = debugMenuItem1
- val debugMenuItem2 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata))
- method debugMenuItem2 = debugMenuItem2
+ (Glade.get_widget_msg ~name:"separator2" ~info:"GtkMenuItem" xmldata))
+ method separator2 = separator2
val helpMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata))
toplevel#destroy ()
method check_widgets () = ()
end
-class debug ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"Debug" ?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:"Debug" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
- method debug = debug
- val dialog_vbox5 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox5" ~info:"GtkVBox" xmldata))
- method dialog_vbox5 = dialog_vbox5
- val cancelbutton2 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"cancelbutton2" ~info:"GtkButton" xmldata))
- method cancelbutton2 = cancelbutton2
- val okbutton2 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata))
- method okbutton2 = okbutton2
- method reparent parent =
- dialog_vbox5#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
let check_all ?(show=false) () =
ignore (GMain.Main.init ());
- let debug = new debug () in
- if show then debug#toplevel#show ();
- debug#check_widgets ();
let interpChoiceDialog = new interpChoiceDialog () in
if show then interpChoiceDialog#toplevel#show ();
interpChoiceDialog#check_widgets ();
object
val aboutMenuItem : GMenu.menu_item
val debugMenu : GMenu.menu_item
- val debugMenuItem0 : GMenu.menu_item
- val debugMenuItem1 : GMenu.menu_item
- val debugMenuItem2 : GMenu.menu_item
val debugMenu_menu : GMenu.menu
val editMenu : GMenu.menu_item
val fileMenu : GMenu.menu_item
val fileMenu_menu : GMenu.menu
val helpMenu : GMenu.menu_item
val helpMenu_menu : GMenu.menu
- val image40 : GMisc.image
- val image41 : GMisc.image
- val image42 : GMisc.image
- val image43 : GMisc.image
- val image44 : GMisc.image
+ val image76 : GMisc.image
+ val image77 : GMisc.image
+ val image78 : GMisc.image
+ val image79 : GMisc.image
+ val image80 : GMisc.image
val mainMenuBar : GMenu.menu_shell
val mainStatusBar : GMisc.statusbar
val mainVPanes : GPack.paned
val saveMenuItem : GMenu.image_menu_item
val scrolledUserInput : GBin.scrolled_window
val separator1 : GMenu.menu_item
+ val separator2 : GMenu.menu_item
val showProofMenuItem : GMenu.check_menu_item
val showToolBarMenuItem : GMenu.check_menu_item
val toplevel : GWindow.window
method bind : name:string -> callback:(unit -> unit) -> unit
method check_widgets : unit -> unit
method debugMenu : GMenu.menu_item
- method debugMenuItem0 : GMenu.menu_item
- method debugMenuItem1 : GMenu.menu_item
- method debugMenuItem2 : GMenu.menu_item
method debugMenu_menu : GMenu.menu
method editMenu : GMenu.menu_item
method fileMenu : GMenu.menu_item
method fileMenu_menu : GMenu.menu
method helpMenu : GMenu.menu_item
method helpMenu_menu : GMenu.menu
- method image40 : GMisc.image
- method image41 : GMisc.image
- method image42 : GMisc.image
- method image43 : GMisc.image
- method image44 : GMisc.image
+ method image76 : GMisc.image
+ method image77 : GMisc.image
+ method image78 : GMisc.image
+ method image79 : GMisc.image
+ method image80 : GMisc.image
method mainMenuBar : GMenu.menu_shell
method mainStatusBar : GMisc.statusbar
method mainVPanes : GPack.paned
method saveMenuItem : GMenu.image_menu_item
method scrolledUserInput : GBin.scrolled_window
method separator1 : GMenu.menu_item
+ method separator2 : GMenu.menu_item
method showProofMenuItem : GMenu.check_menu_item
method showToolBarMenuItem : GMenu.check_menu_item
method toplevel : GWindow.window
method vbox3 : GPack.box
method xml : Glade.glade_xml Gtk.obj
end
-class debug :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val cancelbutton2 : GButton.button
- val debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val dialog_vbox5 : GPack.box
- val okbutton2 : 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 cancelbutton2 : GButton.button
- method check_widgets : unit -> unit
- method debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method dialog_vbox5 : GPack.box
- method okbutton2 : GButton.button
- method reparent : GObj.widget -> unit
- 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
end
+let is_var_uri s =
+ try
+ String.sub s (String.length s - 4) 4 = ".var"
+ with Invalid_argument _ -> false
+
+let non p x = not (p x)
+
+exception No_choice
+
+class type gui =
+ object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog end
+
+let interactive_user_uri_choice
+(* ~(gui: <newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog>) *)
+ ~(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) &&
+ (Helm_registry.get_bool "matita.auto_disambiguation")
+ 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 choices = ref None in
+ let nonvars = ref false in
+ win#uriChoiceDialog#set_title title;
+ win#uriChoiceLabel#set_text msg;
+ List.iter model#easy_append uris;
+ win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ let return v =
+ choices := v;
+ win#uriChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (win#uriChoiceConstantsButton#connect#clicked (fun _ ->
+ return (Some (Lazy.force nonvars_uris))));
+ ignore (win#uriChoiceAutoButton#connect#clicked (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ return (Some (Lazy.force nonvars_uris))));
+ ignore (win#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 ();
+ GtkThread.main ();
+ (match !choices with None -> raise No_choice | Some uris -> uris)
+ end
+
method easy_selection: unit -> string list
end
+(** {2 Matita GUI components} *)
+
+class type gui =
+ object
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ end
+
+exception No_choice
+
+ (** @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
+
let main = new mainWin ~file () in
let about = new aboutWin ~file () in
let dialog = new genericDialog ~file () in
- let uriChoice = new uriChoiceDialog ~file () in
- let interpChoice = new interpChoiceDialog ~file () in
let fileSel = new fileSelectionWin ~file () in
let proof = new proofWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ toolbar#toolBarEventBox; proof#proofWinEventBox ]
in
- let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in
object (self)
initializer
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c dialog; c fileSel; c main; c proof; c toolbar;
- c uriChoice; c interpChoice ]);
+ [ c about; c dialog; c fileSel; c main; c proof; c toolbar ]);
(* show/hide commands *)
toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
toggle_visibility proof#proofWin main#showProofMenuItem;
method main = main
method about = about
method dialog = dialog
- method uriChoice = uriChoice
- method interpChoice = interpChoice
method fileSel = fileSel
method proof = proof
+ method newUriDialog () =
+ let dialog = new uriChoiceDialog ~file () in
+ dialog#check_widgets ();
+ dialog
+
+ method newInterpDialog () =
+ let dialog = new interpChoiceDialog ~file () in
+ dialog#check_widgets ();
+ dialog
+
method private addKeyBinding key callback =
List.iter (fun evbox -> add_key_binding key callback evbox)
keyBindingBoxes
ignore (main#quitMenuItem#connect#activate callback);
self#addKeyBinding GdkKeysyms._q callback
- method uriChoices = uriChoices
-
end
method setQuitCallback : (unit -> unit) -> unit
- method uriChoices: MatitaGtkMisc.stringListModel
-
(** {2 Access to low-level GTK widgets} *)
method about : MatitaGeneratedGui.aboutWin
method dialog : MatitaGeneratedGui.genericDialog
method fileSel : MatitaGeneratedGui.fileSelectionWin
- method interpChoice : MatitaGeneratedGui.interpChoiceDialog
method main : MatitaGeneratedGui.mainWin
method proof : MatitaGeneratedGui.proofWin
method toolbar : MatitaGeneratedGui.toolBarWin
- method uriChoice : MatitaGeneratedGui.uriChoiceDialog
+
+ (** {2 Dialogs instantiation}
+ * 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
end
--- /dev/null
+(* 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 proofStatus ~uri ~typ =
+ object
+ inherit MatitaTypes.subject
+
+ val mutable _proof = (uri, [ 1, [], typ ], Cic.Meta (1, []), typ)
+ val mutable _goal = Some 1
+
+ method proof = _proof
+ method setProof p = _proof <- p
+ method goal = _goal
+ method setGoal g = _goal <- g
+ method status =
+ _proof,
+ (match _goal with Some g -> g | None -> raise MatitaTypes.No_proof)
+ method setStatus (p, g) =
+ _proof <- p;
+ _goal <- Some g
+
+ method to_xml =
+ let (uri, metasenv, bo, ty) = _proof in
+ let currentproof =
+ (* TODO CSC: Wrong: [] is just plainly wrong *)
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+ in
+ let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
+ Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
+ in
+ let xml, bodyxml =
+ match Cic2Xml.print_object uri ~ids_to_inner_sorts
+ ~ask_dtd_to_the_getter:true acurrentproof
+ with
+ | xml, Some bodyxml -> xml, bodyxml
+ | _, None -> assert false
+ in
+ (xml, bodyxml)
+
+ end
+
+class proof ~uri ~typ =
+ object
+ val mutable _status = new proofStatus ~uri ~typ
+ method status = _status
+ method setStatus s = _status <- s
+ end
+
+class tacticCommand ~(tactic:ProofEngineTypes.tactic) (status: proofStatus) =
+ object
+ val statusBackup = status#status
+
+ method execute () =
+ let (new_proof, new_goals) = tactic status#status in
+ status#setProof new_proof;
+ status#setGoal
+ (match new_goals, new_proof with
+ | goal :: _, _ -> Some goal
+ | [], (_, (goal, _, _) :: _, _, _) ->
+ (* the tactic left no open goal: let's choose the first open goal *)
+ (* TODO CSC: here we could implement and use a proof-tree like
+ * notion... *)
+ Some goal
+ | _, _ -> None);
+ status#notify ()
+
+ method undo () =
+ status#setStatus statusBackup;
+ status#notify ()
+ end
+
+let intros ?namer =
+ new tacticCommand
+ ~tactic:(PrimitiveTactics.intros_tac ?mk_fresh_name_callback:namer ())
+
+let reflexivity = new tacticCommand ~tactic:EqualityTactics.reflexivity_tac
+let symmetry = new tacticCommand ~tactic:EqualityTactics.symmetry_tac
+let transitivity term =
+ new tacticCommand ~tactic:(EqualityTactics.transitivity_tac ~term)
+
+let exists = new tacticCommand ~tactic:IntroductionTactics.exists_tac
+let split = new tacticCommand ~tactic:IntroductionTactics.split_tac
+let left = new tacticCommand ~tactic:IntroductionTactics.left_tac
+let right = new tacticCommand ~tactic:IntroductionTactics.right_tac
+
+let assumption = new tacticCommand ~tactic:VariousTactics.assumption_tac
+
--- /dev/null
+(* 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 proofStatus: uri:UriManager.uri -> typ:Cic.term ->
+ object
+ inherit MatitaTypes.subject
+
+ (** {3 properties} *)
+
+ method proof: ProofEngineTypes.proof
+ method setProof: ProofEngineTypes.proof -> unit
+
+ method goal: ProofEngineTypes.goal option
+ method setGoal: ProofEngineTypes.goal option -> unit
+
+ (** @raise MatitaTypes.No_proof *)
+ method status: ProofEngineTypes.status (* proof, goal *)
+ method setStatus: ProofEngineTypes.status -> unit
+
+ (** {3 actions} *)
+
+ (** return a pair of "xml" (as defined in Xml module) representing the *
+ * current proof type and body, respectively *)
+ method to_xml: Xml.token Stream.t * Xml.token Stream.t
+ end
+
+class proof: uri:UriManager.uri -> typ:Cic.term ->
+ object
+ (** {3 status} *)
+ method status: proofStatus
+ method setStatus: proofStatus -> unit
+ end
+
+(** {2 tactic commands builders} *)
+
+(* TODO these are just some examples, a lot of other tactics/tacticals must be
+ * added here *)
+
+val intros: ?namer:MatitaTypes.namer ->
+ proofStatus -> MatitaTypes.command
+
+val reflexivity: proofStatus -> MatitaTypes.command
+val symmetry: proofStatus -> MatitaTypes.command
+val transitivity: Cic.term -> proofStatus -> MatitaTypes.command
+
+val exists: proofStatus -> MatitaTypes.command
+val split: proofStatus -> MatitaTypes.command
+val left: proofStatus -> MatitaTypes.command
+val right: proofStatus -> MatitaTypes.command
+
+val assumption: proofStatus -> MatitaTypes.command
+
--- /dev/null
+(* 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/
+ *)
+
+ (** no current proof is available *)
+exception No_proof
+
+class type observer =
+ (* "observer" pattern *)
+ object
+ method update: unit -> unit
+ end
+
+class subject =
+ (* "observer" pattern *)
+ object
+ val mutable observers = []
+ method attach (o: observer) = observers <- o :: observers
+ method detach (o: observer) =
+ observers <- List.filter (fun o' -> o' != o) observers
+ method notify () = List.iter (fun o -> o#update ()) observers
+ end
+
+class type command =
+ (* "command" pattern *)
+ object
+ method execute: unit -> unit
+ method undo: unit -> unit
+ end
+
+(** {2 shorthands} *)
+
+type namer = ProofEngineTypes.mk_fresh_name_type
+
projects / helm.git / commitdiff