Merge branch 'master' of github.com:ProofGeneral/PG

17 files changed, 37 insertions, 53 deletions

diff --git a/doc/ProofGeneral-image.jpg b/doc/ProofGeneral-image.jpg
index ab45a0d9..85babf1b 100644
--- a/doc/ProofGeneral-image.jpg
+++ b/doc/ProofGeneral-image.jpg
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 20b7bed6..79c1e893 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -355,6 +355,9 @@ for patches and suggestions, to Makarius for many bug reports and help
 with Isabelle support and to Pierre Courtieu for providing new
 features for Coq support.
 
+Proof General 4.4's new icons were contributed by Yoshihiro Imai
+(@uref{http://proofcafe.org/wiki/Generaltan) under CC-BY-SA 3.0}
+(@uref{https://creativecommons.org/licenses/by-sa/3.0/})
 
 @c FIXME: watch contributors here!
 During the development of Proof General 3.x and 4.x releases, 
diff --git a/etc/desktop/icons/16x16/proofgeneral.png b/etc/desktop/icons/16x16/proofgeneral.png
index 276c5d29..50a4bc5e 100644
--- a/etc/desktop/icons/16x16/proofgeneral.png
+++ b/etc/desktop/icons/16x16/proofgeneral.png
diff --git a/etc/desktop/icons/32x32/proofgeneral.png b/etc/desktop/icons/32x32/proofgeneral.png
index 576e97cf..9e5cdbfc 100644
--- a/etc/desktop/icons/32x32/proofgeneral.png
+++ b/etc/desktop/icons/32x32/proofgeneral.png
diff --git a/etc/desktop/icons/48x48/proofgeneral.png b/etc/desktop/icons/48x48/proofgeneral.png
index 984a7f77..148bbe6c 100644
--- a/etc/desktop/icons/48x48/proofgeneral.png
+++ b/etc/desktop/icons/48x48/proofgeneral.png
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 11d84715..f2c9dafe 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -81,7 +81,7 @@
       (string-match "Version \\([^ ]+\\)\\." proof-general-version)
       (match-string 1 proof-general-version))))
 
-(defconst proof-general-version-year "2015")
+(defconst proof-general-version-year "2016")
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 19516af4..6bc20998 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -46,38 +46,35 @@ Proof General."
 
 (defcustom proof-splash-contents
   '(list
-    nil
-    (proof-get-image "pg-text" t)
-    nil
-    (proof-get-image "ProofGeneral-image")
+    (proof-get-image "ProofGeneral-splash.png")
     nil
     "Welcome to"
     (concat proof-assistant " Proof General!")
     nil
     (concat "Version " proof-general-short-version ".")
     nil
-    (concat "(C) LFCS, University of Edinburgh " proof-general-version-year)
+    (concat "© LFCS, University of Edinburgh & contributors " proof-general-version-year)
     nil
     nil
     :link '("    Read the "
 	    "Proof General documentation"
-	   (lambda (button) (info "ProofGeneral")))
-    :link '("    Please report problems at "
-	    "Proof General trac"
-	   (lambda (button)
-	     (browse-url "http://proofgeneral.inf.ed.ac.uk/trac"))
-	   "Report bugs at http://proofgeneral.inf.ed.ac.uk/trac")
-    :link '("Visit the " "Proof General wiki"
-	   (lambda (button)
-	     (browse-url "http://proofgeneral.inf.ed.ac.uk/wiki"))
-	   "Write lots of helpful things at http://proofgeneral.inf.ed.ac.uk/wiki")
+            (lambda (button) (info "ProofGeneral")))
+    :link '("    Please report problems on the "
+            "Github issue tracker"
+            (lambda (button)
+              (browse-url "https://github.com/ProofGeneral/PG/issues"))
+            "Report bugs at https://github.com/ProofGeneral/PG")
+    :link '("Visit the " "Proof General Github page"
+            (lambda (button)
+              (browse-url "https://github.com/ProofGeneral/PG"))
+            "PG is on Github at https://github.com/ProofGeneral/PG")
     :link '("or the " "homepage"
-	   (lambda (button)
-	     (browse-url "http://proofgeneral.inf.ed.ac.uk/"))
-	   "Browse http://proofgeneral.inf.ed.ac.uk/")
+            (lambda (button)
+              (browse-url "http://proofgeneral.inf.ed.ac.uk/"))
+            "Browse http://proofgeneral.inf.ed.ac.uk/")
     nil
-     :link '("Find out about Emacs on the Help menu -- start with the "
-	     "Emacs Tutorial" (lambda (button) (help-with-tutorial)))
+    :link '("Find out about Emacs on the Help menu -- start with the "
+            "Emacs Tutorial" (lambda (button) (help-with-tutorial)))
     nil
     "See this screen again with Proof-General -> About"
     )
@@ -117,27 +114,12 @@ If it is nil, a new line is inserted."
   (and (listp img) (eq (car img) 'image)))
 
 
-(defun proof-get-image (name &optional nojpeg default)
-  "Construct an image instantiator for an image, or string failing that.
-Different formats are chosen from according to what can be displayed.
-Unless NOJPEG is set, try jpeg first. Then try gif, then xpm.
-Gif filename depends on colour depth of display.
-DEFAULT gives return value in case image not valid."
-  (let ((jpg (vector 'jpeg :file
-		     (concat proof-images-directory name ".jpg")))
-	(gif (vector 'gif :file
-		     (concat proof-images-directory ".gif")))
-	img)
-  (cond
-   (window-system
-    (find-image
-     (list
-      (list :type 'jpeg
-	    :file (concat proof-images-directory name ".jpg"))
-      (list :type 'gif
-	    :file (concat proof-images-directory name ".gif")))))
-   (t
-    (or default (concat "[ image " name " ]"))))))
+(defun proof-get-image (name)
+  "Load a PNG image NAME, or string on TTYs."
+  (if (display-graphic-p)
+      (find-image
+       `((:type png :file ,(expand-file-name name proof-images-directory))))
+    (concat "[ image " name " ]")))
 
 (defvar proof-splash-timeout-conf nil
   "Holds timeout ID and previous window config for proof splash screen.")
diff --git a/images/ProofGeneral-splash.png b/images/ProofGeneral-splash.png
new file mode 100644
index 00000000..a1006f9f
--- /dev/null
+++ b/images/ProofGeneral-splash.png
diff --git a/images/ProofGeneral.png b/images/ProofGeneral.png
new file mode 100644
index 00000000..bc372424
--- /dev/null
+++ b/images/ProofGeneral.png
diff --git a/images/README b/images/README
index 9bba39f7..10fa1403 100644
--- a/images/README
+++ b/images/README
@@ -1,8 +1,10 @@
 $Id$
 
-Icons for Proof General.
+# Image credits
 
-The images in this directory were made with The Gimp and Inkscape.
+## Icons and button graphics
+
+Most of the images in this directory were made with The Gimp and Inkscape.
 They were created in my spare time as a donation to the Proof General
 project.  The images here are released under the Creative Commons
 license, see https://creativecommons.org/licenses/by-sa/3.0/
@@ -12,17 +14,14 @@ Fitzsimon's Etiquette search icon (under CC 2.0).
 
 [ Inkscape-based icons forthcoming ]
 
-
 Note for developers: the sources for images have been moved
 to the PG graphics repository.
 
-				David Aspinall <da@inf.ed.ac.uk>
-
-
-
-
-
-
-
+                David Aspinall <da@inf.ed.ac.uk>
 
+## Proof General logo
 
+The 2016 “chibi” icons were contributed by Yoshihiro Imai
+(http://proofcafe.org/~yoshihiro503/, http://proofcafe.org/wiki/Generaltan).
+They are available under the CC-BY-SA 3.0 license; for more information, see
+https://creativecommons.org/licenses/by-sa/3.0/
\ No newline at end of file
diff --git a/previous-art/doc/ProofGeneral-image.jpg b/previous-art/doc/ProofGeneral-image.jpg
new file mode 100644
index 00000000..ab45a0d9
--- /dev/null
+++ b/previous-art/doc/ProofGeneral-image.jpg
diff --git a/previous-art/etc/desktop/icons/16x16/proofgeneral.png b/previous-art/etc/desktop/icons/16x16/proofgeneral.png
new file mode 100644
index 00000000..276c5d29
--- /dev/null
+++ b/previous-art/etc/desktop/icons/16x16/proofgeneral.png
diff --git a/previous-art/etc/desktop/icons/32x32/proofgeneral.png b/previous-art/etc/desktop/icons/32x32/proofgeneral.png
new file mode 100644
index 00000000..576e97cf
--- /dev/null
+++ b/previous-art/etc/desktop/icons/32x32/proofgeneral.png
diff --git a/previous-art/etc/desktop/icons/48x48/proofgeneral.png b/previous-art/etc/desktop/icons/48x48/proofgeneral.png
new file mode 100644
index 00000000..984a7f77
--- /dev/null
+++ b/previous-art/etc/desktop/icons/48x48/proofgeneral.png
diff --git a/images/ProofGeneral-image.gif b/previous-art/images/ProofGeneral-image.gif
index 4f83fb95..4f83fb95 100644
--- a/images/ProofGeneral-image.gif
+++ b/previous-art/images/ProofGeneral-image.gif
diff --git a/images/ProofGeneral-image.jpg b/previous-art/images/ProofGeneral-image.jpg
index d2c430cd..d2c430cd 100644
--- a/images/ProofGeneral-image.jpg
+++ b/previous-art/images/ProofGeneral-image.jpg
diff --git a/previous-art/images/ProofGeneral-splash.png b/previous-art/images/ProofGeneral-splash.png
new file mode 100644
index 00000000..9f90884c
--- /dev/null
+++ b/previous-art/images/ProofGeneral-splash.png