]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 6c6530f)
moogle syntax help page, actually contains only syntax and examples for
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Dec 2004 16:05:27 +0000 (16:05 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Dec 2004 16:05:27 +0000 (16:05 +0000)
the "locate" query. "hint", "match" and "elim" syntaxes are currently
undocumented

helm/searchEngine/html/moogle_syntax.html [new file with mode: 0644] patch | blob

diff --git a/helm/searchEngine/html/moogle_syntax.html b/helm/searchEngine/html/moogle_syntax.html
new file mode 100644 (file)
index 0000000..80e45ca
--- /dev/null
+++ b/helm/searchEngine/html/moogle_syntax.html
@@ -0,0 +1,57 @@
+<html>
+  <head>
+    <style type="text/css">
+      ul.spaced li { padding-bottom: 1em; }
+      ul.empty li { list-style-type: none; }
+    </style>
+  </head>
+  <body>
+    <table>
+      <tr>
+       <td>
+         <img align="center" src="http://helm.cs.unibo.it/moogle.png" alt="moogle" />
+       </td>
+      </tr>
+      <tr>
+       <td>
+         <h2>Moogle Input Syntax</h2>
+         <ul class="spaced">
+           <li>
+           <b>locate <em>&lt;pattern&gt;</em></b>
+           <p>
+           <em>&lt;pattern&gt;</em> is a shell like pattern which could
+           include <tt>*</tt> (denoting any sequence of 0 or more characters)
+           and <tt>?</tt> (denoting any single character).<br />
+           </p>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>nat</tt> pattern matches
+             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
+             </li>
+             <li> <tt>n?t</tt> pattern matches
+             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
+             <tt>cic:/Coq/Init/Logic/not.con</tt>
+             </li>
+             <li> <tt>nat*</tt> pattern matches
+             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
+             <tt>cic:/Coq/Init/Peano/nat_case.con</tt> and many more
+             </li>
+           </ul>
+           </p>
+           </li>
+           <li>
+           <b>hint</b>
+           </li>
+           <li>
+           <b>match</b>
+           </li>
+           <li>
+           <b>elim</b>
+           </li>
+         </ul>
+       </td>
+      </tr>
+    </table>
+  </body>
+</html>
Unnamed repository; edit this file 'description' to name the repository.