From 3cf0591648726eee39e584ce3572d15224cf39b7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 17:10:57 +0000 Subject: [PATCH] removed all old matita files (kept in attic) --- helm/matita/.cvsignore | 13 - helm/matita/Makefile.in | 101 -- helm/matita/TODO | 13 - helm/matita/buildTimeConf.ml.in | 36 - helm/matita/configure.ac | 104 -- helm/matita/matita.conf.xml.sample | 27 - helm/matita/matita.glade | 2519 --------------------------- helm/matita/matita.gladep | 8 - helm/matita/matita.gtkrc | 80 - helm/matita/matita.ml | 209 --- helm/matita/matitaCicMisc.ml | 71 - helm/matita/matitaCicMisc.mli | 48 - helm/matita/matitaConsole.ml | 246 --- helm/matita/matitaConsole.mli | 88 - helm/matita/matitaDb.ml | 144 -- helm/matita/matitaDb.mli | 28 - helm/matita/matitaDisambiguator.ml | 106 -- helm/matita/matitaDisambiguator.mli | 34 - helm/matita/matitaGeneratedGui.ml | 884 ---------- helm/matita/matitaGeneratedGui.mli | 506 ------ helm/matita/matitaGtkMisc.ml | 282 --- helm/matita/matitaGtkMisc.mli | 96 - helm/matita/matitaGui.ml | 235 --- helm/matita/matitaGui.mli | 68 - helm/matita/matitaInterpreter.ml | 678 ------- helm/matita/matitaInterpreter.mli | 33 - helm/matita/matitaMathView.ml | 511 ------ helm/matita/matitaMathView.mli | 95 - helm/matita/matitaMisc.ml | 149 -- helm/matita/matitaMisc.mli | 79 - helm/matita/matitaProof.ml | 155 -- helm/matita/matitaProof.mli | 59 - helm/matita/matitaScript.ml | 212 --- helm/matita/matitaScript.mli | 45 - helm/matita/matitaTypes.ml | 195 --- helm/matita/matitaTypes.mli | 233 --- helm/matita/matitac.ml | 113 -- helm/matita/tests/coercions.ma | 50 - 38 files changed, 8553 deletions(-) delete mode 100644 helm/matita/.cvsignore delete mode 100644 helm/matita/Makefile.in delete mode 100644 helm/matita/TODO delete mode 100644 helm/matita/buildTimeConf.ml.in delete mode 100644 helm/matita/configure.ac delete mode 100644 helm/matita/matita.conf.xml.sample delete mode 100644 helm/matita/matita.glade delete mode 100644 helm/matita/matita.gladep delete mode 100644 helm/matita/matita.gtkrc delete mode 100644 helm/matita/matita.ml delete mode 100644 helm/matita/matitaCicMisc.ml delete mode 100644 helm/matita/matitaCicMisc.mli delete mode 100644 helm/matita/matitaConsole.ml delete mode 100644 helm/matita/matitaConsole.mli delete mode 100644 helm/matita/matitaDb.ml delete mode 100644 helm/matita/matitaDb.mli delete mode 100644 helm/matita/matitaDisambiguator.ml delete mode 100644 helm/matita/matitaDisambiguator.mli delete mode 100644 helm/matita/matitaGeneratedGui.ml delete mode 100644 helm/matita/matitaGeneratedGui.mli delete mode 100644 helm/matita/matitaGtkMisc.ml delete mode 100644 helm/matita/matitaGtkMisc.mli delete mode 100644 helm/matita/matitaGui.ml delete mode 100644 helm/matita/matitaGui.mli delete mode 100644 helm/matita/matitaInterpreter.ml delete mode 100644 helm/matita/matitaInterpreter.mli delete mode 100644 helm/matita/matitaMathView.ml delete mode 100644 helm/matita/matitaMathView.mli delete mode 100644 helm/matita/matitaMisc.ml delete mode 100644 helm/matita/matitaMisc.mli delete mode 100644 helm/matita/matitaProof.ml delete mode 100644 helm/matita/matitaProof.mli delete mode 100644 helm/matita/matitaScript.ml delete mode 100644 helm/matita/matitaScript.mli delete mode 100644 helm/matita/matitaTypes.ml delete mode 100644 helm/matita/matitaTypes.mli delete mode 100644 helm/matita/matitac.ml delete mode 100644 helm/matita/tests/coercions.ma diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore deleted file mode 100644 index 381f91c1a..000000000 --- a/helm/matita/.cvsignore +++ /dev/null @@ -1,13 +0,0 @@ -Makefile -buildTimeConf.ml -config.status -configure -config.log -autom4te.cache -matita -matita.opt -matitac -matitac.opt -*.cm[aiox] -*.cmxa -*.[ao] diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in deleted file mode 100644 index 90a8a2a41..000000000 --- a/helm/matita/Makefile.in +++ /dev/null @@ -1,101 +0,0 @@ - -OCAMLFIND = @OCAMLFIND@ -CAMLP4O = @CAMLP4O@ -LABLGLADECC = @LABLGLADECC@ -REQUIRES = @FINDLIB_REQUIRES@ -CREQUIRES = @FINDLIB_CREQUIRES@ -HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ - -OCAML_FLAGS = -pp $(CAMLP4O) -PKGS = -package "$(REQUIRES)" -CPKGS = -package "$(CREQUIRES)" -OCAML_THREADS_FLAGS = -thread -OCAML_DEBUG_FLAGS = -g -OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) -OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) -OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) -# objects for matita (GTK GUI) -CMOS = \ - buildTimeConf.cmo \ - matitaMisc.cmo \ - matitaDb.cmo \ - matitaGeneratedGui.cmo \ - matitaTypes.cmo \ - matitaCicMisc.cmo \ - matitaGtkMisc.cmo \ - matitaConsole.cmo \ - matitaGui.cmo \ - matitaProof.cmo \ - matitaDisambiguator.cmo \ - matitaMathView.cmo \ - matitaInterpreter.cmo \ - matitaScript.cmo -# objects for matitac (batch compiler) -CCMOS = \ - buildTimeConf.cmo \ - matitaMisc.cmo \ - matitaDb.cmo \ - matitaTypes.cmo \ - matitaCicMisc.cmo \ - matitaProof.cmo \ - matitaDisambiguator.cmo \ - matitaInterpreter.cmo - -LIB_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) - -all: matita matitac cicbrowser - -ifeq ($(HAVE_OCAMLOPT),yes) -CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) -CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) -LIBX_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) -opt: matita.opt matitac.opt cicbrowser.opt -else -opt: - @echo "Native code compilation is disabled" -endif - -matita: $(LIB_DEPS) $(CMOS) matita.ml - $(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml -matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml - -matitac: $(LIB_DEPS) $(CCMOS) matitac.ml - $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml -matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml - -cicbrowser: matita - @test -f $@ || ln -s $< $@ -cicbrowser.opt: matita.opt - @test -f $@ || ln -s $< $@ - -matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade - $(LABLGLADECC) $< > matitaGeneratedGui.ml - $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli - -%.cmi: %.mli - $(OCAMLC) $(PKGS) -c $< -%.cmo %.cmi: %.ml - $(OCAMLC) $(PKGS) -c $< -%.cmx: %.ml - $(OCAMLOPT) $(PKGS) -c $< - -clean: - rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ - matita matita.opt matitac matitac.opt \ - cicbrowser cicbrowser.opt -distclean: clean - rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli - rm -f config.log config.status Makefile buildTimeConf.ml - rm -f matita.glade.bak matita.gladep.bak - rm -rf autom4te.cache/ - -depend: matitaGeneratedGui.ml matitaGeneratedGui.mli - $(OCAMLDEP) *.ml *.mli > .depend - -include .depend - -.PHONY: all opt clean distclean depend - diff --git a/helm/matita/TODO b/helm/matita/TODO deleted file mode 100644 index f64358119..000000000 --- a/helm/matita/TODO +++ /dev/null @@ -1,13 +0,0 @@ -- ricerca - - sintassi concreta (da controllare) - - hint -- script handling -- alias - - sintassi concreta - - generazione di alias dalla disambiguazione allo script -- console - - input (invio + punto) - - cut and paste - - scrolling -- menu contestuali / contesti per tattiche che richiedono argomenti -- linguaggio per la notazione diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in deleted file mode 100644 index 98c033fdb..000000000 --- a/helm/matita/buildTimeConf.ml.in +++ /dev/null @@ -1,36 +0,0 @@ -(* 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@;; -let version = "0.0.1";; -let undo_history_size = 10;; -let console_history_size = 100;; -let browser_history_size = 100;; -let gtkrc = "@MATITA_GTKRC@";; -let base_uri = "cic:/matita";; -let phrase_sep = ".";; -let blank_uri = "about:blank";; -let current_proof_uri = "about:current_proof";; - diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac deleted file mode 100644 index 1af1fca87..000000000 --- a/helm/matita/configure.ac +++ /dev/null @@ -1,104 +0,0 @@ -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" -else - AC_MSG_ERROR(could not find ocamlfind) -fi -AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc2, yes, no) -if test $HAVE_LABLGLADECC = "yes"; then - LABLGLADECC="lablgladecc2" -else - AC_MSG_ERROR(could not find lablgladecc2) -fi -AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no) -if test $HAVE_CAMLP4O = "yes"; then - CAMLP4O="camlp4o" -else - AC_MSG_ERROR(could not find camlp4o) -fi - -FINDLIB_CREQUIRES="\ -pcre \ -mysql \ -unix \ -helm-cic_omdoc \ -helm-cic_transformations \ -helm-registry \ -helm-tactics \ -helm-xml \ -helm-cic_textual_parser2 \ -" -FINDLIB_REQUIRES="\ -$FINDLIB_CREQUIRES \ -lablgtk2.glade \ -lablgtkmathview \ -helm-xmldiff \ -" -for r in $FINDLIB_REQUIRES -do - AC_MSG_CHECKING(for $r ocaml library) - if $OCAMLFIND query $r &> /dev/null; then - AC_MSG_RESULT(yes) - else - AC_MSG_ERROR(could not find $r ocaml library) - fi -done - -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 - -MATITA_GTKRC="matita.gtkrc" - -AC_SUBST(CAMLP4O) -AC_SUBST(DEBUG) -AC_SUBST(TRANSFORMER_MODULE) -AC_SUBST(FINDLIB_REQUIRES) -AC_SUBST(FINDLIB_CREQUIRES) -AC_SUBST(HAVE_OCAMLOPT) -AC_SUBST(LABLGLADECC) -AC_SUBST(OCAMLFIND) -AC_SUBST(MATITA_GTKRC) - -AC_OUTPUT([ - buildTimeConf.ml - Makefile -]) diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample deleted file mode 100644 index 61ab2d8d6..000000000 --- a/helm/matita/matita.conf.xml.sample +++ /dev/null @@ -1,27 +0,0 @@ - - -
- matita.glade - true - true - cic:/matita/ - .matita/xml - zack -
-
- - mowgli.cs.unibo.it - helm - - matita -
-
- - file:///projects/helm/library/coq_contribs - - .matita/getter/cache - .matita/getter/maps - /projects/helm/xml/dtd - -
- diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade deleted file mode 100644 index 809242945..000000000 --- a/helm/matita/matita.glade +++ /dev/null @@ -1,2519 +0,0 @@ - - - - - - - Matita: about - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - <b>Matita @VERSION@</b> - -<tt>http://helm.cs.unibo.it</tt> - -Copyright (C) 2004, -<i>the HELM team</i> - False - True - GTK_JUSTIFY_CENTER - False - False - 0.5 - 0.5 - 5 - 5 - - - 0 - False - False - - - - - - - - 400 - 500 - True - Cic browser - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - - - - True - True - False - - - - True - False - 0 - - - - True - GTK_SHADOW_OUT - GTK_POS_LEFT - GTK_POS_TOP - - - - True - False - 0 - - - - True - new browser win - True - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-new - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - history back - True - True - GTK_RELIEF_NORMAL - True - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - True - gtk-go-back - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - - - - 0 - False - False - - - - - - True - history forward - True - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-go-forward - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - refresh - True - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-refresh - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - home - True - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-home - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - True - - - - - - True - cic uri - True - True - True - 0 - - True - * - False - - - 0 - True - True - - - - - - - 0 - False - True - - - - - - True - 0 - 0 - GTK_SHADOW_NONE - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - - - - - - 0 - True - True - - - - - - - - - - DUMMY - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - DUMMY - False - False - GTK_JUSTIFY_CENTER - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - - - True - DUMMY - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -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 - - - - - - - - - - - - 10 - Select File - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - True - True - GTK_RELIEF_NORMAL - True - - - - - - True - True - True - GTK_RELIEF_NORMAL - True - - - - - - 200 - Interpretation choice - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - True - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-help - True - GTK_RELIEF_NORMAL - True - -11 - - - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - False - 0 - - - - True - some informative message here ... - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - True - True - False - False - False - True - - - - - 0 - True - True - - - - - 0 - True - True - - - - - - - - Matita - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - 800 - 600 - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - - - - True - True - False - - - - True - False - 0 - - - - True - - - - True - _File - True - - - - - - - True - _New - True - - - - True - gtk-new - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - - True - _Proof or definition ... - True - - - - - - True - (Co)Inductive _definitions ... - True - - - - - - - - - - True - _Open... - True - - - - - True - gtk-open - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - True - _Save - True - - - - - True - gtk-save - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - True - Save _As ... - True - - - - True - gtk-save-as - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - True - - - - - - True - _Quit - True - - - - - True - gtk-quit - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - - - - - True - _Edit - True - - - - - - True - _View - True - - - - - - - True - Show Button Bar - True - True - - - - - - True - New Cic Browser - True - - - - - - - True - Show Script Window - True - False - - - - - - - True - - - - - - True - Toggle console - True - - - - - - - - - - - True - Debug - True - - - - - - - True - - - - - - - - - - True - _Help - True - - - - - - - True - About... - True - - - - - - - - - 0 - False - False - - - - - - True - True - 450 - - - - True - True - True - True - GTK_POS_TOP - False - False - - - True - False - - - - - - True - True - False - - - - True - False - 0 - - - - True - False - 0 - - - - True - Hide console - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-close - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - 0 - False - False - - - - - - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - - - - 0 - True - True - - - - - - - True - False - - - - - 0 - True - True - - - - - - True - True - - - 0 - False - False - - - - - - - - - - Matita: script - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - 450 - 800 - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - - - - True - True - False - - - - True - False - 0 - - - - True - GTK_SHADOW_OUT - GTK_POS_LEFT - GTK_POS_TOP - - - - True - False - 0 - - - - True - restart - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-goto-top - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - go back 1 phrase - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-go-up - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - execute until point - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - go forward 1 phrase - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-go-down - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - True - execute all - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-goto-bottom - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - - - 0 - False - True - - - - - - True - True - True - True - GTK_POS_BOTTOM - False - False - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - True - True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 0 - 0 - 0 - - - - - - False - True - - - - - - True - script - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - tab - - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - True - True - False - False - False - True - - - - - False - True - - - - - - True - outline - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - tab - - - - - 0 - True - True - - - - - - - - - - DUMMY - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -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 - - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - True - True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 0 - 0 - 0 - - - - - - 0 - True - True - - - - - - - - 155 - 450 - Tactics - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - False - False - True - False - False - GDK_WINDOW_TYPE_HINT_UTILITY - GDK_GRAVITY_NORTH_WEST - - - - True - True - False - - - - True - False - 0 - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Intros - True - intros - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Apply - True - apply - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Exact - True - exact - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Elim - True - elim - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - ElimType - True - elimTy - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Split - True - split - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 25 - True - Left - True - L - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 25 - True - Right - True - R - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 25 - True - Exists - True - ∃ - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Reflexivity - True - refl - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Symmetry - True - sym - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Transitivity - True - trans - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Simplify - True - simpl - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Reduce - True - red - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Whd - True - whd - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Assumption - True - asum - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Auto - True - auto - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Cut - True - cut - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Replace - True - repl - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - - - - - 280 - Uri choice - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - - - - True - True - True - GTK_RELIEF_NORMAL - True - 0 - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - True - gtk-index - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - Try _Selected - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - - - - - - - True - False - True - True - Try Constants - True - GTK_RELIEF_NORMAL - True - 0 - - - - - - True - True - True - GTK_RELIEF_NORMAL - True - 0 - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - True - gtk-ok - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - _Auto - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - False - 0 - - - - True - some informative message here ... - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - True - True - False - False - False - True - - - - - 0 - True - True - - - - - - True - False - 0 - - - - True - URI: - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - True - True - True - 0 - - True - * - False - - - 0 - True - True - - - - - 0 - False - True - - - - - 0 - True - True - - - - - - - diff --git a/helm/matita/matita.gladep b/helm/matita/matita.gladep deleted file mode 100644 index cc3340fc9..000000000 --- a/helm/matita/matita.gladep +++ /dev/null @@ -1,8 +0,0 @@ - - - - - Matita - matita - FALSE - diff --git a/helm/matita/matita.gtkrc b/helm/matita/matita.gtkrc deleted file mode 100644 index 91081c311..000000000 --- a/helm/matita/matita.gtkrc +++ /dev/null @@ -1,80 +0,0 @@ -# Based on /usr/share/themes/Emacs/gtk-2.0-key/, -# modified by Zack for matita - -# -# A keybinding set implementing emacs-like keybindings -# - -# -# Bindings for GtkTextView and GtkEntry -# -binding "gtk-emacs-text-entry" -{ - bind "b" { "move-cursor" (logical-positions, -1, 0) } - bind "b" { "move-cursor" (logical-positions, -1, 1) } - bind "f" { "move-cursor" (logical-positions, 1, 0) } - bind "f" { "move-cursor" (logical-positions, 1, 1) } - - bind "b" { "move-cursor" (words, -1, 0) } - bind "b" { "move-cursor" (words, -1, 1) } - bind "f" { "move-cursor" (words, 1, 0) } - bind "f" { "move-cursor" (words, 1, 1) } - - bind "a" { "move-cursor" (paragraph-ends, -1, 0) } - bind "a" { "move-cursor" (paragraph-ends, -1, 1) } - bind "e" { "move-cursor" (paragraph-ends, 1, 0) } - bind "e" { "move-cursor" (paragraph-ends, 1, 1) } - - bind "w" { "cut-clipboard" () } - bind "y" { "paste-clipboard" () } - - bind "d" { "delete-from-cursor" (chars, 1) } - bind "d" { "delete-from-cursor" (word-ends, 1) } - bind "k" { "delete-from-cursor" (paragraph-ends, 1) } - bind "backslash" { "delete-from-cursor" (whitespace, 1) } - - bind "space" { "delete-from-cursor" (whitespace, 1) - "insert-at-cursor" (" ") } - bind "KP_Space" { "delete-from-cursor" (whitespace, 1) - "insert-at-cursor" (" ") } - - # - # Some non-Emacs keybindings people are attached to - # - bind "u" { - "move-cursor" (paragraph-ends, -1, 0) - "delete-from-cursor" (paragraph-ends, 1) - } - bind "h" { "delete-from-cursor" (chars, -1) } - bind "w" { "delete-from-cursor" (word-ends, -1) } -} - -# -# Bindings for GtkTextView -# -binding "gtk-emacs-text-view" -{ -# bind "p" { "move-cursor" (display-lines, -1, 0) } - bind "p" { "move-cursor" (display-lines, -1, 1) } -# bind "n" { "move-cursor" (display-lines, 1, 0) } - bind "n" { "move-cursor" (display-lines, 1, 1) } - - bind "space" { "set-anchor" () } - bind "KP_Space" { "set-anchor" () } -} - -# -# Bindings for GtkTreeView -# -binding "gtk-emacs-tree-view" -{ - bind "s" { "start-interactive-search" () } - bind "f" { "move-cursor" (logical-positions, 1) } - bind "b" { "move-cursor" (logical-positions, -1) } -} - -class "GtkEntry" binding "gtk-emacs-text-entry" -class "GtkTextView" binding "gtk-emacs-text-entry" -class "GtkTextView" binding "gtk-emacs-text-view" -class "GtkTreeView" binding "gtk-emacs-tree-view" - diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml deleted file mode 100644 index 3052e975e..000000000 --- a/helm/matita/matita.ml +++ /dev/null @@ -1,209 +0,0 @@ -(* 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/ - *) - -open Printf - -open MatitaGtkMisc -open MatitaTypes -open MatitaMisc - -(** {2 Initialization} *) - -let _ = - Helm_registry.load_from "matita.conf.xml"; (* read conf *) - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment (); - GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; (* loads gtk rc files *) - ignore (GMain.Main.init ()) - -let gui = MatitaGui.instance () -let disambiguator = MatitaDisambiguator.instance () -let _ = (* set disambiguator callbacks *) - disambiguator#setChooseUris (interactive_user_uri_choice ~gui); - disambiguator#setChooseInterp (interactive_interp_choice ~gui) - -let _ = (* environment trust *) - CicEnvironment.set_trust - (let trust = Helm_registry.get_bool "matita.environment_trust" in - fun _ -> trust) - -let currentProof = MatitaProof.instance () - -let sequent_viewer = MatitaMathView.sequent_viewer_instance () -let sequents_viewer = MatitaMathView.sequents_viewer_instance () -let _ = (* attach observers to proof status *) - let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in - let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) = - sequents_viewer#reset; - (match goal_opt with - | None -> () - | Some goal -> - sequents_viewer#load_sequents metasenv; - sequents_viewer#goto_sequent goal) - in - currentProof#addObserver sequents_observer; - currentProof#addObserver browser_observer; - currentProof#connect `Quit (fun () -> - (* quit program, asking for confirmation if needed *) - if not (currentProof#onGoing ()) || - (ask_confirmation ~gui - ~msg:("Proof in progress, are you sure you want to quit?") ()) - then - GMain.Main.quit (); - false); - currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) - -let interpreter = - let mathViewer = MatitaMathView.mathViewer () in - MatitaInterpreter.interpreter ~console:gui#console ~mathViewer () -let script = MatitaScript.script ~interpreter -let _ = - let href_callback uri = - let term = CicAst.Uri (uri, None) in - ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term))) - in - sequent_viewer#set_href_callback (Some href_callback) - -let console_callback s = - let module A = TacticAst in - let rec strip_locations = function - | A.LocatedTactical (loc, tac) -> strip_locations tac - | tac -> tac - in - let needed_by_script ast = - match strip_locations ast with - | A.Tactic _ - | A.Command - (A.Inductive _ | A.Theorem _ | A.Coercion _ | A.Qed _ | A.Proof) -> - true - | _ -> false - in - let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in - debug_print (sprintf "evaluating '%s'" s); - if needed_by_script ast then - script#advance s - else - interpreter#evalAst ast - -let console_callback s = - match gui#console#wrap_exn (fun () -> console_callback s) with - | None -> (false, false) - | Some outcome -> outcome - -(** {2 GUI callbacks} *) - -let _ = - gui#setQuitCallback currentProof#quit; - gui#setPhraseCallback console_callback; - gui#main#debugMenu#misc#hide (); - ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> - gui#console#clear (); - gui#console#show ~msg:"theorem " ())); - ignore (gui#main#openMenuItem#connect#activate (fun _ -> - match gui#chooseFile () with - | None -> () - | Some f when is_proof_script f -> - ignore (gui#console#wrap_exn (fun () -> script#loadFrom f)) - | Some f -> - gui#console#echo_error (sprintf - "Don't know what to do with file: %s\nUnrecognized file format." - f))); - ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> - ignore (MatitaMathView.cicBrowser ()))); - let module A = TacticAst in - let hole = CicAst.UserInput in - let tac ast _ = - let ast = A.Tactic ast in - ignore (script#advance (TacticAstPp.pp_tactical ast)) - in - let tac_w_term ast _ = -(* gui#console#clear (); *) - gui#console#show ~msg:(TacticAstPp.pp_tactic ast) (); - gui#main#mainWin#present () - in - let tbar = gui#toolbar in - connect_button tbar#introsButton (tac (A.Intros (None, []))); - connect_button tbar#applyButton (tac_w_term (A.Apply hole)); - connect_button tbar#exactButton (tac_w_term (A.Exact hole)); - connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None))); - connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole)); - connect_button tbar#splitButton (tac A.Split); - connect_button tbar#leftButton (tac A.Left); - connect_button tbar#rightButton (tac A.Right); - connect_button tbar#existsButton (tac A.Exists); - connect_button tbar#reflexivityButton (tac A.Reflexivity); - connect_button tbar#symmetryButton (tac A.Symmetry); - connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole)); - connect_button tbar#assumptionButton (tac A.Assumption); - connect_button tbar#cutButton (tac_w_term (A.Cut hole)); - connect_button tbar#autoButton (tac A.Auto) - - (** *) - -let _ = - if BuildTimeConf.debug then begin - gui#main#debugMenu#misc#show (); - let addDebugItem ~label callback = - let item = - GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label () - in - ignore (item#connect#activate callback) - in - addDebugItem "dump environment to \"env.dump\"" (fun _ -> - let oc = open_out "env.dump" in - CicEnvironment.dump_to_channel oc; - close_out oc); - addDebugItem "print selected terms" (fun () -> - let i = ref 0 in - List.iter - (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t))) - sequent_viewer#get_selected_terms); - addDebugItem "dump getter settings" (fun _ -> - prerr_endline (Http_getter_env.env_to_string ())); - addDebugItem "getter: update" Http_getter.update; - addDebugItem "getter: getalluris" (fun _ -> - List.iter prerr_endline (Http_getter.getalluris ())); - end - - (** *) - -let _ = - (try script#loadFrom Sys.argv.(1) with Invalid_argument _ -> ()); - if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *) - Helm_registry.set "matita.mode" "cicbrowser"; - let browser = MatitaMathView.cicBrowser () in - try - browser#loadUri Sys.argv.(1) - with Invalid_argument _ -> () - end else begin (* matita *) - Helm_registry.set "matita.mode" "matita"; - gui#main#mainWin#show (); - gui#toolbar#toolBarWin#show (); - gui#console#show () - end; - GtkThread.main () - diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml deleted file mode 100644 index dbb80c791..000000000 --- a/helm/matita/matitaCicMisc.ml +++ /dev/null @@ -1,71 +0,0 @@ -(* 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/ - *) - -open Printf - - (** create a Cic.CurrentProof from a given proof *) -let cicCurrentProof (uri, metasenv, bo, ty) = - let uri = MatitaTypes.unopt_uri uri in - (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [], []) - - (** create a Cic.Constant from a given proof *) -let cicConstant (uri, metasenv, bo, ty) = - let uri = MatitaTypes.unopt_uri uri in - (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], []) - -let canonical_context metano metasenv = - try - let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in - context - with Not_found -> - failwith (sprintf "Can't find canonical context for %d" metano) - - (** term AST -> Cic.term. Uses disambiguator and change imperatively the - * metasenv as needed *) -let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast = - if currentProof#onGoing () then begin - let proof = currentProof#proof in - let metasenv = proof#metasenv in - let goal = proof#goal in - let context = canonical_context goal metasenv in - let (_, metasenv, term,ugraph) as retval = - disambiguator#disambiguateTermAst ~context ~metasenv ast - in - proof#set_metasenv metasenv; - retval - end else - disambiguator#disambiguateTermAst ast - -let get_context_and_metasenv ~(currentProof:#MatitaTypes.currentProof) = - if currentProof#onGoing () then - let proof = currentProof#proof in - let metasenv = proof#metasenv in - let goal = proof#goal in - (canonical_context goal metasenv, metasenv) - else - ([], []) - diff --git a/helm/matita/matitaCicMisc.mli b/helm/matita/matitaCicMisc.mli deleted file mode 100644 index 3d0de435f..000000000 --- a/helm/matita/matitaCicMisc.mli +++ /dev/null @@ -1,48 +0,0 @@ -(* 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/ - *) - - (** build a CurrentProof object *) -val cicCurrentProof: - UriManager.uri option * Cic.metasenv * Cic.term * Cic.term -> - Cic.obj - - (** build a Constant object *) -val cicConstant: UriManager.uri option * 'a * Cic.term * Cic.term -> Cic.obj - -val canonical_context: int -> (int * 'a * 'b) list -> 'a - - (** term AST -> Cic.term. Uses disambiguator and change imperatively the - * metasenv as needed *) -val disambiguate : - disambiguator:MatitaTypes.disambiguator -> - currentProof:#MatitaTypes.currentProof -> - DisambiguateTypes.term -> - DisambiguateTypes.environment * Cic.metasenv * Cic.term * - CicUniv.universe_graph - -val get_context_and_metasenv: - currentProof:#MatitaTypes.currentProof -> - Cic.context * Cic.metasenv - diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml deleted file mode 100644 index 8dc43a093..000000000 --- a/helm/matita/matitaConsole.ml +++ /dev/null @@ -1,246 +0,0 @@ -(* 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/ - *) - -open Printf - -open MatitaTypes - -type callback = string -> command_outcome - -let default_prompt = "# " -let default_phrase_sep = "." -let default_callback = fun (phrase: string) -> (true, true) -let bullet = "∙" - -let message_props = [ `STYLE `ITALIC ] -let error_props = [ `WEIGHT `BOLD ] -let prompt_props = [ ] - -let trailing_NL_RE = Pcre.regexp "\n\\s*$" - -class console - ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj -= - let console_height = 100 in (* pixels *) - object (self) - inherit GText.view obj - - val mutable _phrase_sep = phrase_sep - method phrase_sep = _phrase_sep - method set_phrase_sep sep = _phrase_sep <- sep - - val mutable _prompt = prompt - method prompt = _prompt - method set_prompt prompt = _prompt <- prompt - - val mutable _callback = callback - method set_callback f = _callback <- f - - val mutable _ignore_insert_text_signal = false - method ignore_insert_text_signal ignore = - _ignore_insert_text_signal <- ignore - - val history = - new MatitaMisc.shell_history BuildTimeConf.console_history_size - - val mutable handle_position = 450 - val mutable last_phrase = "" - - initializer - let buf = self#buffer in - self#set_wrap_mode `CHAR; - self#hide (); - (* create "USER_INPUT_START" mark. This mark will always point to the - * beginning of user input not yet processed *) - ignore (buf#create_mark ~name:"USER_INPUT_START" - ~left_gravity:true buf#start_iter); - MatitaGtkMisc.connect_key self#event ~modifiers:[`CONTROL] ~stop:true - GdkKeysyms._Return - (fun () -> - buf#insert ~iter:buf#end_iter "\n"; - let inserted_text = - MatitaMisc.strip_trailing_blanks - (buf#get_text - ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) - ~stop:buf#end_iter ()) - in - self#invoke_callback inserted_text; - self#echo_prompt ()); - -(* - (* callback handling based on phrase terminator (e.g. ";;" at the end of - * the row: each time a character is inserted *) - ignore (buf#connect#after#insert_text (fun iter text -> - if (not _ignore_insert_text_signal) && - (iter#compare buf#end_iter = 0) && (* insertion at end *) - (Pcre.pmatch ~rex:trailing_NL_RE text) - then - let inserted_text = - MatitaMisc.strip_trailing_blanks - (buf#get_text - ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) - ~stop:buf#end_iter ()) - in - let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in - if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *) - self#lock; - last_phrase <- inserted_text; - self#invoke_callback inserted_text; - self#echo_prompt () - end)); -*) - (match evbox with (* history key bindings *) - | None -> () - | Some evbox -> - List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox) - [ GdkKeysyms._p, (fun () -> self#previous_phrase); - GdkKeysyms._n, (fun () -> self#next_phrase); - ]); - ignore (self#connect#after#move_cursor - (* avoid cursor being placed at prompt's left *) - ~callback:(fun step count ~extend -> - let buf = self#buffer in - let cursor_iter = buf#get_iter_at_mark `INSERT in - let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in - if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *) - buf#place_cursor ~where:prompt_iter)) - - method private set_phrase phrase = - let buf = self#buffer in - buf#delete - ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) - ~stop:buf#end_iter; - buf#insert ~iter:buf#end_iter phrase - - method private invoke_callback phrase = - history#add phrase; - let (success, hide) = _callback phrase in - if hide then self#hide () - - method clear () = - let buf = self#buffer in - buf#delete ~start:buf#start_iter ~stop:buf#end_iter - - (* lock old text and bump USER_INPUT_START mark *) - method private lock = - let buf = self#buffer in - let read_only = buf#create_tag [`EDITABLE false] in - buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter; - buf#move_mark (`NAME "USER_INPUT_START") buf#end_iter - - method echo_prompt () = - let buf = self#buffer in - self#ignore_insert_text_signal true; - buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag prompt_props] prompt; - self#ignore_insert_text_signal false; - self#lock - - method echo_message msg = - self#show (); - let buf = self#buffer in - self#ignore_insert_text_signal true; - buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props] - (msg ^ "\n"); - self#ignore_insert_text_signal false; - self#lock - - method echo_error msg = - self#show (); - let buf = self#buffer in - self#ignore_insert_text_signal true; - buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] - (msg ^ "\n"); - self#ignore_insert_text_signal false; - self#lock - - method private get_paned_prop s = - Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int } - paned#as_widget - method private get_position = self#get_paned_prop "position" - method private get_min_position = self#get_paned_prop "min-position" - method private get_max_position = self#get_paned_prop "max-position" - - method show ?(msg = "") () = - self#buffer#insert msg; - paned#set_position (self#get_max_position - console_height); - self#misc#grab_focus () - method hide () = (* ZACK still not sure about the gui, for the moment just - * keep the console persistent *) - () -(* paned#set_position self#get_max_position *) - method toggle () = - let pos = self#get_position in - if pos > self#get_max_position - console_height then - self#show () - else - self#hide () - - (** navigation methods: history, cursor motion, ... *) - - method private previous_phrase = - try self#set_phrase history#previous with MatitaMisc.History_failure -> () - method private next_phrase = - try self#set_phrase history#next with MatitaMisc.History_failure -> () - - method wrap_exn: 'a. (unit -> 'a) -> 'a option = - fun f -> - try - Some (f ()) - with exn -> - (match exn with (* highlight parse errors in user input *) - | CicTextualParser2.Parse_error (floc, msg) -> - let buf = self#buffer in - let (x, y) = CicAst.loc_of_floc floc in - let red = buf#create_tag [`FOREGROUND "red"] in - let (start_error_pos, end_error_pos) = - buf#end_iter#backward_chars (String.length last_phrase - x), - buf#end_iter#backward_chars (String.length last_phrase - y) - in - if x - y = 0 then (* no region to highlight, let's add an hint - about where the error occured *) - buf#insert ~iter:end_error_pos ~tags:[red] bullet - else (* highlight the region where the error occured *) - buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos; - | _ -> ()); - self#echo_error (explain exn); - None - - end - -let console - ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) ?evbox ~paned - ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width - ?width ?height ?packing ?show () -= - let view = - GText.view - ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width - ?width ?height ?packing ?show () - in - new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view - -(* vim: set encoding=utf8: *) diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli deleted file mode 100644 index d0d1a53d3..000000000 --- a/helm/matita/matitaConsole.mli +++ /dev/null @@ -1,88 +0,0 @@ -(* 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/ - *) - -type callback = string -> MatitaTypes.command_outcome - - (** @param evbox event box to which keyboard shortcuts are registered; no - * shortcut will be registered if evbox is not given *) -class console: - ?prompt:string -> ?phrase_sep:string -> ?callback:callback -> - ?evbox:GBin.event_box -> paned:GPack.paned -> Gtk.text_view Gtk.obj -> - object - inherit GText.view - - method echo_prompt : unit -> unit - method echo_message : string -> unit - method echo_error : string -> unit - method clear : unit -> unit - - (* console visibility handling inside VPaned *) - - (** @param msg if given, show the console with a prefeed input, cursor - * just after it; defaults to the empty string *) - method show : ?msg:string -> unit -> unit - method hide : unit -> unit - method toggle : unit -> unit - - method prompt : string - method set_prompt : string -> unit - - method phrase_sep : string - method set_phrase_sep : string -> unit - - (** override previous callback definition *) - method set_callback : callback -> unit - - method ignore_insert_text_signal: bool -> unit - - (** execute a unit -> 'a function, if it raises exceptions shows them as - * errors in the console. - * @return Some of the returned value if the given function suceeds, None - * otherwise *) - method wrap_exn : 'a. (unit -> 'a) -> 'a option - end - - (** @param prompt user prompt (default "# ") - * @param phrase_sep phrase separator (default ".") - * @param callback callback invoked upon reading of a phrase. Callback - * may be invoked more than once if multiple phrases have been inserted before - * hitting return (default: do nothing) *) -val console : - ?prompt:string -> - ?phrase_sep:string -> - ?callback:callback -> - ?evbox:GBin.event_box -> - paned:GPack.paned -> - - ?buffer:GText.buffer -> - ?editable:bool -> - ?cursor_visible:bool -> - ?justification:Gtk.Tags.justification -> - ?wrap_mode:Gtk.Tags.wrap_mode -> - ?border_width:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> console - diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml deleted file mode 100644 index b2c97789d..000000000 --- a/helm/matita/matitaDb.ml +++ /dev/null @@ -1,144 +0,0 @@ -(* 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/ - *) - -open Printf ;; - -let xpointer_RE = Pcre.regexp "#.*$" - -let clean_owner_environment () = - let dbd = MatitaMisc.dbd_instance () in - let owner = (Helm_registry.get "matita.owner") in - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - let conclno_tbl = MetadataTypes.conclno_tbl () in - let conclno_hyp_tbl = MetadataTypes.conclno_hyp_tbl () in - let statements = [ - sprintf "DROP TABLE %s ;" obj_tbl; - sprintf "DROP TABLE %s ;" sort_tbl; - sprintf "DROP TABLE %s ;" rel_tbl; - sprintf "DROP TABLE %s ;" name_tbl; - sprintf "DROP TABLE %s ;" conclno_tbl; - sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in -(* -DROP INDEX refObj_source ON refObj (source); -DROP INDEX refObj_target ON refObj (h_occurrence); -DROP INDEX refObj_position ON refObj (h_position); -DROP INDEX refSort_source ON refSort (source); -DROP INDEX objectName_value ON objectName (value); -DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source); -DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no); -DROP INDEX no_concl_hyp_source ON no_concl_hyp (source); -DROP INDEX no_concl_hyp_no ON no_concl_hyp (no); -*) - let owned_uris = - try - MetadataDb.clean ~dbd - with Mysql.Error _ as exn -> - match Mysql.errno dbd with - | Mysql.No_such_table -> [] - | _ -> raise exn - in - List.iter - (fun uri -> - let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in - List.iter - (fun suffix -> Http_getter.unregister (uri ^ suffix)) - [""; ".body"; ".types"]) - owned_uris; - List.iter (fun statement -> - try - ignore (Mysql.exec dbd statement) - with Mysql.Error _ as exn -> - match Mysql.errno dbd with - | Mysql.Bad_table_error -> () - | _ -> raise exn - ) statements; -;; - -let create_owner_environment () = - let dbd = MatitaMisc.dbd_instance () in - let owner = (Helm_registry.get "matita.owner") in - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - let conclno_tbl = MetadataTypes.conclno_tbl () in - let conclno_hyp_tbl = MetadataTypes.conclno_hyp_tbl () in - let statements = [ - sprintf "CREATE TABLE %s ( - source varchar(255) binary not null, - h_occurrence varchar(255) binary not null, - h_position varchar(255) binary not null, - h_depth integer - );" obj_tbl; - sprintf "CREATE TABLE %s ( - source varchar(255) binary not null, - h_position varchar(255) binary not null, - h_depth integer not null, - h_sort varchar(255) binary not null - );" sort_tbl; - sprintf "CREATE TABLE %s ( - source varchar(255) binary not null, - h_position varchar(255) binary not null, - h_depth integer not null - );" rel_tbl; - sprintf "CREATE TABLE %s ( - source varchar(255) binary not null, - value varchar(255) binary not null - );" name_tbl; - sprintf "CREATE TABLE %s ( - source varchar(255) binary not null, - no tinyint(4) not null - );" conclno_tbl; - sprintf "CREATE TABLE %s ( - source varchar(255) binary not null, - no tinyint(4) not null - );" conclno_hyp_tbl ] in -(* -CREATE INDEX refObj_source ON refObj (source); -CREATE INDEX refObj_target ON refObj (h_occurrence); -CREATE INDEX refObj_position ON refObj (h_position); -CREATE INDEX refSort_source ON refSort (source); -CREATE INDEX objectName_value ON objectName (value); -CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source); -CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no); -CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source); -CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no); -*) - List.iter (fun statement -> - try - ignore (Mysql.exec dbd statement) - with - exn -> - let status = Mysql.status dbd in - match status with - | Mysql.StatusError Mysql.Table_exists_error -> () - | Mysql.StatusError _ -> raise exn - | _ -> () - ) statements -;; - diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli deleted file mode 100644 index 32b816000..000000000 --- a/helm/matita/matitaDb.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* 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/ - *) - -val clean_owner_environment : unit -> unit -val create_owner_environment : unit -> unit - diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml deleted file mode 100644 index 178c7d8c7..000000000 --- a/helm/matita/matitaDisambiguator.ml +++ /dev/null @@ -1,106 +0,0 @@ -(* 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/ - *) - -open MatitaTypes - -class parserr () = - object - method parseTerm = CicTextualParser2.parse_term - method parseTactical = CicTextualParser2.parse_tactical - end - -let parserr () = new parserr () -let parserr_instance = MatitaMisc.singleton parserr - -class disambiguator () = - let _chooseUris = ref mono_uris_callback in - let _chooseInterp = ref mono_interp_callback in - let disambiguate_term = - let module Callbacks = - struct - let interactive_user_uri_choice - ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg - ~id uris - = - !_chooseUris ~selection_mode ~title ~msg - ~nonvars_button:enable_button_for_non_vars uris - - let interactive_interpretation_choice interp = !_chooseInterp interp - - let input_or_locate_uri ~(title:string) ?id = - (* Zack: I try to avoid using this callback. I therefore assume that - * the presence of an identifier that can't be resolved via "locate" - * query is a syntax error *) - let msg = match id with Some id -> id | _ -> "_" in - raise (Unbound_identifier msg) - end - in - let module Disambiguator = Disambiguate.Make (Callbacks) in - Disambiguator.disambiguate_term - in - object (self) - val mutable _env = DisambiguateTypes.Environment.empty - method env = _env - method setEnv e = _env <- e - - method chooseUris = !_chooseUris - method setChooseUris f = _chooseUris := f - - method chooseInterp = !_chooseInterp - method setChooseInterp f = _chooseInterp := f - - val parserr = parserr_instance () - method parserr = parserr - - val dbd = MatitaMisc.dbd_instance () - - method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst = - let (save_state, env) = - match env with - | Some env -> (false, env) - | None -> (true, _env) - in - match disambiguate_term ~initial_ugraph:CicUniv.empty_ugraph - ~dbd context metasenv termAst ~aliases:env with - | [ (env, metasenv, term,ugraph) as x ] -> - if save_state then self#setEnv env; - x - | _ -> assert false - - method disambiguateTermAsts ?(metasenv = []) ?env asts = - let ast = CicAst.pack asts in - let (env, metasenv, term, ugraph) = - self#disambiguateTermAst ~context:[] ~metasenv ?env ast - in - (env, metasenv, CicUtil.unpack term, ugraph) - - method disambiguateTerm ?context ?metasenv ?env stream = - self#disambiguateTermAst ?context ?metasenv ?env - (parserr#parseTerm stream) - end - -let disambiguator () = new disambiguator () -let instance = MatitaMisc.singleton disambiguator - diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli deleted file mode 100644 index 7def4dc70..000000000 --- a/helm/matita/matitaDisambiguator.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* 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/ - *) - -val parserr: unit -> MatitaTypes.parserr -val disambiguator: unit -> MatitaTypes.disambiguator - - (** singleton parser instance *) -val parserr_instance: unit -> MatitaTypes.parserr - - (** singleton disambiguator instance *) -val instance: unit -> MatitaTypes.disambiguator - diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml deleted file mode 100644 index c7d13dfbd..000000000 --- a/helm/matita/matitaGeneratedGui.ml +++ /dev/null @@ -1,884 +0,0 @@ -(* Automatically generated from matita.glade by lablgladecc *) - -class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"AboutWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val aboutWin = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata)) - method aboutWin = aboutWin - val dialog_vbox2 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox2" ~info:"GtkVBox" xmldata)) - method dialog_vbox2 = dialog_vbox2 - val dialog_action_area2 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area2" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area2 = dialog_action_area2 - val aboutDismissButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata)) - method aboutDismissButton = aboutDismissButton - val aboutLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"AboutLabel" ~info:"GtkLabel" xmldata)) - method aboutLabel = aboutLabel - method reparent parent = - dialog_vbox2#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"BrowserWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val browserWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) - method browserWin = browserWin - val browserWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata)) - method browserWinEventBox = browserWinEventBox - val browserVBox = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata)) - method browserVBox = browserVBox - val handlebox1 = - new GBin.handle_box (GtkBin.HandleBox.cast - (Glade.get_widget_msg ~name:"handlebox1" ~info:"GtkHandleBox" xmldata)) - method handlebox1 = handlebox1 - val hbox7 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata)) - method hbox7 = hbox7 - val browserNewButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata)) - method browserNewButton = browserNewButton - val image191 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata)) - method image191 = image191 - val browserBackButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata)) - method browserBackButton = browserBackButton - val alignment3 = - new GBin.alignment (GtkBin.Alignment.cast - (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata)) - method alignment3 = alignment3 - val hbox6 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata)) - method hbox6 = hbox6 - val image188 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata)) - method image188 = image188 - val label10 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata)) - method label10 = label10 - val browserForwardButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata)) - method browserForwardButton = browserForwardButton - val image189 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata)) - method image189 = image189 - val browserRefreshButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata)) - method browserRefreshButton = browserRefreshButton - val image229 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata)) - method image229 = image229 - val browserHomeButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata)) - method browserHomeButton = browserHomeButton - val image190 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata)) - method image190 = image190 - val image187 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata)) - method image187 = image187 - val browserUri = - new GEdit.entry (GtkEdit.Entry.cast - (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata)) - method browserUri = browserUri - val frame1 = - new GBin.frame (GtkBin.Frame.cast - (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata)) - method frame1 = frame1 - val scrolledBrowser = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata)) - method scrolledBrowser = scrolledBrowser - method reparent parent = - browserWinEventBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val confirmationDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) - method confirmationDialog = confirmationDialog - val dialog_vbox1 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata)) - method dialog_vbox1 = dialog_vbox1 - val dialog_action_area1 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area1 = dialog_action_area1 - val confirmationDialogCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata)) - method confirmationDialogCancelButton = confirmationDialogCancelButton - val confirmationDialogOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata)) - method confirmationDialogOkButton = confirmationDialogOkButton - val confirmationDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata)) - method confirmationDialogLabel = confirmationDialogLabel - method reparent parent = - dialog_vbox1#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val emptyDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) - method emptyDialog = emptyDialog - val emptyDialogVBox = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata)) - method emptyDialogVBox = emptyDialogVBox - val dialog_action_area5 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area5 = dialog_action_area5 - val emptyDialogCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata)) - method emptyDialogCancelButton = emptyDialogCancelButton - val emptyDialogOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata)) - method emptyDialogOkButton = emptyDialogOkButton - val emptyDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata)) - method emptyDialogLabel = emptyDialogLabel - method reparent parent = - emptyDialogVBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"FileSelectionWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.file_selection (GtkWindow.FileSelection.cast - (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) - method toplevel = toplevel - val fileSelectionWin = - new GWindow.file_selection (GtkWindow.FileSelection.cast - (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) - method fileSelectionWin = fileSelectionWin - val fileSelCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata)) - method fileSelCancelButton = fileSelCancelButton - val fileSelOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata)) - method fileSelOkButton = fileSelOkButton - method check_widgets () = () - end -class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val interpChoiceDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata)) - method interpChoiceDialog = interpChoiceDialog - val dialog_vbox4 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox4" ~info:"GtkVBox" xmldata)) - method dialog_vbox4 = dialog_vbox4 - val dialog_action_area4 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area4" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area4 = dialog_action_area4 - val interpChoiceHelpButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"InterpChoiceHelpButton" ~info:"GtkButton" xmldata)) - method interpChoiceHelpButton = interpChoiceHelpButton - val interpChoiceCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"InterpChoiceCancelButton" ~info:"GtkButton" xmldata)) - method interpChoiceCancelButton = interpChoiceCancelButton - val interpChoiceOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"InterpChoiceOkButton" ~info:"GtkButton" xmldata)) - method interpChoiceOkButton = interpChoiceOkButton - val vbox3 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata)) - method vbox3 = vbox3 - val interpChoiceDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata)) - method interpChoiceDialogLabel = interpChoiceDialogLabel - val scrolledwindow4 = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow4 = scrolledwindow4 - val interpChoiceTreeView = - new GTree.view (GtkTree.TreeView.cast - (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata)) - method interpChoiceTreeView = interpChoiceTreeView - method reparent parent = - dialog_vbox4#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"MainWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val mainWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) - method mainWin = mainWin - val mainWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata)) - method mainWinEventBox = mainWinEventBox - val mainWinShape = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata)) - method mainWinShape = mainWinShape - val mainMenuBar = - new GMenu.menu_shell (GtkMenu.MenuBar.cast - (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata)) - method mainMenuBar = mainMenuBar - val fileMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata)) - method fileMenu = fileMenu - val fileMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata)) - method fileMenu_menu = fileMenu_menu - val newMenu = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata)) - method newMenu = newMenu - val image224 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata)) - method image224 = image224 - val newMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) - method newMenu_menu = newMenu_menu - val newProofMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata)) - method newProofMenuItem = newProofMenuItem - val newDefsMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata)) - method newDefsMenuItem = newDefsMenuItem - val openMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method openMenuItem = openMenuItem - val image225 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata)) - method image225 = image225 - val saveMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method saveMenuItem = saveMenuItem - val image226 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata)) - method image226 = image226 - val saveAsMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method saveAsMenuItem = saveAsMenuItem - val image227 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata)) - method image227 = image227 - val separator1 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) - method separator1 = separator1 - val quitMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method quitMenuItem = quitMenuItem - val image228 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata)) - method image228 = image228 - val editMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) - method editMenu = editMenu - val viewMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata)) - method viewMenu = viewMenu - val viewMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata)) - method viewMenu_menu = viewMenu_menu - val showToolBarMenuItem = - new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast - (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata)) - method showToolBarMenuItem = showToolBarMenuItem - val newCicBrowserMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata)) - method newCicBrowserMenuItem = newCicBrowserMenuItem - val showScriptMenuItem = - new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast - (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata)) - method showScriptMenuItem = showScriptMenuItem - val separator3 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata)) - method separator3 = separator3 - val showConsoleMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata)) - method showConsoleMenuItem = showConsoleMenuItem - val debugMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) - method debugMenu = debugMenu - val debugMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata)) - method debugMenu_menu = debugMenu_menu - val separator2 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata)) - method separator2 = separator2 - val helpMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata)) - method helpMenu = helpMenu - val helpMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata)) - method helpMenu_menu = helpMenu_menu - val aboutMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata)) - method aboutMenuItem = aboutMenuItem - val mainVPanes = - new GPack.paned (GtkPack.Paned.cast - (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata)) - method mainVPanes = mainVPanes - val sequentsNotebook = - new GPack.notebook (GtkPack.Notebook.cast - (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata)) - method sequentsNotebook = sequentsNotebook - val consoleEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata)) - method consoleEventBox = consoleEventBox - val consoleHBox = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata)) - method consoleHBox = consoleHBox - val vbox6 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata)) - method vbox6 = vbox6 - val hideConsoleButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata)) - method hideConsoleButton = hideConsoleButton - val image169 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata)) - method image169 = image169 - val scrolledConsole = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata)) - method scrolledConsole = scrolledConsole - val mainStatusBar = - new GMisc.statusbar (GtkMisc.Statusbar.cast - (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata)) - method mainStatusBar = mainStatusBar - method reparent parent = - mainWinEventBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"ScriptWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ScriptWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val scriptWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ScriptWin" ~info:"GtkWindow" xmldata)) - method scriptWin = scriptWin - val scriptWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata)) - method scriptWinEventBox = scriptWinEventBox - val vbox7 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata)) - method vbox7 = vbox7 - val handlebox2 = - new GBin.handle_box (GtkBin.HandleBox.cast - (Glade.get_widget_msg ~name:"handlebox2" ~info:"GtkHandleBox" xmldata)) - method handlebox2 = handlebox2 - val hbox8 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox8" ~info:"GtkHBox" xmldata)) - method hbox8 = hbox8 - val scriptWinTopButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ScriptWinTopButton" ~info:"GtkButton" xmldata)) - method scriptWinTopButton = scriptWinTopButton - val image235 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image235" ~info:"GtkImage" xmldata)) - method image235 = image235 - val scriptWinBackButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata)) - method scriptWinBackButton = scriptWinBackButton - val image237 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image237" ~info:"GtkImage" xmldata)) - method image237 = image237 - val scriptWinJumpButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ScriptWinJumpButton" ~info:"GtkButton" xmldata)) - method scriptWinJumpButton = scriptWinJumpButton - val image134 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image134" ~info:"GtkImage" xmldata)) - method image134 = image134 - val scriptWinForwardButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ScriptWinForwardButton" ~info:"GtkButton" xmldata)) - method scriptWinForwardButton = scriptWinForwardButton - val image239 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image239" ~info:"GtkImage" xmldata)) - method image239 = image239 - val scriptWinBottomButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ScriptWinBottomButton" ~info:"GtkButton" xmldata)) - method scriptWinBottomButton = scriptWinBottomButton - val image238 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image238" ~info:"GtkImage" xmldata)) - method image238 = image238 - val scriptNotebook = - new GPack.notebook (GtkPack.Notebook.cast - (Glade.get_widget_msg ~name:"ScriptNotebook" ~info:"GtkNotebook" xmldata)) - method scriptNotebook = scriptNotebook - val scrolledScript = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledScript" ~info:"GtkScrolledWindow" xmldata)) - method scrolledScript = scrolledScript - val scriptTextView = - new GText.view (GtkText.View.cast - (Glade.get_widget_msg ~name:"ScriptTextView" ~info:"GtkTextView" xmldata)) - method scriptTextView = scriptTextView - val label7 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label7" ~info:"GtkLabel" xmldata)) - method label7 = label7 - val scrolledOutline = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledOutline" ~info:"GtkScrolledWindow" xmldata)) - method scrolledOutline = scrolledOutline - val outlineTreeView = - new GTree.view (GtkTree.TreeView.cast - (Glade.get_widget_msg ~name:"OutlineTreeView" ~info:"GtkTreeView" xmldata)) - method outlineTreeView = outlineTreeView - val label8 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label8" ~info:"GtkLabel" xmldata)) - method label8 = label8 - method reparent parent = - scriptWinEventBox#misc#reparent parent; - 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 = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val textDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) - method textDialog = textDialog - val vbox5 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata)) - method vbox5 = vbox5 - val hbuttonbox1 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata)) - method hbuttonbox1 = hbuttonbox1 - 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 - val scrolledwindow2 = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow2 = scrolledwindow2 - val textDialogTextView = - new GText.view (GtkText.View.cast - (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata)) - method textDialogTextView = textDialogTextView - method reparent parent = - vbox5#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"ToolBarWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val toolBarWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata)) - method toolBarWin = toolBarWin - val toolBarEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata)) - method toolBarEventBox = toolBarEventBox - val toolBarVBox = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata)) - method toolBarVBox = toolBarVBox - val toolbar2 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata)) - method toolbar2 = toolbar2 - val introsButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata)) - method introsButton = introsButton - val applyButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata)) - method applyButton = applyButton - val exactButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata)) - method exactButton = exactButton - val toolbar3 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata)) - method toolbar3 = toolbar3 - val elimButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata)) - method elimButton = elimButton - val elimTypeButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata)) - method elimTypeButton = elimTypeButton - val toolbar4 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata)) - method toolbar4 = toolbar4 - val splitButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata)) - method splitButton = splitButton - val leftButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata)) - method leftButton = leftButton - val rightButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata)) - method rightButton = rightButton - val existsButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata)) - method existsButton = existsButton - val toolbar5 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata)) - method toolbar5 = toolbar5 - val reflexivityButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata)) - method reflexivityButton = reflexivityButton - val symmetryButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata)) - method symmetryButton = symmetryButton - val transitivityButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata)) - method transitivityButton = transitivityButton - val toolbar8 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata)) - method toolbar8 = toolbar8 - val simplifyButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata)) - method simplifyButton = simplifyButton - val reduceButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata)) - method reduceButton = reduceButton - val whdButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata)) - method whdButton = whdButton - val toolbar6 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata)) - method toolbar6 = toolbar6 - val assumptionButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata)) - method assumptionButton = assumptionButton - val autoButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata)) - method autoButton = autoButton - val toolbar7 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata)) - method toolbar7 = toolbar7 - val cutButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata)) - method cutButton = cutButton - val replaceButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata)) - method replaceButton = replaceButton - method reparent parent = - toolBarEventBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val uriChoiceDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) - method uriChoiceDialog = uriChoiceDialog - val dialog_vbox3 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata)) - method dialog_vbox3 = dialog_vbox3 - val dialog_action_area3 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area3 = dialog_action_area3 - val uriChoiceAbortButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata)) - method uriChoiceAbortButton = uriChoiceAbortButton - val uriChoiceSelectedButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata)) - method uriChoiceSelectedButton = uriChoiceSelectedButton - val alignment2 = - new GBin.alignment (GtkBin.Alignment.cast - (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata)) - method alignment2 = alignment2 - val hbox3 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata)) - method hbox3 = hbox3 - val image19 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata)) - method image19 = image19 - val label3 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata)) - method label3 = label3 - val uriChoiceConstantsButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata)) - method uriChoiceConstantsButton = uriChoiceConstantsButton - val uriChoiceAutoButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata)) - method uriChoiceAutoButton = uriChoiceAutoButton - val alignment1 = - new GBin.alignment (GtkBin.Alignment.cast - (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata)) - method alignment1 = alignment1 - val hbox1 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata)) - method hbox1 = hbox1 - val image18 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata)) - method image18 = image18 - val label1 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata)) - method label1 = label1 - val vbox2 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata)) - method vbox2 = vbox2 - val uriChoiceLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata)) - method uriChoiceLabel = uriChoiceLabel - val scrolledwindow1 = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow1 = scrolledwindow1 - val uriChoiceTreeView = - new GTree.view (GtkTree.TreeView.cast - (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata)) - method uriChoiceTreeView = uriChoiceTreeView - val hbox2 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata)) - method hbox2 = hbox2 - val label2 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata)) - method label2 = label2 - val entry1 = - new GEdit.entry (GtkEdit.Entry.cast - (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata)) - method entry1 = entry1 - method reparent parent = - dialog_vbox3#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end - -let check_all ?(show=false) () = - ignore (GMain.Main.init ()); - let uriChoiceDialog = new uriChoiceDialog () in - if show then uriChoiceDialog#toplevel#show (); - uriChoiceDialog#check_widgets (); - let toolBarWin = new toolBarWin () in - if show then toolBarWin#toplevel#show (); - toolBarWin#check_widgets (); - let textDialog = new textDialog () in - if show then textDialog#toplevel#show (); - textDialog#check_widgets (); - let scriptWin = new scriptWin () in - if show then scriptWin#toplevel#show (); - scriptWin#check_widgets (); - let mainWin = new mainWin () in - if show then mainWin#toplevel#show (); - mainWin#check_widgets (); - let interpChoiceDialog = new interpChoiceDialog () in - if show then interpChoiceDialog#toplevel#show (); - interpChoiceDialog#check_widgets (); - let fileSelectionWin = new fileSelectionWin () in - if show then fileSelectionWin#toplevel#show (); - fileSelectionWin#check_widgets (); - let emptyDialog = new emptyDialog () in - if show then emptyDialog#toplevel#show (); - emptyDialog#check_widgets (); - let confirmationDialog = new confirmationDialog () in - if show then confirmationDialog#toplevel#show (); - confirmationDialog#check_widgets (); - let browserWin = new browserWin () in - if show then browserWin#toplevel#show (); - browserWin#check_widgets (); - let aboutWin = new aboutWin () in - if show then aboutWin#toplevel#show (); - aboutWin#check_widgets (); - if show then GMain.Main.main () -;; diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli deleted file mode 100644 index 33b9a87f5..000000000 --- a/helm/matita/matitaGeneratedGui.mli +++ /dev/null @@ -1,506 +0,0 @@ -class aboutWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val aboutDismissButton : GButton.button - val aboutLabel : GMisc.label - val aboutWin : GWindow.dialog_any - val dialog_action_area2 : GPack.button_box - val dialog_vbox2 : GPack.box - val toplevel : GWindow.dialog_any - val xml : Glade.glade_xml Gtk.obj - method aboutDismissButton : GButton.button - method aboutLabel : GMisc.label - method aboutWin : GWindow.dialog_any - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area2 : GPack.button_box - method dialog_vbox2 : GPack.box - method reparent : GObj.widget -> unit - method toplevel : GWindow.dialog_any - method xml : Glade.glade_xml Gtk.obj - end -class browserWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val alignment3 : GBin.alignment - val browserBackButton : GButton.button - val browserForwardButton : GButton.button - val browserHomeButton : GButton.button - val browserNewButton : GButton.button - val browserRefreshButton : GButton.button - val browserUri : GEdit.entry - val browserVBox : GPack.box - val browserWin : GWindow.window - val browserWinEventBox : GBin.event_box - val frame1 : GBin.frame - val handlebox1 : GBin.handle_box - val hbox6 : GPack.box - val hbox7 : GPack.box - val image187 : GMisc.image - val image188 : GMisc.image - val image189 : GMisc.image - val image190 : GMisc.image - val image191 : GMisc.image - val image229 : GMisc.image - val label10 : GMisc.label - val scrolledBrowser : GBin.scrolled_window - val toplevel : GWindow.window - val xml : Glade.glade_xml Gtk.obj - method alignment3 : GBin.alignment - method bind : name:string -> callback:(unit -> unit) -> unit - method browserBackButton : GButton.button - method browserForwardButton : GButton.button - method browserHomeButton : GButton.button - method browserNewButton : GButton.button - method browserRefreshButton : GButton.button - method browserUri : GEdit.entry - method browserVBox : GPack.box - method browserWin : GWindow.window - method browserWinEventBox : GBin.event_box - method check_widgets : unit -> unit - method frame1 : GBin.frame - method handlebox1 : GBin.handle_box - method hbox6 : GPack.box - method hbox7 : GPack.box - method image187 : GMisc.image - method image188 : GMisc.image - method image189 : GMisc.image - method image190 : GMisc.image - method image191 : GMisc.image - method image229 : GMisc.image - method label10 : GMisc.label - method reparent : GObj.widget -> unit - method scrolledBrowser : GBin.scrolled_window - method toplevel : GWindow.window - method xml : Glade.glade_xml Gtk.obj - end -class confirmationDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val confirmationDialog : GWindow.dialog_any - val confirmationDialogCancelButton : GButton.button - val confirmationDialogLabel : GMisc.label - val confirmationDialogOkButton : GButton.button - val dialog_action_area1 : GPack.button_box - val dialog_vbox1 : GPack.box - val toplevel : GWindow.dialog_any - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method confirmationDialog : GWindow.dialog_any - method confirmationDialogCancelButton : GButton.button - method confirmationDialogLabel : GMisc.label - method confirmationDialogOkButton : GButton.button - method dialog_action_area1 : GPack.button_box - method dialog_vbox1 : GPack.box - method reparent : GObj.widget -> unit - method toplevel : GWindow.dialog_any - method xml : Glade.glade_xml Gtk.obj - end -class emptyDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val dialog_action_area5 : GPack.button_box - val emptyDialog : GWindow.dialog_any - val emptyDialogCancelButton : GButton.button - val emptyDialogLabel : GMisc.label - val emptyDialogOkButton : GButton.button - val emptyDialogVBox : GPack.box - val toplevel : GWindow.dialog_any - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area5 : GPack.button_box - method emptyDialog : GWindow.dialog_any - method emptyDialogCancelButton : GButton.button - method emptyDialogLabel : GMisc.label - method emptyDialogOkButton : GButton.button - method emptyDialogVBox : GPack.box - method reparent : GObj.widget -> unit - method toplevel : GWindow.dialog_any - method xml : Glade.glade_xml Gtk.obj - end -class fileSelectionWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val fileSelCancelButton : GButton.button - val fileSelOkButton : GButton.button - val fileSelectionWin : GWindow.file_selection - val toplevel : GWindow.file_selection - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method fileSelCancelButton : GButton.button - method fileSelOkButton : GButton.button - method fileSelectionWin : GWindow.file_selection - method toplevel : GWindow.file_selection - method xml : Glade.glade_xml Gtk.obj - end -class interpChoiceDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val dialog_action_area4 : GPack.button_box - val dialog_vbox4 : GPack.box - val interpChoiceCancelButton : GButton.button - val interpChoiceDialog : GWindow.dialog_any - val interpChoiceDialogLabel : GMisc.label - val interpChoiceHelpButton : GButton.button - val interpChoiceOkButton : GButton.button - val interpChoiceTreeView : GTree.view - val scrolledwindow4 : GBin.scrolled_window - val toplevel : GWindow.dialog_any - val vbox3 : GPack.box - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area4 : GPack.button_box - method dialog_vbox4 : GPack.box - method interpChoiceCancelButton : GButton.button - method interpChoiceDialog : GWindow.dialog_any - method interpChoiceDialogLabel : GMisc.label - method interpChoiceHelpButton : GButton.button - method interpChoiceOkButton : GButton.button - method interpChoiceTreeView : GTree.view - method reparent : GObj.widget -> unit - method scrolledwindow4 : GBin.scrolled_window - method toplevel : GWindow.dialog_any - method vbox3 : GPack.box - method xml : Glade.glade_xml Gtk.obj - end -class mainWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val aboutMenuItem : GMenu.menu_item - val consoleEventBox : GBin.event_box - val consoleHBox : GPack.box - val debugMenu : 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 hideConsoleButton : GButton.button - val image169 : GMisc.image - val image224 : GMisc.image - val image225 : GMisc.image - val image226 : GMisc.image - val image227 : GMisc.image - val image228 : GMisc.image - val mainMenuBar : GMenu.menu_shell - val mainStatusBar : GMisc.statusbar - val mainVPanes : GPack.paned - val mainWin : GWindow.window - val mainWinEventBox : GBin.event_box - val mainWinShape : GPack.box - val newCicBrowserMenuItem : GMenu.menu_item - val newDefsMenuItem : GMenu.menu_item - val newMenu : GMenu.image_menu_item - val newMenu_menu : GMenu.menu - val newProofMenuItem : GMenu.menu_item - val openMenuItem : GMenu.image_menu_item - val quitMenuItem : GMenu.image_menu_item - val saveAsMenuItem : GMenu.image_menu_item - val saveMenuItem : GMenu.image_menu_item - val scrolledConsole : GBin.scrolled_window - val separator1 : GMenu.menu_item - val separator2 : GMenu.menu_item - val separator3 : GMenu.menu_item - val sequentsNotebook : GPack.notebook - val showConsoleMenuItem : GMenu.menu_item - val showScriptMenuItem : GMenu.check_menu_item - val showToolBarMenuItem : GMenu.check_menu_item - val toplevel : GWindow.window - val vbox6 : GPack.box - val viewMenu : GMenu.menu_item - val viewMenu_menu : GMenu.menu - val xml : Glade.glade_xml Gtk.obj - method aboutMenuItem : GMenu.menu_item - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method consoleEventBox : GBin.event_box - method consoleHBox : GPack.box - method debugMenu : 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 hideConsoleButton : GButton.button - method image169 : GMisc.image - method image224 : GMisc.image - method image225 : GMisc.image - method image226 : GMisc.image - method image227 : GMisc.image - method image228 : GMisc.image - method mainMenuBar : GMenu.menu_shell - method mainStatusBar : GMisc.statusbar - method mainVPanes : GPack.paned - method mainWin : GWindow.window - method mainWinEventBox : GBin.event_box - method mainWinShape : GPack.box - method newCicBrowserMenuItem : GMenu.menu_item - method newDefsMenuItem : GMenu.menu_item - method newMenu : GMenu.image_menu_item - method newMenu_menu : GMenu.menu - method newProofMenuItem : GMenu.menu_item - method openMenuItem : GMenu.image_menu_item - method quitMenuItem : GMenu.image_menu_item - method reparent : GObj.widget -> unit - method saveAsMenuItem : GMenu.image_menu_item - method saveMenuItem : GMenu.image_menu_item - method scrolledConsole : GBin.scrolled_window - method separator1 : GMenu.menu_item - method separator2 : GMenu.menu_item - method separator3 : GMenu.menu_item - method sequentsNotebook : GPack.notebook - method showConsoleMenuItem : GMenu.menu_item - method showScriptMenuItem : GMenu.check_menu_item - method showToolBarMenuItem : GMenu.check_menu_item - method toplevel : GWindow.window - method vbox6 : GPack.box - method viewMenu : GMenu.menu_item - method viewMenu_menu : GMenu.menu - method xml : Glade.glade_xml Gtk.obj - end -class scriptWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val handlebox2 : GBin.handle_box - val hbox8 : GPack.box - val image134 : GMisc.image - val image235 : GMisc.image - val image237 : GMisc.image - val image238 : GMisc.image - val image239 : GMisc.image - val label7 : GMisc.label - val label8 : GMisc.label - val outlineTreeView : GTree.view - val scriptNotebook : GPack.notebook - val scriptTextView : GText.view - val scriptWin : GWindow.window - val scriptWinBackButton : GButton.button - val scriptWinBottomButton : GButton.button - val scriptWinEventBox : GBin.event_box - val scriptWinForwardButton : GButton.button - val scriptWinJumpButton : GButton.button - val scriptWinTopButton : GButton.button - val scrolledOutline : GBin.scrolled_window - val scrolledScript : GBin.scrolled_window - val toplevel : GWindow.window - val vbox7 : GPack.box - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method handlebox2 : GBin.handle_box - method hbox8 : GPack.box - method image134 : GMisc.image - method image235 : GMisc.image - method image237 : GMisc.image - method image238 : GMisc.image - method image239 : GMisc.image - method label7 : GMisc.label - method label8 : GMisc.label - method outlineTreeView : GTree.view - method reparent : GObj.widget -> unit - method scriptNotebook : GPack.notebook - method scriptTextView : GText.view - method scriptWin : GWindow.window - method scriptWinBackButton : GButton.button - method scriptWinBottomButton : GButton.button - method scriptWinEventBox : GBin.event_box - method scriptWinForwardButton : GButton.button - method scriptWinJumpButton : GButton.button - method scriptWinTopButton : GButton.button - method scrolledOutline : GBin.scrolled_window - method scrolledScript : GBin.scrolled_window - method toplevel : GWindow.window - method vbox7 : GPack.box - method xml : Glade.glade_xml Gtk.obj - end -class textDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val hbuttonbox1 : GPack.button_box - val scrolledwindow2 : GBin.scrolled_window - val textDialog : GWindow.dialog_any - val textDialogCancelButton : GButton.button - val textDialogLabel : GMisc.label - val textDialogOkButton : GButton.button - val textDialogTextView : GText.view - val toplevel : GWindow.dialog_any - val vbox5 : GPack.box - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method hbuttonbox1 : GPack.button_box - method reparent : GObj.widget -> unit - method scrolledwindow2 : GBin.scrolled_window - method textDialog : GWindow.dialog_any - method textDialogCancelButton : GButton.button - method textDialogLabel : GMisc.label - method textDialogOkButton : GButton.button - method textDialogTextView : GText.view - method toplevel : GWindow.dialog_any - method vbox5 : GPack.box - method xml : Glade.glade_xml Gtk.obj - end -class toolBarWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val applyButton : GButton.button - val assumptionButton : GButton.button - val autoButton : GButton.button - val cutButton : GButton.button - val elimButton : GButton.button - val elimTypeButton : GButton.button - val exactButton : GButton.button - val existsButton : GButton.button - val introsButton : GButton.button - val leftButton : GButton.button - val reduceButton : GButton.button - val reflexivityButton : GButton.button - val replaceButton : GButton.button - val rightButton : GButton.button - val simplifyButton : GButton.button - val splitButton : GButton.button - val symmetryButton : GButton.button - val toolBarEventBox : GBin.event_box - val toolBarVBox : GPack.box - val toolBarWin : GWindow.window - val toolbar2 : GButton.toolbar - val toolbar3 : GButton.toolbar - val toolbar4 : GButton.toolbar - val toolbar5 : GButton.toolbar - val toolbar6 : GButton.toolbar - val toolbar7 : GButton.toolbar - val toolbar8 : GButton.toolbar - val toplevel : GWindow.window - val transitivityButton : GButton.button - val whdButton : GButton.button - val xml : Glade.glade_xml Gtk.obj - method applyButton : GButton.button - method assumptionButton : GButton.button - method autoButton : GButton.button - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method cutButton : GButton.button - method elimButton : GButton.button - method elimTypeButton : GButton.button - method exactButton : GButton.button - method existsButton : GButton.button - method introsButton : GButton.button - method leftButton : GButton.button - method reduceButton : GButton.button - method reflexivityButton : GButton.button - method reparent : GObj.widget -> unit - method replaceButton : GButton.button - method rightButton : GButton.button - method simplifyButton : GButton.button - method splitButton : GButton.button - method symmetryButton : GButton.button - method toolBarEventBox : GBin.event_box - method toolBarVBox : GPack.box - method toolBarWin : GWindow.window - method toolbar2 : GButton.toolbar - method toolbar3 : GButton.toolbar - method toolbar4 : GButton.toolbar - method toolbar5 : GButton.toolbar - method toolbar6 : GButton.toolbar - method toolbar7 : GButton.toolbar - method toolbar8 : GButton.toolbar - method toplevel : GWindow.window - method transitivityButton : GButton.button - method whdButton : GButton.button - method xml : Glade.glade_xml Gtk.obj - end -class uriChoiceDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val alignment1 : GBin.alignment - val alignment2 : GBin.alignment - val dialog_action_area3 : GPack.button_box - val dialog_vbox3 : GPack.box - val entry1 : GEdit.entry - val hbox1 : GPack.box - val hbox2 : GPack.box - val hbox3 : GPack.box - val image18 : GMisc.image - val image19 : GMisc.image - val label1 : GMisc.label - val label2 : GMisc.label - val label3 : GMisc.label - val scrolledwindow1 : GBin.scrolled_window - val toplevel : GWindow.dialog_any - val uriChoiceAbortButton : GButton.button - val uriChoiceAutoButton : GButton.button - val uriChoiceConstantsButton : GButton.button - val uriChoiceDialog : GWindow.dialog_any - val uriChoiceLabel : GMisc.label - val uriChoiceSelectedButton : GButton.button - val uriChoiceTreeView : GTree.view - val vbox2 : GPack.box - val xml : Glade.glade_xml Gtk.obj - method alignment1 : GBin.alignment - method alignment2 : GBin.alignment - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area3 : GPack.button_box - method dialog_vbox3 : GPack.box - method entry1 : GEdit.entry - method hbox1 : GPack.box - method hbox2 : GPack.box - method hbox3 : GPack.box - method image18 : GMisc.image - method image19 : GMisc.image - method label1 : GMisc.label - method label2 : GMisc.label - method label3 : GMisc.label - method reparent : GObj.widget -> unit - method scrolledwindow1 : GBin.scrolled_window - method toplevel : GWindow.dialog_any - method uriChoiceAbortButton : GButton.button - method uriChoiceAutoButton : GButton.button - method uriChoiceConstantsButton : GButton.button - method uriChoiceDialog : GWindow.dialog_any - method uriChoiceLabel : GMisc.label - method uriChoiceSelectedButton : GButton.button - method uriChoiceTreeView : GTree.view - method vbox2 : GPack.box - 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 deleted file mode 100644 index a0755371b..000000000 --- a/helm/matita/matitaGtkMisc.ml +++ /dev/null @@ -1,282 +0,0 @@ -(* 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/ - *) - -open Printf - -open MatitaTypes - -let connect_button (button: GButton.button) callback = - ignore (button#connect#clicked callback) - -let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key - callback -= - ignore (ev#connect#key_press (fun key' -> - let modifiers' = GdkEvent.Key.state key' in - (match key' with - | key' when GdkEvent.Key.keyval key' = key - && List.for_all (fun m -> List.mem m modifiers') modifiers -> - callback (); - stop - | _ -> false))) - -let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) = - ignore (check#connect#toggled (fun _ -> - if check#active then win#show () else win#misc#hide ())); - ignore (win#event#connect#delete (fun _ -> - win#misc#hide (); - check#set_active false; - true)) - -let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () = - if win#is_active then win#misc#hide () else win#show (); - match check with - | None -> () - | Some check -> check#set_active (not check#active) - -let add_key_binding key callback (evbox: GBin.event_box) = - ignore (evbox#event#connect#key_press (function - | key' when GdkEvent.Key.keyval key' = key -> - callback (); - false - | _ -> false)) - -class stringListModel (tree_view: GTree.view) = - let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in - let list_store = GTree.list_store column_list in - object (self) - - initializer - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in - tree_view#set_model (Some (list_store :> GTree.model)); - ignore (tree_view#append_column view_column) - - method list_store = list_store - - method easy_append s = - let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s - - method easy_insert pos s = - let tree_iter = list_store#insert pos in - list_store#set ~row:tree_iter ~column:text_column s - - method easy_selection () = - List.map - (fun tree_path -> - let iter = list_store#get_iter tree_path in - list_store#get ~row:iter ~column:text_column) - tree_view#selection#get_selected_rows - - end - -class interpModel = - let cols = new GTree.column_list in - let id_col = cols#add Gobject.Data.string in - let dsc_col = cols#add Gobject.Data.string in - let interp_no_col = cols#add Gobject.Data.int in - let tree_store = GTree.tree_store cols in - let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in - let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in - let id_view_col = GTree.view_column ~renderer:id_renderer () in - let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in - fun tree_view choices -> - object - initializer - tree_view#set_model (Some (tree_store :> GTree.model)); - ignore (tree_view#append_column id_view_col); - ignore (tree_view#append_column dsc_view_col); - let name_of_interp = - (* try to find a reasonable name for an interpretation *) - let idx = ref 0 in - fun interp -> - try - List.assoc "0" interp - with Not_found -> - incr idx; string_of_int !idx - in - tree_store#clear (); - let idx = ref ~-1 in - List.iter - (fun interp -> - incr idx; - let interp_row = tree_store#append () in - tree_store#set ~row:interp_row ~column:id_col - (name_of_interp interp); - tree_store#set ~row:interp_row ~column:interp_no_col !idx; - List.iter - (fun (id, dsc) -> - let row = tree_store#append ~parent:interp_row () in - tree_store#set ~row ~column:id_col id; - tree_store#set ~row ~column:dsc_col dsc; - tree_store#set ~row ~column:interp_no_col !idx) - interp) - choices - - method get_interp_no tree_path = - let iter = tree_store#get_iter tree_path in - tree_store#get ~row:iter ~column:interp_no_col - 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) - -class type gui = - object - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog - method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog - end - -let interactive_user_uri_choice - ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(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 dialog = gui#newUriDialog () in - dialog#uriChoiceTreeView#selection#set_mode - (selection_mode :> Gtk.Tags.selection_mode); - let model = new stringListModel dialog#uriChoiceTreeView in - let choices = ref None in - let nonvars = ref false in - dialog#uriChoiceDialog#set_title title; - dialog#uriChoiceLabel#set_text msg; - List.iter model#easy_append uris; - dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; - let return v = - choices := v; - dialog#uriChoiceDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#uriChoiceConstantsButton (fun _ -> - return (Some (Lazy.force nonvars_uris))); - connect_button dialog#uriChoiceAutoButton (fun _ -> - Helm_registry.set_bool "matita.auto_disambiguation" true; - return (Some (Lazy.force nonvars_uris))); - connect_button dialog#uriChoiceSelectedButton (fun _ -> - match model#easy_selection () with - | [] -> () - | uris -> return (Some uris)); - connect_button dialog#uriChoiceAbortButton (fun _ -> return None); - dialog#uriChoiceDialog#show (); - GtkThread.main (); - (match !choices with - | None -> raise Cancel - | Some uris -> uris) - end - -let interactive_interp_choice ~(gui:#gui) choices = - assert (choices <> []); - let dialog = gui#newInterpDialog () in - let model = new interpModel dialog#interpChoiceTreeView choices in - let interp_len = List.length (List.hd choices) in - dialog#interpChoiceDialog#set_title "Interpretation choice"; - dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:"; - let interp_no = ref None in - let return _ = - dialog#interpChoiceDialog#destroy (); - GMain.Main.quit () - in - let fail _ = interp_no := None; return () in - ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#interpChoiceOkButton (fun _ -> - match !interp_no with None -> () | Some _ -> return ()); - connect_button dialog#interpChoiceCancelButton fail; - ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ -> - interp_no := Some (model#get_interp_no path); - return ())); - let selection = dialog#interpChoiceTreeView#selection in - ignore (selection#connect#changed (fun _ -> - match selection#get_selected_rows with - | [path] -> - debug_print (sprintf "selection: %d" (model#get_interp_no path)); - interp_no := Some (model#get_interp_no path) - | _ -> assert false)); - dialog#interpChoiceDialog#show (); - GtkThread.main (); - (match !interp_no with Some row -> [row] | _ -> raise Cancel) - -let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () = - 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)); - connect_button dialog#confirmationDialogOkButton (return true); - connect_button dialog#confirmationDialogCancelButton (return false); - if not cancel then dialog#confirmationDialogCancelButton#misc#hide (); - 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#newEmptyDialog () in - dialog#emptyDialog#set_title title; - dialog#emptyDialogLabel#set_label msg; - let result = ref None in - let return r = - result := r; - dialog#emptyDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#emptyDialog#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#emptyDialogVBox#add () - in - let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in - view#misc#grab_focus (); - connect_button dialog#emptyDialogOkButton (fun _ -> - return (Some (view#buffer#get_text ()))) - end else begin (* monoline input required: use a TextEntry widget *) - let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in - entry#misc#grab_focus (); - connect_button dialog#emptyDialogOkButton (fun _ -> - return (Some entry#text)) - end; - connect_button dialog#emptyDialogCancelButton (fun _ ->return None); - dialog#emptyDialog#show (); - GtkThread.main (); - (match !result with None -> raise Cancel | Some r -> r) - diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli deleted file mode 100644 index 46e584596..000000000 --- a/helm/matita/matitaGtkMisc.mli +++ /dev/null @@ -1,96 +0,0 @@ -(* 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/ - *) - -(** {2 Gtk helpers} *) - - (** given a window and a check menu item it links the two so that the former - * is only hidden on delete and the latter toggle show/hide of the former *) -val toggle_visibility: - win:GWindow.window -> check:GMenu.check_menu_item -> unit - -val toggle_win: - ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit - -val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit - -val connect_button: GButton.button -> (unit -> unit) -> unit - - (** connect a unit -> unit callback to a particular key press event. Event can - * be specified using its keysym and a list of modifiers which must be in - * effect for the callback to be executed. Further signal processing of other - * key press events remains unchanged; further signal processing of the - * specified key press depends on the stop parameter *) -val connect_key: - GObj.event_ops -> - ?modifiers:Gdk.Tags.modifier list -> - ?stop:bool -> (* stop signal handling when the given key has been pressed? - * Defaults to false *) - Gdk.keysym -> (* (= int) the key, see GdkKeysyms.ml *) - (unit -> unit) -> (* callback *) - unit - - (** single string column list *) -class stringListModel: - GTree.view -> - object - method list_store: GTree.list_store (** list_store forwarding *) - - method easy_append: string -> unit (** append + set *) - method easy_insert: int -> string -> unit (** insert + set *) - method easy_selection: unit -> string list - end - -(** {2 Matita GUI components} *) - -class type gui = - object (* minimal gui object requirements *) - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog - method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog - end - - (** {3 Dialogs} *) - - (** @raise MatitaTypes.Cancel *) -val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback - - (** @raise MatitaTypes.Cancel *) -val interactive_interp_choice: gui:#gui -> MatitaTypes.choose_interp_callback - - (** @return true if user hit "ok" button, false if user hit "cancel" button - * @param cancel if set to true a cancel button is shown to the user, otherwise - * it is not (and indeed the function will return true). Defaults to true *) -val ask_confirmation: - gui:#gui -> - ?cancel:bool -> ?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 deleted file mode 100644 index 7ac22dc8d..000000000 --- a/helm/matita/matitaGui.ml +++ /dev/null @@ -1,235 +0,0 @@ -(* 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/ - *) - -open Printf - -open MatitaGeneratedGui -open MatitaGtkMisc -open MatitaMisc - -let gui_instance = ref None ;; - -class console ~evbox ~phrase_sep ~packing ~paned () = - let console = MatitaConsole.console ~evbox ~phrase_sep ~packing ~paned () in - object - method clear = console#clear - method echo_error = console#echo_error - method echo_message = console#echo_message - method wrap_exn: 'a. (unit -> 'a) -> 'a option = console#wrap_exn - method choose_uri uris = - let g = match !gui_instance with None -> assert false | Some g -> g in - let ul = g#newUriDialog () in - ul#toplevel#show (); - let model = new stringListModel ul#uriChoiceTreeView in - List.iter model#easy_append uris; - ul#uriChoiceDialog#set_title "Hints"; - ul#uriChoiceLabel#set_text "Suggested uris"; - ul#uriChoiceAbortButton#misc#hide (); - ul#uriChoiceAutoButton#misc#hide (); - ul#uriChoiceConstantsButton#misc#hide (); - ul#hbox2#misc#hide (); - ul#uriChoiceTreeView#selection#set_mode - (`SINGLE :> Gtk.Tags.selection_mode); - let _ = ul#uriChoiceTreeView#selection#connect#changed - ~callback:(fun () -> ()) in - let _ = ul#toplevel#connect#destroy - ~callback:(fun () -> GMain.Main.quit ()) in - let choices = ref None in - let _ = ul#uriChoiceSelectedButton#connect#clicked - ~callback:(fun () -> - (match model#easy_selection () with - | [] -> () - | [uri] -> choices := (Some uri) - | _ -> assert false); - ul#uriChoiceDialog#destroy (); - GMain.Main.quit ()) in - GMain.main (); - match !choices with - | Some u -> u - | None -> raise MatitaTypes.Cancel - - method show = console#show - - method console = console - end - -class gui file = - (* creation order _is_ relevant for windows placement *) - let toolbar = new toolBarWin ~file () in - let main = new mainWin ~file () in - let about = new aboutWin ~file () in - let fileSel = new fileSelectionWin ~file () in - let script = new scriptWin ~file () in - let keyBindingBoxes = (* event boxes which should receive global key events *) - [ toolbar#toolBarEventBox; main#mainWinEventBox; - script#scriptWinEventBox; main#consoleEventBox ] - in - let console = - new console ~evbox:main#consoleEventBox - ~phrase_sep:BuildTimeConf.phrase_sep - ~packing:main#scrolledConsole#add ~paned:main#mainVPanes () - in - object (self) - val mutable chosen_file = None - - initializer - (* glade's check widgets *) - List.iter (fun w -> w#check_widgets ()) - (let c w = (w :> unit>) in - [ c about; c fileSel; c main; c toolbar; c script ]); - (* key bindings *) - List.iter (* global key bindings *) - (fun (key, callback) -> self#addKeyBinding key callback) -(* - [ GdkKeysyms._F3, - toggle_win ~check:main#showProofMenuItem proof#proofWin; - GdkKeysyms._F4, - toggle_win ~check:main#showCheckMenuItem check#checkWin; -*) - [ GdkKeysyms._F5, - toggle_win ~check:main#showScriptMenuItem script#scriptWin; - GdkKeysyms._x, (fun () -> console#console#toggle ()); - ]; - add_key_binding GdkKeysyms._Escape console#console#hide - main#consoleEventBox; - (* about win *) - ignore (about#aboutWin#event#connect#delete (fun _ -> true)); - ignore (main#aboutMenuItem#connect#activate (fun _ -> - about#aboutWin#show ())); - connect_button about#aboutDismissButton (fun _ -> - about#aboutWin#misc#hide ()); - about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@" - ~templ:BuildTimeConf.version about#aboutLabel#label); - (* file selection win *) - ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); - ignore (fileSel#fileSelectionWin#connect#response (fun event -> - let return r = - chosen_file <- r; - fileSel#fileSelectionWin#misc#hide (); - GMain.Main.quit () - in - match event with - | `OK -> - let fname = fileSel#fileSelectionWin#filename in - if is_regular fname then return (Some fname) - | `CANCEL -> return None - | `HELP -> () - | `DELETE_EVENT -> return None)); - (* script *) - (* menus *) - toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; -(* - toggle_visibility proof#proofWin main#showProofMenuItem; - toggle_visibility check#checkWin main#showCheckMenuItem; -*) - toggle_visibility script#scriptWin main#showScriptMenuItem; - List.iter (fun w -> w#misc#set_sensitive false) - [ main#saveMenuItem; main#saveAsMenuItem ]; - main#helpMenu#set_right_justified true; - ignore (main#showConsoleMenuItem#connect#activate console#console#toggle); - (* main *) - connect_button main#hideConsoleButton console#console#hide; - (* console *) - console#echo_message (sprintf "\tMatita version %s\n" - BuildTimeConf.version); - console#console#echo_prompt (); - console#console#misc#grab_focus (); - - method about = about - method console = (console :> MatitaTypes.console) - method fileSel = fileSel - method main = main - method script = script - method toolbar = toolbar - - method newBrowserWin () = - let win = new browserWin ~file () in - win#check_widgets (); - win - - 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 newConfirmationDialog () = - let dialog = new confirmationDialog ~file () in - dialog#check_widgets (); - dialog - - method newEmptyDialog () = - let dialog = new emptyDialog ~file () in - dialog#check_widgets (); - dialog - - method private addKeyBinding key callback = - List.iter (fun evbox -> add_key_binding key callback evbox) - keyBindingBoxes - - method setQuitCallback callback = - ignore (main#toplevel#connect#destroy callback); - ignore (main#quitMenuItem#connect#activate callback); - self#addKeyBinding GdkKeysyms._q callback - - method setPhraseCallback = console#console#set_callback - - method chooseFile () = - fileSel#fileSelectionWin#show (); - GtkThread.main (); - chosen_file - - method askText ?(title = "") ?(msg = "") () = - let dialog = new textDialog () in - dialog#textDialog#set_title title; - dialog#textDialogLabel#set_label msg; - let text = ref None in - let return v = - text := v; - dialog#textDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#textDialogCancelButton (fun _ -> return None); - connect_button dialog#textDialogOkButton (fun _ -> - let text = dialog#textDialogTextView#buffer#get_text () in - return (Some text)); - dialog#textDialog#show (); - GtkThread.main (); - !text - - end - -let gui () = - let g = new gui (Helm_registry.get "matita.glade_file") in - gui_instance := Some g; - g - -let instance = singleton gui - diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli deleted file mode 100644 index 90cb814a1..000000000 --- a/helm/matita/matitaGui.mli +++ /dev/null @@ -1,68 +0,0 @@ -(* 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/ - *) - - (** @param fname name of the Glade file describing the GUI *) -class gui : - string -> - object - - method setQuitCallback : (unit -> unit) -> unit - method setPhraseCallback : (string -> MatitaTypes.command_outcome) -> unit - - (** {2 Access to singleton instances of lower-level GTK widgets} *) - - method about : MatitaGeneratedGui.aboutWin - method fileSel : MatitaGeneratedGui.fileSelectionWin - method main : MatitaGeneratedGui.mainWin - method script: MatitaGeneratedGui.scriptWin - method toolbar : MatitaGeneratedGui.toolBarWin - - (** {2 Access to GUI useful components} *) - - method console: MatitaTypes.console - - (** {2 Dialogs instantiation} - * methods below create a new window on each invocation. You should - * remember to destroy windows after use *) - - method newBrowserWin: unit -> MatitaGeneratedGui.browserWin - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog - method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog - - (** {2 Utility methods} *) - - (** ask the used to choose a file with the file chooser *) - method chooseFile: unit -> string option - - (** prompt the user for a (multiline) text entry *) - method askText: ?title:string -> ?msg:string -> unit -> string option - - end - - (** singleton instance of the gui *) -val instance: unit -> gui - diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml deleted file mode 100644 index e578a3eb0..000000000 --- a/helm/matita/matitaInterpreter.ml +++ /dev/null @@ -1,678 +0,0 @@ -(* 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/ - *) - -(** Interpreter for textual phrases coming from matita's console (textual entry -* window at the bottom of the main window). -* -* Interpreter is either in Command state or in Proof state (see state type -* below). In Command state commands for starting proofs are accepted, but -* tactic and tactical applications are not. In Proof state both -* tactic/tacticals and commands are accepted. -*) - -open Printf - -open MatitaTypes - -type state = Command | Proof -type outcome = New_state of state | Quiet | Echo of string - -exception Command_error of string - -(* -let uri name = - UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name) -*) - -let baseuri = lazy (ref ("cic:/matita/" ^ Helm_registry.get "matita.owner")) -let basedir = lazy (ref (Helm_registry.get "matita.basedir")) - -let qualify name = - let baseuri = !(Lazy.force baseuri) in - if baseuri.[String.length baseuri - 1] = '/' then - baseuri ^ name - else - String.concat "/" [baseuri; name] -let split_obj = function - | Cic.Constant (name, body, ty, _, attrs) - | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) - | _ -> assert false - -class virtual interpreterState = - (* static values, shared by all states inheriting this class *) - let loc = ref None in - let last_item = ref None in - let evalAstCallback = ref None in - fun ~(console: #MatitaTypes.console) -> - object (self) - - val dbd = MatitaMisc.dbd_instance () - val currentProof = MatitaProof.instance () - val disambiguator = MatitaDisambiguator.instance () - - (** eval a toplevel phrase in the current state and return the new state - *) - method parsePhrase s = - match disambiguator#parserr#parseTactical s with - | (TacticAst.LocatedTactical (loc', tac)) as tactical -> - loc := Some loc'; - tactical - | _ -> assert false - - method virtual evalTactical: - (CicAst.term, string) TacticAst.tactical -> outcome - - method private _evalTactical ast = - self#setLastItem None; - let res = self#evalTactical ast in - (match !evalAstCallback with Some f -> f ast | None -> ()); - res - - method evalPhrase s = - self#_evalTactical (self#parsePhrase (Stream.of_string s)) - - method evalAst ast = self#_evalTactical ast - - method endOffset = - match !loc with - | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum - | None -> failwith "MatitaInterpreter: no offset recorded" - - method lastItem: script_item option = !last_item - method private setLastItem item = last_item := item - - method setEvalAstCallback f = evalAstCallback := Some f - - end - - (** Implements phrases that should be accepted in all states *) -class sharedState - ~(console: #MatitaTypes.console) - ?(mathViewer: MatitaTypes.mathViewer option) - () -= - object (self) - inherit interpreterState ~console - method evalTactical = function - | TacticAst.Command TacticAst.Quit -> - currentProof#quit (); - assert false (* dummy answer, useless *) - | TacticAst.Command TacticAst.Proof -> - (* do nothing, just for compatibility with coq syntax *) - New_state Command - | TacticAst.Command (TacticAst.Baseuri (Some uri)) -> - Lazy.force baseuri := uri; - console#echo_message (sprintf "base uri set to \"%s\"" uri); - Quiet - | TacticAst.Command (TacticAst.Baseuri None) -> - console#echo_message (sprintf "base uri is \"%s\"" - !(Lazy.force baseuri)); - Quiet - | TacticAst.Command (TacticAst.Basedir (Some path)) -> - Lazy.force basedir := path; - console#echo_message (sprintf "base dir set to \"%s\"" path); - Quiet - | TacticAst.Command (TacticAst.Basedir None) -> - console#echo_message (sprintf "base dir is \"%s\"" - !(Lazy.force basedir)); - Quiet - | TacticAst.Command (TacticAst.Check term) -> - let (_, metasenv, term,ugraph) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof term - in - let (context, _) = - MatitaCicMisc.get_context_and_metasenv currentProof - in -(* this is the Eval Compute - let term = CicReduction.whd context term in -*) - let dummyno = CicMkImplicit.new_meta metasenv [] in - let ty,ugraph1 = - CicTypeChecker.type_of_aux' metasenv context term ugraph - in - (* TASSI: here ugraph1 is unused.... FIXME *) - let expr = Cic.Cast (term, ty) in - (match mathViewer with - | Some v -> v#checkTerm (`Cic (expr, metasenv)) - | _ -> ()); - Quiet - | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) -> - let uris = - match search_kind with - | `Locate -> MetadataQuery.locate ~dbd pat - | `Elim -> MetadataQuery.elim ~dbd pat - | _ -> assert false - in - (* TODO ZACK: show URIs to the user *) - Quiet - | TacticAst.Command (TacticAst.Print `Env) -> - let uris = CicEnvironment.list_uri () in - console#echo_message "Environment:"; - List.iter (fun u -> - console#echo_message (" " ^ (UriManager.string_of_uri u)) - ) uris; - Quiet - | TacticAst.Command (TacticAst.Print `Coer) -> - let uris = CoercGraph.get_coercions_list () in - console#echo_message "Coercions:"; - List.iter (fun (s,t,u) -> - console#echo_message (" " ^ (UriManager.string_of_uri u)) - ) uris; - Quiet - | tactical -> - raise (Command_error (TacticAstPp.pp_tactical tactical)) - end - -open Printf - -let pp_indtypes indTypes = - List.iter - (fun (name, _, typ, constructors) -> - printf "%s: %s\n" name (CicPp.ppterm typ); - List.iter - (fun (name, term) -> printf "\t%s: %s\n" name (CicPp.ppterm term)) - constructors) - indTypes; - flush stdout - -let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = - let add_pi binders t = - List.fold_right - (fun (name, ast) acc -> - CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) - binders t - in - let ind_binders = - List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes - in - let binders = ind_binders @ params in - let asts = ref [] in - let add_ast ast = asts := ast :: !asts in - let paramsno = List.length params in - let indbindersno = List.length ind_binders in - List.iter - (fun (name, _, typ, constructors) -> - add_ast (add_pi params typ); - List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors) - indTypes; - let (_, metasenv, terms, ugraph) = - disambiguator#disambiguateTermAsts ~metasenv:[] !asts - in - let terms = ref (List.rev terms) in - let get_term () = - match !terms with [] -> assert false | hd :: tl -> terms := tl; hd - in - let uri = - match indTypes with - | (name, _, _, _) :: _ -> qualify name ^ ".ind" - | _ -> assert false - in - let mutinds = - let counter = ref 0 in - List.map - (fun _ -> - incr counter; - CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter)) - indTypes - in - let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in - let cicIndTypes = - List.fold_left - (fun acc (name, inductive, typ, constructors) -> - let cicTyp = get_term () in - let cicConstructors = - List.fold_left - (fun acc (name, _) -> - let typ = - subst_mutinds (CicUtil.strip_prods indbindersno (get_term ())) - in - (name, typ) :: acc) - [] constructors - in - (name, inductive, cicTyp, List.rev cicConstructors) :: acc) - [] indTypes - in - let cicIndTypes = List.rev cicIndTypes in - (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) - -let save_object_to_disk uri obj = - let ensure_path_exists path = - let dir = Filename.dirname path in - try - let stats = Unix.stat dir in - if stats.Unix.st_kind <> Unix.S_DIR then - raise (Failure (dir ^ " already exists and is not a directory")) - else - () - with - Unix.Unix_error (_,_,_) -> - let pstatus = Unix.system ("mkdir -p " ^ dir) in - match pstatus with - | Unix.WEXITED n when n = 0 -> () - | _ -> raise (Failure ("Unable to create " ^ dir)) - in - (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) - let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = - Cic2acic.acic_object_of_cic_object ~eta_fix:false obj - in - (* prepare XML *) - let xml, bodyxml = - Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false - annobj - in - let xmlinnertypes = - Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types - ~ask_dtd_to_the_getter:false - in - (* prepare URIs and paths *) - let innertypesuri = UriManager.innertypesuri_of_uri uri in - let bodyuri = UriManager.bodyuri_of_uri uri in - let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in - let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in - let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".xml.gz" in - let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in - let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".body.xml.gz" in - let xmlbodypath = !(Lazy.force basedir) ^ "/" ^ xmlbodyfilename in - let path_scheme_of path = "file://" ^ path in - MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]); - (* now write to disk *) - ensure_path_exists innertypespath; - Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ; - ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath) ; - - (* now register to the getter *) - Http_getter.register' innertypesuri (path_scheme_of innertypespath); - Http_getter.register' uri (path_scheme_of xmlpath); - (* now the optional body, both write and register *) - (match bodyxml,bodyuri with - None,None -> () - | Some bodyxml,Some bodyuri-> - ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ; - Http_getter.register' bodyuri (path_scheme_of xmlbodypath) - | _-> assert false) - - (* TODO ZACK a lot more to be done here: - * - save universe file *) -let add_constant_to_world ~(console: #MatitaTypes.console) - ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph () -= - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - error (sprintf "%s constant already defined" suri) - else begin - let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name, body, ty, params, attrs) in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd ~uri ~body ~ty; - save_object_to_disk uri obj; - console#echo_message (sprintf "%s constant defined" suri) - end - -let add_inductive_def_to_world ~(console: #MatitaTypes.console) - ~dbd ~uri ~indTypes ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph () -= - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - error (sprintf "%s inductive type already defined" suri) - else begin - let name = UriManager.name_of_uri uri in - let obj = Cic.InductiveDefinition (indTypes, params, leftno, attrs) in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.put_inductive_definition uri (obj, ugraph); - MetadataDb.index_inductive_def ~dbd ~uri ~types:indTypes; - save_object_to_disk uri obj; - console#echo_message (sprintf "%s inductive type defined" suri); - let elim sort = - try - let obj = CicElim.elim_of ~sort uri 0 in - let (name, body, ty, attrs) = split_obj obj in - let suri = qualify name ^ ".con" in - let uri = UriManager.uri_of_string suri in - (* TODO Zack: make CicElim returns a universe *) - let ugraph = CicUniv.empty_ugraph in - add_constant_to_world ~console ~dbd ~uri ?body ~ty ~attrs ~ugraph (); -(* - console#echo_message - (sprintf "%s eliminator (automatically) defined" suri) -*) - with CicElim.Can_t_eliminate -> () - in - List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - end - - (** Implements phrases that should be accepted only in Command state *) -class commandState ~(console: #MatitaTypes.console) ?mathViewer () = - let shared = new sharedState ~console ?mathViewer () in - object (self) - inherit interpreterState ~console - - method evalTactical = function - | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical - | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) -> - let (_, metasenv, expr,ugraph) = - disambiguator#disambiguateTermAst ast - in - let uri = UriManager.uri_of_string (qualify name ^ ".con") in - let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in - currentProof#start proof; - self#setLastItem (Some `Theorem); - New_state Proof - | TacticAst.Command - (TacticAst.Theorem (_, Some name, type_ast, Some body_ast)) -> - let (_, metasenv, type_cic, ugraph) = - disambiguator#disambiguateTermAst type_ast - in - let (_, metasenv, body_cic, ugraph) = - disambiguator#disambiguateTermAst ~metasenv body_ast - in - let (body_type, ugraph) = - CicTypeChecker.type_of_aux' metasenv [] body_cic ugraph - in - let uri = UriManager.uri_of_string (qualify name ^ ".con") in - let (subst, metasenv, ugraph) = - CicUnification.fo_unif metasenv [] body_type type_cic ugraph - in - let body = CicMetaSubst.apply_subst subst body_cic in - let ty = CicMetaSubst.apply_subst subst type_cic in - add_constant_to_world ~console ~dbd ~uri ~body ~ty ~ugraph (); - self#setLastItem (Some (`Def uri)); - Quiet - | TacticAst.Command (TacticAst.Inductive (params, indTypes)) -> - - let (uri, (indTypes, params, leftno)) = - inddef_of_ast params indTypes disambiguator - in - let obj = Cic.InductiveDefinition (indTypes, params, leftno, []) in - let ugraph = - CicTypeChecker.typecheck_mutual_inductive_defs uri - (indTypes, params, leftno) CicUniv.empty_ugraph - in - add_inductive_def_to_world ~console - ~dbd ~uri ~indTypes ~params ~leftno ~ugraph (); - self#setLastItem (Some (`Inductive uri)); - Quiet - | TacticAst.Command TacticAst.Quit -> - currentProof#quit (); - New_state Command (* dummy answer, useless *) - | TacticAst.Command TacticAst.Proof -> - (* do nothing, just for compatibility with coq syntax *) - New_state Command - | TacticAst.Command (TacticAst.Coercion c_ast) -> - let env, metasenv, coercion, ugraph = - disambiguator#disambiguateTermAst c_ast - in - let coer_uri,coer_ty = - match coercion with - | Cic.Const (uri,_) - | Cic.Var (uri,_) -> - let o,_ = - CicEnvironment.get_obj CicUniv.empty_ugraph uri - in - (match o with - | Cic.Constant (_,_,ty,_,_) - | Cic.Variable (_,_,ty,_,_) -> - uri,ty - | _ -> assert false) - | Cic.MutConstruct (uri,t,c,_) -> - let o,_ = - CicEnvironment.get_obj CicUniv.empty_ugraph uri - in - (match o with - | Cic.InductiveDefinition (l,_,_,_) -> - let (_,_,_,cl) = List.nth l t in - let (_,cty) = List.nth cl c in - uri,cty - | _ -> assert false) - | _ -> assert false - in - (* we have to get the source and the tgt type uri - * in Coq syntax we have already their names, but - * since we don't support Funclass and similar I think - * all the coercion should be of the form - * (A:?)(B:?)T1->T2 - * So we should be able to extract them from the coercion type - *) - let extract_last_two_p ty = - let rec aux = function - | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2)) - | Cic.Prod( _, src, tgt) -> src, tgt - | _ -> assert false - in - aux ty - in - let rec uri_of_term = function - | Cic.Const(u,_) -> u - | Cic.MutInd (u, i , _) -> - (* we have to build by hand the #xpointer *) - let base = UriManager.string_of_uri u in - let xp = "#xpointer(1/" ^ (string_of_int (i+1)) ^ ")" in - UriManager.uri_of_string (base ^ xp) - | Cic.Appl (he::_) -> uri_of_term he - | t -> - error ("can't extract uri from " ^ (CicPp.ppterm t)); - assert false - in - let ty_src,ty_tgt = extract_last_two_p coer_ty in - let src_uri = uri_of_term ty_src in - let tgt_uri = uri_of_term ty_tgt in - let coercions_to_add = - CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri - in - (* FIXME: we should chek it this object can be a coercion - * maybe add the check to extract_last_two_p - *) - console#echo_message (sprintf "Coercion %s" - (UriManager.string_of_uri coer_uri)); - List.iter (fun (uri,obj,ugraph) -> - (* - console#echo_message - (sprintf "Coercion (automatic) %s" - (UriManager.string_of_uri uri)); - *) - let (name, body, ty, attrs) = split_obj obj in - add_constant_to_world ~console - ~dbd ~uri ?body ~ty ~attrs ~ugraph (); - ) coercions_to_add; - Quiet - | tactical -> shared#evalTactical tactical - end - - (** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -let namer_of names = - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = Cic.Name (List.nth names !count) in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - - (** Implements phrases that should be accepted only in Proof state, basically - * tacticals *) -class proofState ~(console: #MatitaTypes.console) ?mathViewer () = - let shared = new sharedState ~console ?mathViewer () in - object (self) - inherit interpreterState ~console - - method private disambiguate ast = - let (_, _, term, _) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast - in - term - - (** tactic AST -> ProofEngineTypes.tactic *) - method private lookup_tactic = function - | TacticAst.LocatedTactic (_, tactic) -> self#lookup_tactic tactic - | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *) - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) - () - | TacticAst.Reflexivity -> Tactics.reflexivity - | TacticAst.Assumption -> Tactics.assumption - | TacticAst.Contradiction -> Tactics.contradiction - | TacticAst.Exists -> Tactics.exists - | TacticAst.Fourier -> Tactics.fourier - | TacticAst.Left -> Tactics.left - | TacticAst.Right -> Tactics.right - | TacticAst.Ring -> Tactics.ring - | TacticAst.Split -> Tactics.split - | TacticAst.Symmetry -> Tactics.symmetry - | TacticAst.Transitivity term -> - Tactics.transitivity (self#disambiguate term) - | TacticAst.Apply term -> Tactics.apply (self#disambiguate term) - | TacticAst.Absurd term -> Tactics.absurd (self#disambiguate term) - | TacticAst.Exact term -> Tactics.exact (self#disambiguate term) - | TacticAst.Cut term -> Tactics.cut (self#disambiguate term) - | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *) - Tactics.elim_intros_simpl (self#disambiguate term) - | TacticAst.ElimType term -> Tactics.elim_type (self#disambiguate term) - | TacticAst.Replace (what, with_what) -> - Tactics.replace ~what:(self#disambiguate what) - ~with_what:(self#disambiguate with_what) - | TacticAst.Auto -> Tactics.auto_new ~dbd - | TacticAst.Hint -> - let l = List.map fst - (MetadataQuery.experimental_hint ~dbd - (currentProof#proof#proof,currentProof#proof#goal)) - in - let u = console#choose_uri l in - Tactics.apply (CicUtil.term_of_uri u) - | TacticAst.Change (what, with_what, _) -> - let what = self#disambiguate what in - let with_what = self#disambiguate with_what in - Tactics.change ~what ~with_what - (* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Discriminate of 'ident - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option - | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option - *) - | _ -> MatitaTypes.not_implemented "some tactic" - - method evalTactical = function - | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical - | TacticAst.Command TacticAst.Abort -> - currentProof#abort (); - New_state Command - | TacticAst.Command (TacticAst.Undo steps) -> - currentProof#proof#undo ?steps (); - New_state Proof - | TacticAst.Command (TacticAst.Redo steps) -> - currentProof#proof#redo ?steps (); - New_state Proof - | TacticAst.Command (TacticAst.Qed None) -> - if not (currentProof#onGoing ()) then assert false; - let proof = currentProof#proof in - let (uri, metasenv, bo, ty) = proof#proof in - let uri = MatitaTypes.unopt_uri uri in - let suri = UriManager.string_of_uri uri in - (* TODO Zack this function probably should not simply fail with - * Failure, but rather raise some more meaningful exception *) - if metasenv <> [] then failwith "Proof not completed"; - let proved_ty,ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph - in - let b,ugraph = - CicReduction.are_convertible [] proved_ty ty ugraph - in - if not b then failwith "Wrong proof"; - add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph (); - currentProof#abort (); - console#echo_message (sprintf "%s defined" suri); - self#setLastItem (Some (`Qed uri)); - New_state Command - | TacticAst.Seq tacticals -> - (* TODO ZACK check for proof completed at each step? *) - (* TODO ZACK code completely broken here: we must build logic level - * tacticals instead of iterating interpreter evaluation *) - if (List.length tacticals > 1) then - warning "tacticals are broken: see matitaInterpreter.ml"; - List.iter (fun t -> ignore (self#evalTactical t)) tacticals; - self#setLastItem (Some `Tactic); - New_state Proof - | TacticAst.Tactic tactic_phrase -> - let tactic = self#lookup_tactic tactic_phrase in - currentProof#proof#apply_tactic tactic; - self#setLastItem (Some `Tactic); - New_state Proof - | tactical -> shared#evalTactical tactical - end - -class interpreter ~(console: #MatitaTypes.console) ?mathViewer () = - let commandState = new commandState ~console ?mathViewer () in - let proofState = new proofState ~console ?mathViewer () in - object (self) - val mutable state = commandState - - method setState (tag: [`Proof | `Command]) = - match tag with - | `Proof -> (state <- proofState) - | `Command -> (state <- commandState) - - method endOffset = state#endOffset - - method private updateState = function - | New_state Command -> (state <- commandState) - | New_state Proof -> (state <- proofState) - | _ -> () - - method private eval f = - let ok () = (* console#clear (); *) (true, true) in - match console#wrap_exn f with - | Some (New_state Command) -> (state <- commandState); ok () - | Some (New_state Proof) -> (state <- proofState); ok () - | Some (Echo msg) -> console#echo_message msg; (true, false) - | Some Quiet -> ok () - | None -> (false, false) - - method evalPhrase s = self#eval (fun () -> state#evalPhrase s) - method evalAst ast = self#eval (fun () -> state#evalAst ast) - - (** {2 methods delegated to current state} *) - - method endOffset = state#endOffset - method lastItem = state#lastItem - method setEvalAstCallback = state#setEvalAstCallback - end - -let interpreter ~(console: #MatitaTypes.console) ?mathViewer () = - new interpreter ~console ?mathViewer () - diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli deleted file mode 100644 index a6da315ba..000000000 --- a/helm/matita/matitaInterpreter.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* 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/ - *) - -exception Command_error of string - -val interpreter: - console:#MatitaTypes.console -> - ?mathViewer:MatitaTypes.mathViewer -> - unit -> - MatitaTypes.interpreter - diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml deleted file mode 100644 index 59324f1a1..000000000 --- a/helm/matita/matitaMathView.ml +++ /dev/null @@ -1,511 +0,0 @@ -(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. - *) - -open Printf - -open MatitaCicMisc -open MatitaTypes - -(* List utility functions *) -exception Skip - -let list_map_fail f = - let rec aux = - function - [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Skip -> - (aux tl) - in - aux - -class clickable_math_view obj = - let href = Gdome.domString "href" in - let xref = Gdome.domString "xref" in - object (self) - inherit GMathViewAux.multi_selection_math_view obj - - val mutable href_callback: (string -> unit) option = None - method set_href_callback f = href_callback <- f - - initializer - ignore (self#connect#selection_changed self#choose_selection); - ignore (self#connect#click (fun (gdome_elt, _, _, _) -> - match gdome_elt with - | Some elt (* element is an hyperlink, use href_callback on it *) - when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href -> - (match href_callback with - | None -> () - | Some f -> - let uri = - elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href - in - f (uri#to_string)) - | Some elt -> ignore (self#action_toggle elt) - | None -> ())) - method private choose_selection gdome_elt = - let rec aux elt = - if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then - self#set_selection (Some elt) - else - try - (match elt#get_parentNode with - | None -> assert false - | Some p -> aux (new Gdome.element_of_node p)) - with GdomeInit.DOMCastException _ -> () -(* debug_print "trying to select above the document root" *) - in - match gdome_elt with - | Some elt -> aux elt - | None -> self#set_selection None - end - -let clickable_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity = - GtkBase.Widget.size_params - ~cont:(OgtkMathViewProps.pack_return (fun p -> - OgtkMathViewProps.set_params - (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p)) - ~font_size:None ~log_verbosity:None)) - [] - -class sequent_viewer obj = - object(self) - - inherit clickable_math_view obj - - val mutable current_infos = None - - method get_selected_terms = - let selections = self#get_selections in - list_map_fail - (fun node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - | Some (ids_to_terms,_,_) -> - (try - Hashtbl.find ids_to_terms xpath - with _ -> raise Skip) - | None -> assert false) (* "ERROR: No current term!!!" *) - selections - - method get_selected_hypotheses = - let selections = self#get_selections in - list_map_fail - (fun node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - | Some (_,_,ids_to_hypotheses) -> - (try - Hashtbl.find ids_to_hypotheses xpath - with _ -> raise Skip) - | None -> assert false) (* "ERROR: No current term!!!" *) - selections - - method load_sequent metasenv metano = - let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) = - ApplyTransformation.mml_of_cic_sequent metasenv sequent - in - current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); -(* - debug_print "load_sequent: dumping MathML to ./prova"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); -*) - self#load_root ~root:mathml#get_documentElement - end - - -class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) () -= - let tab_label metano = - (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce - in - let set_goal goal = - let currentProof = MatitaProof.instance () in - assert (currentProof#onGoing ()); - currentProof#proof#set_goal goal - in - object (self) - val mutable pages = 0 - val mutable switch_page_callback = None - val mutable page2goal = [] (* associative list: page no -> goal no *) - val mutable goal2page = [] (* the other way round *) - val mutable goal2win = [] (* associative list: goal no -> scrolled win *) - val mutable _metasenv = [] - val mutable scrolledWin: GBin.scrolled_window option = None - (* scrolled window to which the sequent_viewer is currently attached *) - - method reset = - (match scrolledWin with - | Some w -> - (* removing page from the notebook will destroy all contained widget, - * we do not want the sequent_viewer to be destroyed as well *) - w#remove sequent_viewer#coerce; - scrolledWin <- None - | None -> ()); - for i = 1 to pages do notebook#remove_page 0 done; - pages <- 0; - page2goal <- []; - goal2page <- []; - goal2win <- []; - _metasenv <- []; - (match switch_page_callback with - | Some id -> - GtkSignal.disconnect notebook#as_widget id; - switch_page_callback <- None - | None -> ()) - - method load_sequents metasenv = - let sequents_no = List.length metasenv in - _metasenv <- metasenv; - pages <- sequents_no; - let win metano = - let w = - GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC - ~shadow_type:`IN ~show:true () - in - let reparent () = - scrolledWin <- Some w; - match sequent_viewer#misc#parent with - | None -> w#add sequent_viewer#coerce - | Some _ -> sequent_viewer#misc#reparent w#coerce - in - goal2win <- (metano, reparent) :: goal2win; - w#coerce - in - let page = ref 0 in - List.iter - (fun (metano, _, _) -> - page2goal <- (!page, metano) :: page2goal; - goal2page <- (metano, !page) :: goal2page; - incr page; - notebook#append_page ~tab_label:(tab_label metano) (win metano)) - metasenv; - switch_page_callback <- - Some (notebook#connect#switch_page ~callback:(fun page -> - let goal = - try - List.assoc page page2goal - with Not_found -> assert false - in - set_goal goal; - self#render_page ~page ~goal)) - - method private render_page ~page ~goal = - sequent_viewer#load_sequent _metasenv goal; - try - List.assoc goal goal2win (); - sequent_viewer#set_selection None - with Not_found -> assert false - - method goto_sequent goal = - let page = - try - List.assoc goal goal2page - with Not_found -> assert false - in - notebook#goto_page page; - self#render_page page goal - - end - - (** constructors *) - -type 'widget constructor = - ?hadjustment:GData.adjustment -> - ?vadjustment:GData.adjustment -> - ?font_size:int -> - ?log_verbosity:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> - unit -> - 'widget - -let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = - GtkBase.Widget.size_params - ~cont:(OgtkMathViewProps.pack_return (fun p -> - OgtkMathViewProps.set_params - (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) - ~font_size ~log_verbosity)) - [] - -let blank_uri = BuildTimeConf.blank_uri -let current_proof_uri = BuildTimeConf.current_proof_uri - -exception Browser_failure of string - -let cicBrowsers = ref [] - -class cicBrowser ~(history:string MatitaMisc.history) () = - let term_RE = Pcre.regexp "^term:(.*)" in - let trailing_slash_RE = Pcre.regexp "/$" in - let gui = MatitaGui.instance () in - let win = gui#newBrowserWin () in - let toplevel = win#toplevel in - let mathView = sequent_viewer ~packing:win#scrolledBrowser#add () in - let fail msg = - ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) - ~title:"Cic browser" ~msg ~cancel:false ()); - in - let handle_error f = - try - f () - with exn -> - fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn)) - in - let handle_error' f = fun () -> handle_error f in (* used in callbacks *) - object (self) - initializer - ignore (win#browserUri#connect#activate (handle_error' (fun () -> - self#_loadUri win#browserUri#text))); - ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> - self#_loadUri current_proof_uri))); - ignore (win#browserRefreshButton#connect#clicked - (handle_error' self#refresh)); - ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); - ignore (win#browserForwardButton#connect#clicked - (handle_error' self#forward)); - ignore (win#toplevel#event#connect#delete (fun _ -> - let my_id = Oo.id self in - cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; - if !cicBrowsers = [] && - Helm_registry.get "matita.mode" = "cicbrowser" - then - GMain.quit (); - false)); - mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#_loadUri uri))); - self#_loadUri ~add_to_history:false blank_uri; - toplevel#show (); - - val disambiguator = MatitaDisambiguator.instance () - val currentProof = MatitaProof.instance () - - val mutable current_uri = "" - val mutable current_infos = None - val mutable current_mathml = None - - method private back () = - try - self#_loadUri ~add_to_history:false history#previous - with MatitaMisc.History_failure -> () - - method private forward () = - try - self#_loadUri ~add_to_history:false history#next - with MatitaMisc.History_failure -> () - - (* loads a uri which can be a cic uri or an about:* uri - * @param uri string *) - method private _loadUri ?(add_to_history = true) uri = - try - if current_uri <> uri || uri = current_proof_uri then begin - (match uri with - | uri when uri = blank_uri -> self#blank () - | uri when uri = current_proof_uri -> self#home () - | uri when Pcre.pmatch ~rex:term_RE uri -> - self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1)) - | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri - | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri)); - self#setUri uri; - if add_to_history then history#add uri - end - with - | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri) - | CicEnvironment.Object_not_found _ -> - fail (sprintf "object not found: %s" uri) - | Browser_failure msg -> fail msg - - method loadUri uri = - handle_error (fun () -> self#_loadUri ~add_to_history:true uri) - - method private blank () = - mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement - - method private home () = - if currentProof#onGoing () then - self#loadObj (cicCurrentProof currentProof#proof#proof) - else - raise (Browser_failure "no on going proof") - - (** loads a cic uri from the environment - * @param uri UriManager.uri *) - method private loadUriManagerUri uri = - let uri = UriManager.strip_xpointer uri in - let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - self#loadObj obj - - method private loadDir dir = - let mathml = MatitaMisc.empty_boxml () in - let content = Http_getter.ls dir in - let root = mathml#get_documentElement in - let new_box_elt name = - mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns) - ~qualifiedName:(Gdome.domString ("b:" ^ name)) - in - let new_text content = mathml#createTextNode (Gdome.domString content) in - let b_v = new_box_elt "v" in - List.iter - (fun item -> - let b_text = new_box_elt "text" in - let uri, elt = - match item with - | Http_getter_types.Ls_section subdir -> - (dir ^ subdir ^ "/"), (new_text (subdir ^ "/")) - | Http_getter_types.Ls_object obj -> - (dir ^ obj.Http_getter_types.uri), - (new_text obj.Http_getter_types.uri) - in - b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns) - ~qualifiedName:(Gdome.domString "xlink:href") - ~value:(Gdome.domString uri); - ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node)); - ignore (b_text#appendChild ~newChild:(elt :> Gdome.node))) - content; - ignore (root#appendChild ~newChild:(b_v :> Gdome.node)); -(* Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *) - mathView#load_root ~root:root - - method private setUri uri = - win#browserUri#set_text uri; - current_uri <- uri - - method private loadObj obj = - let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) - let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses,_,_))) = - ApplyTransformation.mml_of_cic_object obj - in - current_infos <- Some (ids_to_terms, ids_to_father_ids, - ids_to_conjectures, ids_to_hypotheses); - match current_mathml with - | Some current_mathml when use_diff -> - mathView#freeze; - XmlDiff.update_dom ~from:current_mathml mathml; - mathView#thaw - | _ -> - mathView#load_root ~root:mathml#get_documentElement; - current_mathml <- Some mathml - - method private _loadTerm s = - self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) - - method private _loadTermAst ast = - let (_, metasenv, term, _) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast - in - self#_loadTermCic term metasenv - - method private _loadTermCic term metasenv = - let (context, _) = - MatitaCicMisc.get_context_and_metasenv currentProof - in - let dummyno = CicMkImplicit.new_meta metasenv [] in - let sequent = (dummyno, context, term) in - mathView#load_sequent (sequent :: metasenv) dummyno - - method loadTerm (src:MatitaTypes.term_source) = - handle_error (fun () -> - (match src with - | `Ast ast -> self#_loadTermAst ast - | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv - | `String s -> self#_loadTerm s); - self#setUri "check") - - (** {2 methods used by constructor only} *) - - method win = win - method history = history - method currentUri = current_uri - method refresh () = - if current_uri = current_proof_uri then - self#_loadUri ~add_to_history:false current_proof_uri - - end - -let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) () -= - new sequents_viewer ~notebook ~sequent_viewer () - -let cicBrowser () = - let size = BuildTimeConf.browser_history_size in - let rec aux history = - let browser = new cicBrowser ~history () in - let win = browser#win in - ignore (win#browserNewButton#connect#clicked (fun () -> - let history = - new MatitaMisc.browser_history ~memento:history#save size "" - in - let newBrowser = aux history in - newBrowser#loadUri browser#currentUri)); -(* - (* attempt (failed) to close windows on CTRL-W ... *) - MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL] - GdkKeysyms._W (fun () -> win#toplevel#destroy ()); -*) - cicBrowsers := browser :: !cicBrowsers; - (browser :> MatitaTypes.cicBrowser) - in - let history = new MatitaMisc.browser_history size blank_uri in - aux history - -let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers - -class mathViewer = - object - method checkTerm (src:MatitaTypes.term_source) = - (cicBrowser ())#loadTerm src - end - -let mathViewer () = new mathViewer - -let default_sequent_viewer () = sequent_viewer ~show:true () -let sequent_viewer_instance = MatitaMisc.singleton default_sequent_viewer - -let default_sequents_viewer () = - let gui = MatitaGui.instance () in - let sequent_viewer = sequent_viewer_instance () in - sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer () -let sequents_viewer_instance = MatitaMisc.singleton default_sequents_viewer - diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli deleted file mode 100644 index 0a1e425e3..000000000 --- a/helm/matita/matitaMathView.mli +++ /dev/null @@ -1,95 +0,0 @@ -(* 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/ - *) - - (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions - * are handled internally. Hyperlinks are handled by calling an user provided - * callback *) -class type clickable_math_view = - object - inherit GMathViewAux.multi_selection_math_view - - (** set hyperlink callback. None disable hyperlink handling *) - method set_href_callback: (string -> unit) option -> unit - end - -class type sequent_viewer = - object - inherit clickable_math_view - - (** @return the list of selected terms. Selections which are not terms are - * ignored *) - method get_selected_terms: Cic.term list - - (** @return the list of selected hypothese. Selections which are not - * hypotheses are ignored *) - method get_selected_hypotheses: Cic.hypothesis list - - (** load a sequent and render it into parent widget *) - method load_sequent: Cic.metasenv -> int -> unit - end - -class type sequents_viewer = - object - method reset: unit - method load_sequents: Cic.metasenv -> unit - method goto_sequent: int -> unit (* to be called _after_ load_sequents *) - end - -(** {2 Constructors} *) - - (** meta constructor *) -type 'widget constructor = - ?hadjustment:GData.adjustment -> - ?vadjustment:GData.adjustment -> - ?font_size:int -> - ?log_verbosity:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> - unit -> - 'widget - -val clickable_math_view: clickable_math_view constructor - -val sequent_viewer: sequent_viewer constructor - -val sequents_viewer: - notebook:GPack.notebook -> - sequent_viewer:sequent_viewer -> - unit -> - sequents_viewer - -val cicBrowser: unit -> MatitaTypes.cicBrowser - -val refresh_all_browsers: unit -> unit - -val mathViewer: unit -> MatitaTypes.mathViewer - -(** {2 singleton instances} *) - -val sequent_viewer_instance: unit -> sequent_viewer -val sequents_viewer_instance: unit -> sequents_viewer - diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml deleted file mode 100644 index 094f965e0..000000000 --- a/helm/matita/matitaMisc.ml +++ /dev/null @@ -1,149 +0,0 @@ -(* 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/ - *) - -open Printf - -let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR -let is_regular fname = (Unix.stat fname).Unix.st_kind = Unix.S_REG - -let input_file fname = - let size = (Unix.stat fname).Unix.st_size in - let buf = Buffer.create size in - let ic = open_in fname in - Buffer.add_channel buf ic size; - close_in ic; - Buffer.contents buf - -let is_proof_script fname = true (** TODO Zack *) -let is_proof_object fname = true (** TODO Zack *) - -let append_phrase_sep s = - if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then - s ^ BuildTimeConf.phrase_sep - else - s - -let strip_trailing_blanks = - let rex = Pcre.regexp "\\s*$" in - fun s -> Pcre.replace ~rex s - -let empty_mathml () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) - ~qualifiedName:(Gdome.domString "math") ~doctype:None - -let empty_boxml () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) - ~qualifiedName:(Gdome.domString "box") ~doctype:None - -exception History_failure - -type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *) - -class type ['a] history = - object - method add : 'a -> unit - method next : 'a - method previous : 'a - method load: 'a memento -> unit - method save: 'a memento - end - -class shell_history size = - let size = size + 1 in - let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in - let incr x = (x + 1) mod size in - object (self) - val data = Array.create size "" - val mutable hd = 0 (* insertion point *) - val mutable tl = -1 (* oldest inserted item *) - val mutable cur = -1 (* current item for the history *) - method add s = - data.(hd) <- s; - if tl = -1 then tl <- hd; - hd <- incr hd; - if hd = tl then tl <- incr tl; - cur <- hd - method previous = - if cur = tl then raise History_failure; - cur <- decr cur; - data.(cur) - method next = - if cur = hd then raise History_failure; - cur <- incr cur; - if cur = hd then "" else data.(cur) - method load (data', hd', tl', cur') = - assert (Array.length data = Array.length data'); - hd <- hd'; tl <- tl'; cur <- cur'; - Array.blit data' 0 data 0 (Array.length data') - method save = (Array.copy data, hd, tl, cur) - end - -class ['a] browser_history ?memento size init = - object (self) - initializer match memento with Some m -> self#load m | _ -> () - val data = Array.create size init - val mutable hd = 0 - val mutable tl = 0 - val mutable cur = 0 - method previous = - if cur = tl then raise History_failure; - cur <- cur - 1; - if cur = ~-1 then cur <- size - 1; - data.(cur) - method next = - if cur = hd then raise History_failure; - cur <- cur + 1; - if cur = size then cur <- 0; - data.(cur) - method add (e:'a) = - cur <- cur + 1; - if cur = size then cur <- 0; - if cur = tl then tl <- tl + 1; - if tl = size then tl <- 0; - hd <- cur; - data.(cur) <- e - method load (data', hd', tl', cur') = - assert (Array.length data = Array.length data'); - hd <- hd'; tl <- tl'; cur <- cur'; - Array.blit data' 0 data 0 (Array.length data') - method save = (Array.copy data, hd, tl, cur) - end - -let dbd_instance = - let dbd = lazy ( - Mysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") - ()) - in - fun () -> Lazy.force dbd - -let singleton f = - let instance = lazy (f ()) in - fun () -> Lazy.force instance - -let mkdirs = List.iter (fun d -> ignore (Unix.system ("mkdir -p " ^ d))) - diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli deleted file mode 100644 index 79219f174..000000000 --- a/helm/matita/matitaMisc.mli +++ /dev/null @@ -1,79 +0,0 @@ -(* 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/ - *) - -val is_dir: string -> bool (** @return true if file is a directory *) -val is_regular: string -> bool (** @return true if file is a regular file *) - -val input_file: string -> string (** read all the contents of file to string *) - - (** @return true if file is a (textual) proof script *) -val is_proof_script: string -> bool - - (** @return true if file is a (binary) proof object *) -val is_proof_object: string -> bool - - (** given a phrase, if it doesn't end with BuildTimeConf.phrase_sep, append - * it *) -val append_phrase_sep: string -> string - -val strip_trailing_blanks: string -> string - - (** Gdome.element of a MathML document whose rendering should be blank. Used - * by cicBrowser to render "about:blank" document *) -val empty_mathml: unit -> Gdome.document -val empty_boxml: unit -> Gdome.document - -exception History_failure - -type 'a memento - -class type ['a] history = - object ('b) - method add : 'a -> unit - method next : 'a (** @raise History_failure *) - method previous : 'a (** @raise History_failure *) - method load: 'a memento -> unit - method save: 'a memento - end - - (** shell like history: new items added at the end of the history - * @param size maximum history size *) -class shell_history : int -> [string] history - - (** browser like history: new items added at the current point of the history - * @param size maximum history size - * @param first element in history (this history is never empty) *) -class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history - - (** create a singleton from a given function. Given function is invoked the - * first time it gets called. Next invocation will return first value *) -val singleton: (unit -> 'a) -> (unit -> 'a) - - (** create a list of directories, building also parents as needed *) -val mkdirs: string list -> unit - - (** {2 db handling} *) -val dbd_instance: unit -> Mysql.dbd - diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml deleted file mode 100644 index 99214e724..000000000 --- a/helm/matita/matitaProof.ml +++ /dev/null @@ -1,155 +0,0 @@ -(* 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/ - *) - -open MatitaCicMisc - -let init_metadata _ = () -let compute_metadata _ _ = () - -(* -let init_metadata status = - let ((_, metasenv, _, _) as proof, _) = status in - let proof_object_metadata = (* compute proof annotations *) - Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) - in - let sequents_metadata = (* compute all sequent annotations from scratch *) - List.map - (fun ((metano, context, term) as sequent) -> - (metano, Cic2acic.asequent_of_sequent metasenv sequent)) - metasenv - in - (proof_object_metadata, sequents_metadata) - -let compute_metadata (old_status, old_metadata) new_status = - let ((_, new_metasenv, _, _) as new_proof, goal_opt) = new_status in - let proof_object_metadata = (* compute proof annotations *) - let obj = - match goal_opt with - | Some _ -> cicCurrentProof new_proof - | None -> cicConstant new_proof - in - Cic2acic.acic_object_of_cic_object obj - in - let sequents_metadata = (* compute all sequent annotations from scratch *) - (** TODO Zack could we reuse some of the annotations from the previous - * status to avoid recomputing all of them? uhm ... we have to which - * sequents haven't been changed by last tactic applications ... doh! *) - List.map - (fun ((metano, context, term) as sequent) -> - (metano, Cic2acic.asequent_of_sequent new_metasenv sequent)) - new_metasenv - in - (proof_object_metadata, sequents_metadata) -*) - -class proof ?uri ~typ ~metasenv ~body () = - object (self) - - inherit [unit] - StatefulProofEngine.status - ~history_size:BuildTimeConf.undo_history_size ?uri ~typ ~body ~metasenv - init_metadata compute_metadata () - - method toXml = - let currentproof = cicCurrentProof self#proof in - let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = - Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof - in - let uri = MatitaTypes.unopt_uri self#uri 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) - - method toString = - let (xml, bodyxml) = self#toXml in - let buf = Buffer.create 10240 in - List.iter (Buffer.add_string buf) - [ "\n"; - "\n"; - "\n"; - (Misc.strip_xml_headings (Xml.pp_to_string xml)); - (Misc.strip_xml_headings(Xml.pp_to_string bodyxml)); - (if not (self#proof_completed) then - Printf.sprintf "%d" self#goal - else - ""); - "\n" - ]; - Buffer.contents buf - - end - -class currentProof = - let fail () = failwith "No current proof" in - object (self) - val mutable _proof: MatitaTypes.proof option = None - val mutable observers = [] - val mutable callbacks = [] - - initializer self#connect `Abort (fun () -> _proof <- None; false) - - (** execute all callbacks related to a given event until one of them - * return true or the end of the callback list is reached *) - method private do_callbacks event = - let rec aux = function - | [] -> () - | (event', f) :: tl when event' = event -> if not (f ()) then aux tl - | _ :: tl -> aux tl - in - aux callbacks - - method addObserver o = observers <- o :: observers - - method connect (event:[`Abort|`Quit]) f = - callbacks <- (event, f) :: callbacks - - method onGoing () = _proof <> None - method proof = match _proof with None -> fail () | Some proof -> proof - method start (proof: MatitaTypes.proof) = - List.iter - (fun observer -> - ignore (proof#attach_observer - ~interested_in:StatefulProofEngine.all_events observer)) - observers; - proof#notify; - _proof <- Some proof - method abort () = self#do_callbacks `Abort - method quit () = self#do_callbacks `Quit - end - -let proof ?uri ~metasenv ~typ () = - let metasenv = (1, [], typ) :: metasenv in - let body = Cic.Meta (1,[]) in - let _ = CicTypeChecker.type_of_aux' metasenv [] typ in - new proof ~typ ~metasenv ~body ?uri () - -let currentProof () = new currentProof -let instance = MatitaMisc.singleton currentProof - diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli deleted file mode 100644 index 9ed622191..000000000 --- a/helm/matita/matitaProof.mli +++ /dev/null @@ -1,59 +0,0 @@ -(* 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/ - *) - - (** create a new proof object. Typecheck the resulting sequent. - * @param typ goal type - * @param metasenv metasenv returned by the disambiguator, this will not be - * the final metasenv of the first sequence, meta corresponding to typ will - * be added - * @param uri new proof uri *) -val proof: - ?uri:UriManager.uri -> - metasenv:Cic.metasenv -> typ:Cic.term -> - unit -> - MatitaTypes.proof - - (** current proof handler *) -class type currentProof = - object - inherit MatitaTypes.currentProof - - (** add an observer to the current observer list. All observers will be - * attached to each new proof (method "start") created by this object - *) - method addObserver: unit StatefulProofEngine.observer -> unit - - (** connect as the first event handler for a given event (abort or quit). - * If the event handler returns true, handler processing stops, otherwise - * continue with the next handler - *) - method connect: [`Abort|`Quit] -> (unit -> bool) -> unit - end - -val currentProof: unit -> currentProof - - (** currentProof singleton instance *) -val instance: unit -> currentProof - diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml deleted file mode 100644 index 69334355f..000000000 --- a/helm/matita/matitaScript.ml +++ /dev/null @@ -1,212 +0,0 @@ -(* Copyright (C) 2005, 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/ - *) - -open Printf - -open MatitaTypes - -exception Script_failure of string - -let remove_constant_from_world ~dbd ~uri = - CicEnvironment.remove_obj uri; - MetadataDb.unindex ~dbd ~uri; - let uri = UriManager.string_of_uri uri in - List.iter - (* TODO ZACK remove xml files from disk *) - (fun suffix -> Http_getter.unregister (uri ^ suffix)) - [""; ".body"; ".types"] - -let remove_inductive_def_from_world ~dbd ~uri = - remove_constant_from_world ~dbd ~uri; - let uri = UriManager.string_of_uri uri in - Http_getter.unregister uri; - List.iter - (fun suffix -> - let uri = - Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri - in - remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri)) - ["ind"; "rec"; "rect"] - -let is_empty = - let rex = Pcre.regexp "^\\s*$" in - fun s -> - Pcre.pmatch ~rex s - -class script ~(interpreter:MatitaTypes.interpreter) () = - let gui = MatitaGui.instance () in - let script = gui#script in - let buf = script#scriptTextView#buffer in - let dbd = MatitaMisc.dbd_instance () in - let rec undo_item = function - | None -> () - | Some item -> - (match item with - | `Tactic -> - let res = - interpreter#evalAst (TacticAst.Command (TacticAst.Undo None)) - in - assert (fst res) - | `Theorem -> - interpreter#setState `Command; - (MatitaMathView.sequents_viewer_instance ())#reset - | `Qed uri - | `Def uri -> remove_constant_from_world ~dbd ~uri - | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri) - in - object (self) - initializer - let console = (MatitaGui.instance ())#console in - let w f () = ignore (console#wrap_exn (fun () -> f ())) in - ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top)); - ignore (gui#script#scriptWinBottomButton#connect#clicked (w self#bottom)); - ignore (gui#script#scriptWinForwardButton#connect#clicked - (w self#forward)); - ignore (gui#script#scriptWinBackButton#connect#clicked (w self#back)); - ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top)); - ignore (gui#script#scriptWinJumpButton#connect#clicked (w self#jump)) - - val mutable items = [] - - (** {3 text buffer locking} *) - - (** text mark and tag representing locked part of a script *) - val locked_mark = - buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter - val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] - - (** lock script text view from the beginning to the given offset (in UTF-8 - * characters) *) - method private lockScript offset = - let mark = `MARK locked_mark in - buf#move_mark mark ~where:(buf#get_iter_at_char offset); - buf#remove_tag locked_tag ~start:buf#start_iter ~stop:buf#end_iter; - buf#apply_tag locked_tag ~start:buf#start_iter - ~stop:(buf#get_iter_at_mark mark) - - method win = gui#script - - method loadFrom fname = - buf#set_text (MatitaMisc.input_file fname); - gui#script#scriptWin#show (); - gui#main#showScriptMenuItem#set_active true - - method advance tactical = - let text = "\n" ^ tactical in - buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text; - let res = self#_forward () in - if not (fst res) then begin - let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - buf#delete ~start:locked_iter - ~stop:(locked_iter#forward_chars (String.length text)); - end; - res - - (** {3 script progress} *) - - method private jump () = - let locked_iter () = buf#get_iter_at_mark (`NAME "locked") in - let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in - let rec forward_until_cursor () = - prerr_endline "forward_until_cursor"; - (* go forward until locked > cursor (or forward fails) *) - let success = - try - fst (self#_forward ~stop:cursor_iter ()) - with - | Script_failure _ | CicTextualParser2.Parse_error _ -> false - in - if success && (locked_iter ())#compare cursor_iter < 0 then - forward_until_cursor () - in - let rec back_until_cursor () = (* go backward until locked < cursor *) - prerr_endline "back_until_cursor"; - let res = self#back () in - if (locked_iter ())#compare cursor_iter > 0 then - back_until_cursor () - in - let cmp = (locked_iter ())#compare cursor_iter in - if cmp < 0 then (* locked < cursor *) - (prerr_endline "locked < cursor"; forward_until_cursor ()) - else if cmp > 0 then (* locked > cursor *) - (prerr_endline "locked > cursor"; back_until_cursor ()) - else (* cursor = locked *) - () - - method private top () = - try while true do self#back () done with Script_failure _ -> () - - method private bottom () = - try - while true do - let res = self#_forward () in - if not (fst res) then raise (Script_failure "error") - done - with Script_failure _ -> () - - method private _forward ?(stop = buf#end_iter) () = - let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - let (success, hide) as res = - let text = buf#get_text ~start:locked_iter ~stop () in - if is_empty text then - raise (Script_failure "at bottom") - else - interpreter#evalPhrase text - in - if success then begin - let old_offset = locked_iter#offset in - let new_offset = old_offset + interpreter#endOffset in - self#lockScript new_offset; - items <- (interpreter#lastItem, old_offset) :: items - end; - res - - method private forward () = ignore (self#_forward ()) - - method private back () = - (* clean history backward until the first theorem, return offset before - * it and remaning history *) - let rec flush_theorem = function - | (Some `Theorem, offset) :: tl -> offset, tl - | _ :: tl -> flush_theorem tl - | [] -> assert false - in - match items with - | [] -> raise (Script_failure "at top") - | (item, last_offset) :: tl -> - undo_item item; - let (last_offset, tl) = - (* if undoing a qed, go back before corresponding theorem *) - match item with - | Some (`Qed _) -> flush_theorem tl - | _ -> last_offset, tl - in - items <- tl; - self#lockScript last_offset - - end - -let script ~interpreter = new script ~interpreter () - diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli deleted file mode 100644 index b1d32eb99..000000000 --- a/helm/matita/matitaScript.mli +++ /dev/null @@ -1,45 +0,0 @@ -(* Copyright (C) 2005, 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/ - *) - - (** script failures (e.g. going before the beginning or after the end of the - * script) *) -exception Script_failure of string - -class type script = - object - (** script window used by this script *) - method win: MatitaGeneratedGui.scriptWin - - (** fill text buffer reading a script from a file *) - method loadFrom: string -> unit - - (** adds a tactical at current script execution point and execute it. Used - * when the user uses buttons or console instead of directly editing the - * script *) - method advance: string -> MatitaTypes.command_outcome - end - -val script: interpreter:MatitaTypes.interpreter -> script - diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml deleted file mode 100644 index 95618d142..000000000 --- a/helm/matita/matitaTypes.ml +++ /dev/null @@ -1,195 +0,0 @@ -(* 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/ - *) - -open Printf - -exception Not_implemented of string -let not_implemented feature = raise (Not_implemented feature) - -exception Failure of string -let error s = raise (Failure s) -let warning s = prerr_endline ("MATITA WARNING:\t" ^ s) -let debug_print s = - if BuildTimeConf.debug then prerr_endline ("MATITA DEBUG:\t" ^ s) - -let explain = function - | StatefulProofEngine.Tactic_failure exn -> - sprintf "Tactic failed: %s"(Printexc.to_string exn) - | StatefulProofEngine.Observer_failures exns -> - String.concat "\n" - (List.map (fun (_, exn) -> Printexc.to_string exn) exns) - | CicTextualParser2.Parse_error (floc, msg) -> - let (x, y) = CicAst.loc_of_floc floc in - sprintf "parse error at character %d-%d: %s" x y msg - | CicEnvironment.Object_not_found uri -> - sprintf "object not found: %s" (UriManager.string_of_uri uri) - | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn) - -exception No_proof - -exception Cancel -exception Unbound_identifier of string - -(* -let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" -let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind" - -let unopt_uri ?(kind = `Con) = function - | Some uri -> uri - | None -> - (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri) -*) -let unopt_uri = function Some uri -> uri | None -> assert false - -class type parserr = (* "parser" is a keyword :-( *) - object - method parseTerm: char Stream.t -> DisambiguateTypes.term - method parseTactical: char Stream.t -> DisambiguateTypes.tactical - end - -class type console = - object - method echo_message : string -> unit - method echo_error : string -> unit - method clear : unit -> unit - method wrap_exn : 'a. (unit -> 'a) -> 'a option - method choose_uri : string list -> string - method show : ?msg:string -> unit -> unit - end - -type choose_uris_callback = - selection_mode:[`MULTIPLE|`SINGLE] -> - ?title:string -> ?msg:string -> ?nonvars_button:bool -> - string list -> - string list -type choose_interp_callback = (string * string) list list -> int list - -class type disambiguator = - object - method env: DisambiguateTypes.environment - method setEnv: DisambiguateTypes.environment -> unit - - method chooseUris: choose_uris_callback - method setChooseUris: choose_uris_callback -> unit - - method chooseInterp: choose_interp_callback - method setChooseInterp: choose_interp_callback -> unit - - method parserr: parserr - - method disambiguateTerm: - ?context:Cic.context -> ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - char Stream.t -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term * - CicUniv.universe_graph) - method disambiguateTermAst: - ?context:Cic.context -> ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - DisambiguateTypes.term -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term * - CicUniv.universe_graph) - - method disambiguateTermAsts: - ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - DisambiguateTypes.term list -> - (DisambiguateTypes.environment * Cic.metasenv * Cic.term list * - CicUniv.universe_graph) - end - -class type proof = - object - inherit [unit] StatefulProofEngine.status - - method toXml: Xml.token Stream.t * Xml.token Stream.t - method toString: string - end - -class type currentProof = - object - method onGoing: unit -> bool - method proof: proof - method start: proof -> unit - method abort: unit -> unit - method quit: unit -> unit - end - -type command_outcome = bool * bool - -type script_item = - [ `Tactic - | `Theorem - | `Qed of UriManager.uri - | `Def of UriManager.uri - | `Inductive of UriManager.uri - ] - -class type interpreter = - object - method evalAst : DisambiguateTypes.tactical -> command_outcome - method evalPhrase : string -> command_outcome -(* method evalStream: char Stream.t -> command_outcome *) - method endOffset : int - method lastItem: script_item option - method setState: [`Proof | `Command] -> unit - method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit - end - -type term_source = - [ `Ast of DisambiguateTypes.term - | `Cic of Cic.term * Cic.metasenv - | `String of string - ] - -class type mathViewer = - object - method checkTerm: term_source -> unit - end - -class type cicBrowser = - object - method loadUri: string -> unit - method loadTerm: term_source -> unit - end - -type mml_of_cic_sequent = - Cic.metasenv -> Cic.conjecture -> - Gdome.document * - ((Cic.id, Cic.term) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * - (string, Cic.hypothesis) Hashtbl.t) - -type mml_of_cic_object = - explode_all:bool -> UriManager.uri -> Cic.annobj -> - (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t -> - Gdome.document - -type namer = ProofEngineTypes.mk_fresh_name_type - -let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ = - raise (Failure "ambiguous input") -let mono_interp_callback _ = raise (Failure "ambiguous input") - diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli deleted file mode 100644 index 262999672..000000000 --- a/helm/matita/matitaTypes.mli +++ /dev/null @@ -1,233 +0,0 @@ -(* 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/ - *) - - (** exceptions whose content should be presented to the user *) -exception Not_implemented of string -exception Failure of string - -val not_implemented : string -> 'a -val error : string -> 'a -val warning : string -> unit -val debug_print : string -> unit - -exception No_proof (** no current proof is available *) -exception Cancel -exception Unbound_identifier of string - - (** @param exn an exception - * @return a string which is meant to be a textual explaination of the - exception understandable by a user *) -val explain: exn -> string - -val unopt_uri : 'a option -> 'a - - (** {3 disambiguator callbacks} *) - -type choose_uris_callback = - selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?title:string -> - ?msg:string -> ?nonvars_button:bool -> string list -> string list - -type choose_interp_callback = (string * string) list list -> int list - - (** @raise Failure if called, use if unambiguous input is required *) -val mono_uris_callback: choose_uris_callback - (** @raise Failure if called, use if unambiguous input is required *) -val mono_interp_callback: choose_interp_callback - -(** {2 major matita objects} *) - -class type parserr = - object - method parseTactical : char Stream.t -> DisambiguateTypes.tactical - method parseTerm : char Stream.t -> DisambiguateTypes.term - end - - (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) -class type console = - object - method clear : unit -> unit - method echo_error : string -> unit - method echo_message : string -> unit - method wrap_exn : 'a. (unit -> 'a) -> 'a option - method choose_uri : string list -> string - method show : ?msg:string -> unit -> unit - end - -class type disambiguator = - object - method env : DisambiguateTypes.environment - method setEnv : DisambiguateTypes.environment -> unit - - method chooseUris: choose_uris_callback - method setChooseUris: choose_uris_callback -> unit - - method chooseInterp: choose_interp_callback - method setChooseInterp: choose_interp_callback -> unit - - method parserr: parserr - - (* TODO Zack: as long as matita doesn't support MDI inteface, - * disambiguateTerm will return a single term *) - (** @param env disambiguation environment. If this parameter is given the - * disambiguator act statelessly, that is internal disambiguation status - * want be changed but only returned. If this parameter is not given the - * internal one will be used and updated with the disambiguation status - * resulting from the disambiguation *) - method disambiguateTerm : - ?context:Cic.context -> - ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - char Stream.t -> - DisambiguateTypes.environment * Cic.metasenv * Cic.term * - CicUniv.universe_graph - - (** @param env @see disambiguateTerm above *) - method disambiguateTermAst : - ?context:Cic.context -> - ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - DisambiguateTypes.term -> - DisambiguateTypes.environment * Cic.metasenv * Cic.term * - CicUniv.universe_graph - - (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All - * AST should be closed hence no context param is permitted on this method - *) - method disambiguateTermAsts : - ?metasenv:Cic.metasenv -> - ?env:DisambiguateTypes.environment -> - DisambiguateTypes.term list -> - DisambiguateTypes.environment * Cic.metasenv * Cic.term list * - CicUniv.universe_graph - end - -class type proof = - object - inherit [unit] StatefulProofEngine.status - - (** return a pair of "xml" (as defined in Xml module) representing the * - * current proof type and body, respectively *) - method toXml : Xml.token Stream.t * Xml.token Stream.t - - method toString : string - end - -class type currentProof = - object - method onGoing: unit -> bool (** true if a proof is on going *) - method proof: proof (** @raise Failure "No current proof" *) - method start: proof -> unit (** starts a new proof *) - method abort: unit -> unit (** abort the on going proof *) - method quit: unit -> unit (** quit matita *) - end - - (** first component represents success: true = success, false = failure - * second component represents console action: true = hide, false = keep *) -type command_outcome = bool * bool - - (** schematic representation of items scripts are made of *) -type script_item = - [ `Tactic (** action on proof status *) - | `Theorem (** start of proof, to be proved *) - | `Qed of UriManager.uri (** end of proof, successfull *) - | `Def of UriManager.uri (** constant with body *) - | `Inductive of UriManager.uri (** inductive definition *) - ] - - (** interpreter for toplevel phrases given via console *) -class type interpreter = - object - (** parse a single phrase contained in the input string. Additional - * garbage at the end of the phrase is ignored - * @return true if no exception has been raised by the evaluation, false - * otherwise - *) - method evalPhrase: string -> command_outcome - - (** as evalPhrase above, but parses a character stream. Only characters - * composing next phrases are consumed *) -(* method evalStream: char Stream.t -> command_outcome *) - - (** as above, evaluating a command/tactics AST *) - method evalAst: DisambiguateTypes.tactical -> command_outcome - - (** {3 callbacks} *) - - method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit - - (** {3 stateful methods} - * bookkeeping of last interpreted phrase *) - - (** offset from the starting of the last string parser by evalPhrase where - * parsing stop. - * @raise Failure when no offset has been recorded *) - method endOffset: int - - (** last item parsed *) - method lastItem: script_item option - - (** change internal interpreter state *) - method setState: [`Proof | `Command] -> unit - - end - -(** {2 MathML widgets} *) - -type term_source = - [ `Ast of DisambiguateTypes.term - | `Cic of Cic.term * Cic.metasenv - | `String of string - ] - -class type mathViewer = - object - method checkTerm: term_source -> unit - end - -class type cicBrowser = - object - method loadUri: string -> unit - method loadTerm: term_source -> unit - end - -type mml_of_cic_sequent = - Cic.metasenv -> - Cic.conjecture -> - Gdome.document * - ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t * - (string, Cic.hypothesis) Hashtbl.t) - -type mml_of_cic_object = - explode_all:bool -> - UriManager.uri -> - Cic.annobj -> - (string, string) Hashtbl.t -> - (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document - -(** {2 shorthands} *) - -type namer = ProofEngineTypes.mk_fresh_name_type - diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml deleted file mode 100644 index 533bbc6a3..000000000 --- a/helm/matita/matitac.ml +++ /dev/null @@ -1,113 +0,0 @@ -(* 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/ - *) - -open Printf - -open MatitaTypes - -let message s = printf "** MatitaC: %s\n" s; flush stdout -let warn s = eprintf "** MatitaC WARNING: %s\n" s; flush stdout -let error s = eprintf "** MatitaC ERROR: %s\n" s; flush stderr - - (** console which prints on stdout/stderr *) -class tty_console = - object (self) - method clear () = () - method echo_message s = message s - method echo_error s = error s - (* TODO Zack: this method is similar to omonymous method in console, - * factorize it in a common super class *) - method wrap_exn: 'a. (unit -> 'a) -> 'a option = - fun f -> - try - Some (f ()) - with exn -> - self#echo_error (explain exn); - None - method show ?(msg = "") () = assert false; () - method choose_uri (uris: string list): string = assert false - end - -(** {2 Initialization} *) - -let arg_spec = [ -(* "-opt", Arg...., "set bla bla bla"; *) -] -let usage = - sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:" - BuildTimeConf.version - -let _ = - Helm_registry.load_from "matita.conf.xml"; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment () - -let scripts = - let acc = ref [] in - let add_script fname = acc := fname :: !acc in - Arg.parse arg_spec add_script usage; - List.rev !acc - -let console = new tty_console -let interpreter = MatitaInterpreter.interpreter ~console () - -let run_script fname = - message (sprintf "execution of %s started:" fname); - let script = - let ic = open_in fname in - let ast = - try - snd (CicTextualParser2.parse_script (Stream.of_channel ic)) - with - exn -> - error (explain exn); - assert false (* should be something like (Unix.exit 1) *) - in - close_in ic; - ast - in - let rec aux = function - | [] -> () (* script is over *) - | DisambiguateTypes.Comment _ :: tl -> aux tl - | DisambiguateTypes.Command ast :: tl -> - let loc = - match ast with - | TacticAst.LocatedTactical (loc, _) -> loc - | _ -> assert false - in - let (success, _) = interpreter#evalAst ast in - if not success then - error (sprintf "%s: error at %s, aborting." fname - (CicAst.pp_location loc)) - else - aux tl - in - aux script; - message (sprintf "execution of %s completed." fname) - -let _ = List.iter run_script scripts - diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma deleted file mode 100644 index 1e92364fe..000000000 --- a/helm/matita/tests/coercions.ma +++ /dev/null @@ -1,50 +0,0 @@ - -Inductive nat : Set \def -| O : nat -| S : nat \to nat. - -Inductive list (A:Set) : Set \def -| nil : list A -| cons : A \to list A \to list A. - -Inductive bool: Set \def -| true : bool -| false : bool. - - - - -let rec len (A:Set)(l:list A) on l : nat \def - match l:list with [ - nil \Rightarrow O - | (cons e tl) \Rightarrow (S (len A tl))]. - -let rec plus (n,m:nat) : nat \def - match n:nat with [ - O \Rightarrow m - | (S x) \Rightarrow (S (plus x m)) ]. - -let rec is_zero (n:nat) : bool \def - match n:nat with [ - O \Rightarrow true - | (S x) \Rightarrow false]. - -let rec nat_eq_dec (n,m:nat) : bool \def - match n:nat with [ - O \Rightarrow - match m:nat with [ - O \Rightarrow true - | (S x) \Rightarrow false] - | (S x) \Rightarrow - match m:nat with [ - O \Rightarrow false - | (S y) \Rightarrow (nat_eq_dec x y)] - ]. - - -Coercion is_zero. -Coercion len. - -Print Coer. -Print Env. - -- 2.39.2