From b5d69130dd83587b5fb9cbb39251aaa8df8c456e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Apr 2004 10:41:14 +0000 Subject: [PATCH] snapshot --- helm/matita/.depend | 14 +-- helm/matita/Makefile.in | 11 ++- helm/matita/buildTimeConf.ml.in | 27 ++++++ helm/matita/configure.ac | 55 +++++++++++- helm/matita/matita.glade | 90 ++----------------- helm/matita/matita.ml | 137 ++++++----------------------- helm/matita/matitaGeneratedGui.ml | 76 ++++------------ helm/matita/matitaGeneratedGui.mli | 50 +++-------- helm/matita/matitaGtkMisc.ml | 54 ++++++++++++ helm/matita/matitaGtkMisc.mli | 17 ++++ helm/matita/matitaGui.ml | 20 +++-- helm/matita/matitaGui.mli | 11 ++- helm/matita/matitaProof.ml | 109 +++++++++++++++++++++++ helm/matita/matitaProof.mli | 74 ++++++++++++++++ helm/matita/matitaTypes.ml | 55 ++++++++++++ 15 files changed, 487 insertions(+), 313 deletions(-) create mode 100644 helm/matita/matitaProof.ml create mode 100644 helm/matita/matitaProof.mli create mode 100644 helm/matita/matitaTypes.ml diff --git a/helm/matita/.depend b/helm/matita/.depend index d6894d903..c369a7b52 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,9 +1,13 @@ 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 diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index c784b0be6..fb9f9cf5b 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -3,6 +3,7 @@ OCAMLFIND = @OCAMLFIND@ CAMLP4O = @CAMLP4O@ LABLGLADECC = @LABLGLADECC@ REQUIRES = @FINDLIB_REQUIRES@ +HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O) OCAML_THREADS_FLAGS = -thread @@ -14,11 +15,19 @@ CMOS = \ 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 $@ $^ diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index e69de29bb..525c678b4 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -0,0 +1,27 @@ +(* 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@;; + diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index cc8d14a13..2b8f535f0 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -1,5 +1,13 @@ 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" @@ -19,7 +27,14 @@ else 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) @@ -30,10 +45,44 @@ do 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 diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 6eba147fd..497470299 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -40,7 +40,7 @@ True - + True gtk-new 1 @@ -83,7 +83,7 @@ - + True gtk-open 1 @@ -104,7 +104,7 @@ - + True gtk-save 1 @@ -124,7 +124,7 @@ True - + True gtk-save-as 1 @@ -151,7 +151,7 @@ - + True gtk-quit 1 @@ -218,26 +218,8 @@ - + True - 0 - True - - - - - - True - 1 - True - - - - - - True - 2 - True @@ -1017,64 +999,4 @@ - - True - dialog1 - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - True - 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 - - - - - - - - - - diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 5056a88a2..59076c94e 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open MatitaGtkMisc + exception Not_implemented of string let not_implemented feature = raise (Not_implemented feature) @@ -34,121 +36,34 @@ let _ = Helm_registry.load_from "matita.conf.xml" 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 () + + (** *) +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 _ = -(* gui#uriChoices#easy_append "pippo"; *) -(* gui#uriChoices#list_store#clear (); *) - GtkThread.main () +let _ = GtkThread.main () diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index f912ef0f9..e110e1d92 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -32,10 +32,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -52,26 +52,26 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -80,10 +80,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -112,18 +112,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -441,41 +433,9 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () 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 (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 6b72a8b27..017b3cae6 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -6,20 +6,17 @@ class mainWin : 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 @@ -36,6 +33,7 @@ class mainWin : 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 @@ -46,20 +44,17 @@ class mainWin : 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 @@ -77,6 +72,7 @@ class mainWin : 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 @@ -284,26 +280,4 @@ class interpChoiceDialog : 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 diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index fc4fecc8f..a87700941 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -75,3 +75,57 @@ class stringListModel (tree_view: GTree.view) = 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: 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 + diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 03847ac87..6ad12a756 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -46,3 +46,20 @@ class stringListModel: 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 + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 16af24434..7161aa9e8 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -50,21 +50,17 @@ class gui file = 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 :> 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; @@ -90,11 +86,19 @@ class gui file = 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 @@ -104,7 +108,5 @@ class gui file = ignore (main#quitMenuItem#connect#activate callback); self#addKeyBinding GdkKeysyms._q callback - method uriChoices = uriChoices - end diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 734f1cefe..f7faab8c5 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -38,18 +38,21 @@ class gui : 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 diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml new file mode 100644 index 000000000..5612043f3 --- /dev/null +++ b/helm/matita/matitaProof.ml @@ -0,0 +1,109 @@ +(* 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 + diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli new file mode 100644 index 000000000..e74efdf7d --- /dev/null +++ b/helm/matita/matitaProof.mli @@ -0,0 +1,74 @@ +(* 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 + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml new file mode 100644 index 000000000..b26c2f677 --- /dev/null +++ b/helm/matita/matitaTypes.ml @@ -0,0 +1,55 @@ +(* 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 + -- 2.39.2