Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explain special control symbols;
authorwenzelm
Sun, 19 Jun 2011 22:53:15 +0200
changeset 43470 3d42dea16357
parent 43469 882108e9536a
child 43471 7ab4be64575d
explain special control symbols;
src/Tools/jEdit/README.html file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/README.html	Sun Jun 19 22:52:49 2011 +0200
+++ b/src/Tools/jEdit/README.html	Sun Jun 19 22:53:15 2011 +0200
@@ -4,6 +4,9 @@
 
 <head>
 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<style type="text/css" media="screen">
+body { font-family: IsabelleText; font-size: 14pt; }
+</style>
 <title>Notes on the Isabelle/jEdit Prover IDE</title>
 </head>
 
@@ -47,6 +50,14 @@
     <tt>\&lt;foo&gt;</tt>, <tt>\&lt;bar&gt;</tt>, <tt>\&lt;baz&gt;</tt>, &hellip;<br/>
   </li>
 
+  <li>There are some special control symbols to modify the style of a
+  <em>single</em> symbol:<br/>
+    &#8681; subscript<br/>
+    &#8679; superscript<br/>
+    &#8675; subscript within identifier<br/>
+    &#8673; superscript within identifier<br/>
+    &#10073; bold face</li>
+
   <li>A default mapping relates some Isabelle symbols to Unicode points
     (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
   </li>
@@ -80,6 +91,13 @@
       <tr><td>noteq</td>          <td><tt>~=</tt></td>          <td>&ne;</td></tr>
       <tr><td>in</td>             <td><tt>:</tt></td>           <td>&isin;</td></tr>
       <tr><td>notin</td>          <td><tt>~:</tt></td>          <td>&notin;</td></tr>
+
+      <tr><td>sub</td>            <td><tt>=_</tt></td>          <td>&#8681;</td></tr>
+      <tr><td>sup</td>            <td><tt>=^</tt></td>          <td>&#8679;</td></tr>
+      <tr><td>isup</td>           <td><tt>-_</tt></td>          <td>&#8675;</td></tr>
+      <tr><td>isub</td>           <td><tt>-^</tt></td>          <td>&#8673;</td></tr>
+      <tr><td>bold</td>           <td><tt>-.</tt></td>          <td>&#10073;</td></tr>
+
     </table>
     </li>
   </ul>
isabelle