added screenshots describing matita features

diff --git a/helm/www/matita/images/MINI_screenshot-cicbrowser-browsing.png b/helm/www/matita/images/MINI_screenshot-cicbrowser-browsing.png
new file mode 100644 (file)
index 0000000..e5c1d55
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-cicbrowser-browsing.png differ

diff --git a/helm/www/matita/images/MINI_screenshot-cicbrowser-proof.png b/helm/www/matita/images/MINI_screenshot-cicbrowser-proof.png
new file mode 100644 (file)
index 0000000..469fbb9
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-cicbrowser-proof.png differ

diff --git a/helm/www/matita/images/MINI_screenshot-cicbrowser-query.png b/helm/www/matita/images/MINI_screenshot-cicbrowser-query.png
new file mode 100644 (file)
index 0000000..08c0525
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-cicbrowser-query.png differ

diff --git a/helm/www/matita/images/MINI_screenshot-matita-href.png b/helm/www/matita/images/MINI_screenshot-matita-href.png
new file mode 100644 (file)
index 0000000..22b878c
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-matita-href.png differ

diff --git a/helm/www/matita/images/MINI_screenshot-matita-selection.png b/helm/www/matita/images/MINI_screenshot-matita-selection.png
new file mode 100644 (file)
index 0000000..66a045a
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-matita-selection.png differ

diff --git a/helm/www/matita/images/MINI_screenshot-matita.png b/helm/www/matita/images/MINI_screenshot-matita.png
new file mode 100644 (file)
index 0000000..5296d0f
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-matita.png differ

diff --git a/helm/www/matita/images/MINI_screenshot-tinycals.png b/helm/www/matita/images/MINI_screenshot-tinycals.png
new file mode 100644 (file)
index 0000000..c6a9491
Binary files /dev/null and b/helm/www/matita/images/MINI_screenshot-tinycals.png differ

diff --git a/helm/www/matita/images/README.minis b/helm/www/matita/images/README.minis
new file mode 100644 (file)
index 0000000..05d5552
--- /dev/null
+++ b/helm/www/matita/images/README.minis
@@ -0,0 +1,4 @@
+To generate miniatures:
+
+  for f in screenshot-* ; do convert -resize 100 $f MINI_$f ; done
+

diff --git a/helm/www/matita/images/bg0.png b/helm/www/matita/images/bg0.png
new file mode 100644 (file)
index 0000000..fc75123
Binary files /dev/null and b/helm/www/matita/images/bg0.png differ

diff --git a/helm/www/matita/images/bg1.png b/helm/www/matita/images/bg1.png
new file mode 100644 (file)
index 0000000..f2aa2ce
Binary files /dev/null and b/helm/www/matita/images/bg1.png differ

diff --git a/helm/www/matita/images/bg2.png b/helm/www/matita/images/bg2.png
new file mode 100644 (file)
index 0000000..4253823
Binary files /dev/null and b/helm/www/matita/images/bg2.png differ

diff --git a/helm/www/matita/images/bg3.png b/helm/www/matita/images/bg3.png
new file mode 100644 (file)
index 0000000..081b149
Binary files /dev/null and b/helm/www/matita/images/bg3.png differ

diff --git a/helm/www/matita/images/screenshot-cicbrowser-browsing.png b/helm/www/matita/images/screenshot-cicbrowser-browsing.png
new file mode 100644 (file)
index 0000000..76bb482
Binary files /dev/null and b/helm/www/matita/images/screenshot-cicbrowser-browsing.png differ

diff --git a/helm/www/matita/images/screenshot-cicbrowser-proof.png b/helm/www/matita/images/screenshot-cicbrowser-proof.png
new file mode 100644 (file)
index 0000000..f52bc6e
Binary files /dev/null and b/helm/www/matita/images/screenshot-cicbrowser-proof.png differ

diff --git a/helm/www/matita/images/screenshot-cicbrowser-query.png b/helm/www/matita/images/screenshot-cicbrowser-query.png
new file mode 100644 (file)
index 0000000..c19c382
Binary files /dev/null and b/helm/www/matita/images/screenshot-cicbrowser-query.png differ

diff --git a/helm/www/matita/images/screenshot-matita-href.png b/helm/www/matita/images/screenshot-matita-href.png
new file mode 100644 (file)
index 0000000..699d1e1
Binary files /dev/null and b/helm/www/matita/images/screenshot-matita-href.png differ

diff --git a/helm/www/matita/images/screenshot-matita-selection.png b/helm/www/matita/images/screenshot-matita-selection.png
new file mode 100644 (file)
index 0000000..5c85bd3
Binary files /dev/null and b/helm/www/matita/images/screenshot-matita-selection.png differ

diff --git a/helm/www/matita/images/screenshot-matita.png b/helm/www/matita/images/screenshot-matita.png
new file mode 100644 (file)
index 0000000..b72080b
Binary files /dev/null and b/helm/www/matita/images/screenshot-matita.png differ

diff --git a/helm/www/matita/images/screenshot-tinycals.png b/helm/www/matita/images/screenshot-tinycals.png
new file mode 100644 (file)
index 0000000..c64612e
Binary files /dev/null and b/helm/www/matita/images/screenshot-tinycals.png differ

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 403c06db6b98c3003eb152d8b108634bd93394d7..8d6a75f292791576df284c3dbd714e3bbb7e16ae 100644 (file)
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -27,21 +27,59 @@
       proof language is procedural in the same spirit of LCF. </p>
 
       <p> Matita is <strong>innovative</strong>: </p>
-      <ul class="wide">
+      <ul class="with_screenshots">
 
-       <li> the user interface sports high quality bidimensional rendering of
-       proofs and formulae transformed on-the-fly to
-       <a href="http://www.w3.org/Math/">MathML</a> markup, on which direct
-       manipulation of the underlying CIC terms is still possible; </li>
+       <li>
+       <p>
+       <span class="screenshots">
+         <a class="quiet" href="images/screenshot-matita-href.png">
+           <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
+         </a>
+         <a class="quiet" href="images/screenshot-matita-selection.png">
+           <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
+         </a>
+       </span>
+       the user interface sports high quality bidimensional rendering of
+       proofs and formulae transformed on-the-fly to <a
+         href="http://www.w3.org/Math/">MathML</a> markup, on which direct
+       manipulation of the underlying CIC terms is still possible;
+       </p>
+       </li>
 
-       <li> the knowledge base is distributed: every authored concepts can be
-       published becoming part of the Matita library which can be browsed as
-       an hypertext (locally or on the World Wide Web) and searched by means
-       of content-based queries; </li>
+       <li>
+       <p>
+       <span class="screenshots">
+         <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
+           <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
+         </a>
+         <a class="quiet" href="images/screenshot-cicbrowser-query.png">
+           <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
+         </a>
+         <!--
+         <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
+           <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
+         </a>
+         -->
+       </span>
+       the knowledge base is distributed: every authored concepts can be
+       published becoming part of the Matita library which can be <a
+         href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+       (locally or on the World Wide Web) and <a
+         href="http://helm.cs.unibo.it/whelp/"> searched by means of
+         content-based queries</a>; </p>
+       </li>
 
-       <li> the tactical language, part of the proof language, has
+       <li>
+       <p>
+       <span class="screenshots">
+         <a class="quiet" href="images/screenshot-tinycals.png">
+           <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
+         </a>
+       </span>
+       the tactical language, part of the proof language, has
        step-by-step semantics, enabling inspection and replaying of deeply
-       structured proof scripts. </li>
+       structured proof scripts. </p>
+       </li>
 
       </ul>
 

diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css
index 6d8bedea96d6e54dc7232a740c555b3c421647a0..98fc1d9de3aee41a2e9f0eadcf5b1bcbdaad40bb 100644 (file)
--- a/helm/www/matita/style.css
+++ b/helm/www/matita/style.css
@@ -148,3 +148,10 @@ pre.code {
   font-size: 95%;
 }
 
+ul.with_screenshots li {
+}
+
+ul.with_screenshots li p span.screenshots {
+  float: right;
+}
+

diff --git a/helm/www/matita/xhtml-header.shtml b/helm/www/matita/xhtml-header.shtml
index a78b3ccf58adff9fc7d112c4e5f5cbbec6dc40ad..ad156d65104333e228904b5df3ccc93616ff915f 100644 (file)
--- a/helm/www/matita/xhtml-header.shtml
+++ b/helm/www/matita/xhtml-header.shtml
@@ -2,4 +2,4 @@
 <?xml version="1.0" encoding="UTF-8" ?>
 <?xml-stylesheet type="text/css" href="style.css" ?>
 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
-  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">