diff options
author | Marco Maggesi <maggesi@math.unifi.it> | 2011-05-14 20:59:53 +0000 |
---|---|---|
committer | Marco Maggesi <maggesi@math.unifi.it> | 2011-05-14 20:59:53 +0000 |
commit | 503f04ca546da08c7479ba5ae5730a235df06c3b (patch) | |
tree | 4ac91dc7d89e9e9d806f4940500c86b116c909c8 /pkgs/applications/editors | |
parent | bfa7c9791ab673436648c2e2f68f62317399e96b (diff) |
ProofGeneral 4.0
svn path=/nixpkgs/trunk/; revision=27252
Diffstat (limited to 'pkgs/applications/editors')
-rw-r--r-- | pkgs/applications/editors/emacs-modes/proofgeneral/default.nix | 25 | ||||
-rw-r--r-- | pkgs/applications/editors/emacs-modes/proofgeneral/emacs-23.3.patch | 45 |
2 files changed, 56 insertions, 14 deletions
diff --git a/pkgs/applications/editors/emacs-modes/proofgeneral/default.nix b/pkgs/applications/editors/emacs-modes/proofgeneral/default.nix index d8316886c34ed..ce01d4b920468 100644 --- a/pkgs/applications/editors/emacs-modes/proofgeneral/default.nix +++ b/pkgs/applications/editors/emacs-modes/proofgeneral/default.nix @@ -1,25 +1,20 @@ { stdenv, fetchurl, emacs, texinfo, texLive, perl, which, automake }: -let - pname = "ProofGeneral"; - version = "3.7.1.1"; - name = "${pname}-${version}"; - website = "http://proofgeneral.inf.ed.ac.uk"; -in - -stdenv.mkDerivation { - inherit name; +stdenv.mkDerivation (rec { + name = "ProofGeneral-4.0"; src = fetchurl { - url = "http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/contrib/${name}.tar.gz"; - sha256 = "ae430590d6763618df50a662a37f0627d3c3c8f31372f6f0bb2116b738fc92d8"; + url = http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.0.tgz; + sha256 = "1ang2lsc97vl70fkgypfsr1ivdzsdliq3bkvympj30wnc7ayzbmq"; }; sourceRoot = name; buildInputs = [ emacs texinfo texLive perl which ]; - patchPhase = + patches = [ ./emacs-23.3.patch ]; + + postPatch = '' sed -i "Makefile" \ -e "s|^\(\(DEST_\)\?PREFIX\)=.*$|\1=$out|g ; \ s|/sbin/install-info|install-info|g" @@ -27,6 +22,8 @@ stdenv.mkDerivation { sed -i "bin/proofgeneral" -e's/which/type -p/g' ''; + preBuild = "make clean"; + installPhase = # Copy `texinfo.tex' in the right place so that `texi2pdf' works. '' cp -v "${automake}/share/"automake-*/texinfo.tex doc @@ -39,8 +36,8 @@ stdenv.mkDerivation { Proof General is a generic front-end for proof assistants (also known as interactive theorem provers), based on the customizable text editor Emacs. ''; - homepage = website; + homepage = http://proofgeneral.inf.ed.ac.uk; license = "GPLv2+"; platforms = stdenv.lib.platforms.gnu; # arbitrary choice }; -} +}) diff --git a/pkgs/applications/editors/emacs-modes/proofgeneral/emacs-23.3.patch b/pkgs/applications/editors/emacs-modes/proofgeneral/emacs-23.3.patch new file mode 100644 index 0000000000000..9bbc21a82b840 --- /dev/null +++ b/pkgs/applications/editors/emacs-modes/proofgeneral/emacs-23.3.patch @@ -0,0 +1,45 @@ +diff -Nuar ProofGeneral-4.0/contrib/mmm/mmm-mode.el ProofGeneral-4.0-nix/contrib/mmm/mmm-mode.el +--- ProofGeneral-4.0/contrib/mmm/mmm-mode.el 2010-10-11 00:56:57.000000000 +0200 ++++ ProofGeneral-4.0-nix/contrib/mmm/mmm-mode.el 2011-05-14 21:55:12.000000000 +0200 +@@ -160,9 +160,9 @@ + (mmm-add-hooks) + (mmm-fixup-skeleton) + (make-local-variable 'font-lock-fontify-region-function) +- (make-local-variable 'font-lock-beginning-of-syntax-function) ++ (make-local-variable 'syntax-begin-function) + (setq font-lock-fontify-region-function 'mmm-fontify-region +- font-lock-beginning-of-syntax-function 'mmm-beginning-of-syntax) ++ syntax-begin-function 'mmm-beginning-of-syntax) + (setq mmm-mode t) + (condition-case err + (mmm-apply-all) +@@ -190,7 +190,7 @@ + (mmm-update-submode-region) + (setq font-lock-fontify-region-function + (get mmm-primary-mode 'mmm-fontify-region-function) +- font-lock-beginning-of-syntax-function ++ syntax-begin-function + (get mmm-primary-mode 'mmm-beginning-of-syntax-function)) + (mmm-update-font-lock-buffer) + (mmm-refontify-maybe) +diff -Nuar ProofGeneral-4.0/contrib/mmm/mmm-region.el ProofGeneral-4.0-nix/contrib/mmm/mmm-region.el +--- ProofGeneral-4.0/contrib/mmm/mmm-region.el 2010-10-11 00:56:57.000000000 +0200 ++++ ProofGeneral-4.0-nix/contrib/mmm/mmm-region.el 2011-05-14 21:58:01.000000000 +0200 +@@ -548,7 +548,7 @@ + (put mode 'mmm-fontify-region-function + font-lock-fontify-region-function)) + (put mode 'mmm-beginning-of-syntax-function +- font-lock-beginning-of-syntax-function)) ++ syntax-begin-function)) + ;; Get variables + (setq global-vars (mmm-get-locals 'global) + buffer-vars (mmm-get-locals 'buffer) +@@ -768,7 +768,7 @@ + ;; For some reason `font-lock-fontify-block' binds this to nil, thus + ;; preventing `mmm-beginning-of-syntax' from doing The Right Thing. + ;; I don't know why it does this, but let's undo it here. +- (let ((font-lock-beginning-of-syntax-function 'mmm-beginning-of-syntax)) ++ (let ((syntax-begin-function 'mmm-beginning-of-syntax)) + (mapc #'(lambda (elt) + (when (get (car elt) 'mmm-font-lock-mode) + (mmm-fontify-region-list (car elt) (cdr elt)))) |