]> matita.cs.unibo.it Git - helm.git/commitdiff
added help on virtuals and UTF-8 equivalence classes
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 Jan 2009 16:07:15 +0000 (16:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 Jan 2009 16:07:15 +0000 (16:07 +0000)
helm/software/matita/help/C/sec_gettingstarted.xml

index b0c0a863e55e1a8c9a69602730f360fa48d3bf30..e18f3a0675cd208debb5f985e62f9a010128a980 100644 (file)
       <listitem><para>Using the &quot;Ctrl+Shift+Unicode code&quot; standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates &quot;Ω&quot;.</para>
      </listitem>
      <listitem><para>Typing the ligature &quot;\name&quot; where &quot;name&quot;
-      is a standard Unicode or LaTeX name for the character. Pressing
-      &quot;Alt+L&quot; just after the last character of the name converts
-      the ligature to the Unicode symbol. This operation is
-      not required since Matita understands also the &quot;\name&quot;
-      sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
-      &quot;Ω&quot;.</para>
+                    is a standard Unicode or LaTeX name for the character or an 
+                    ASCII art resembling the shape of the character. Pressing
+      &quot;Alt+L&quot; or Space or Enter just after the last character 
+      of the name converts
+      the ligature to the Unicode symbol. 
+      E.g. &quot;\Delta&quot; followed by Alt+L generates
+      &quot;Δ&quot;, while pressing Alt-L after &quot;=>&quot; generates
+      &quot;⇒&quot;</para>
      </listitem>
-     <listitem><para>Typing one of the following ligatures (and optionally
-         converting the ligature to the Unicode character has described before):
-         &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for
-         &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).</para>
+     <listitem>
+            <para>Typing a symbol and rotating trough its equivalence class
+                  with Alt-L. E.g. pressing Alt-L after an  &quot;l&quot;
+                  generates a &quot;λ&quot;, while pressing Alt-L after an
+                  &quot;→&quot; once generates &quot;⇉&quot; and pressing
+                  Alt-L again generates &quot;⇒&quot;.
+         </para>
      </listitem>
     </itemizedlist>
+    <para>
+    The comprehensive list of symbols names or shortcuts and their equivalence
+    classes is available clicking on the &quot;TeX/UTF-8 table&quot; item
+    of the &quot;View&quot; menu.
+    </para>
+    <para>
+           There is a memory mechanism related to equivalence classes that
+           remembers your last choice, making it the default one. For example,
+           if you use &quot;_&quot; to generate &quot;⎻&quot; 
+           (that is the third choice, after &quot;⎽&quot; and &quot;⎼&quot;), 
+           the next time you type Alt-L
+           after &quot;_&quot; you immediately get &quot;⎻&quot;.
+    </para>
   </sect1>
   <sect1 id="cicbrowser">
    <title>Browsing and searching</title>