<listitem><para>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</para>
</listitem>
<listitem><para>Typing the ligature "\name" where "name"
- is a standard Unicode or LaTeX name for the character. Pressing
- "Alt+L" 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 "\name"
- sequences. E.g. "\Omega" followed by Alt+L generates
- "Ω".</para>
+ is a standard Unicode or LaTeX name for the character or an
+ ASCII art resembling the shape of the character. Pressing
+ "Alt+L" or Space or Enter just after the last character
+ of the name converts
+ the ligature to the Unicode symbol.
+ E.g. "\Delta" followed by Alt+L generates
+ "Δ", while pressing Alt-L after "=>" generates
+ "⇒"</para>
</listitem>
- <listitem><para>Typing one of the following ligatures (and optionally
- converting the ligature to the Unicode character has described before):
- ":=" (which stands for ≝); "->" (which stands for
- "→"); "=>" (which stands for "⇒").</para>
+ <listitem>
+ <para>Typing a symbol and rotating trough its equivalence class
+ with Alt-L. E.g. pressing Alt-L after an "l"
+ generates a "λ", while pressing Alt-L after an
+ "→" once generates "⇉" and pressing
+ Alt-L again generates "⇒".
+ </para>
</listitem>
</itemizedlist>
+ <para>
+ The comprehensive list of symbols names or shortcuts and their equivalence
+ classes is available clicking on the "TeX/UTF-8 table" item
+ of the "View" 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 "_" to generate "⎻"
+ (that is the third choice, after "⎽" and "⎼"),
+ the next time you type Alt-L
+ after "_" you immediately get "⎻".
+ </para>
</sect1>
<sect1 id="cicbrowser">
<title>Browsing and searching</title>
</sect1>
<sect1 id="authoring">
<title>Authoring</title>
- <sect2 id="developments">
- <title>How to use developments</title>
- <para>
- A development is a set of scripts files that are strictly related (i.e.
- they depend on each other). &appname; is able to automatically manage
- dependencies among the scripts in a development, compiling them in the
- correct order.
- </para>
+ <sect2 id="compilation">
+ <title>How to compile a script</title>
<para>
- The include statement can be performed by &appname; only if the mentioned
- script is compiled. If both scripts (the one that includes and the included)
- are part of the same development, the included script (and recursively all
- its dependencies) can be compiled automatically. Dependencies among scripts
- belonging to different developments is not implemented yet.
+ Scripts are compiled to base URIs. Base URIs are of the form
+ "cic:/matita/path" and are given once for all for a set
+ of scripts using the "root" file.
</para>
<para>
- The "Developments..." item the File menu (or pressing
- Ctrl+D) opens the Developments window.
- </para>
- <figure><title>The Developments window</title>
- <mediaobject>
- <imageobject>
- <imagedata fileref="developments.png" align="center"/>
- </imageobject>
- <textobject><phrase>Screenshot of the Developments window.</phrase></textobject>
- </mediaobject>
- </figure>
- <para>
- <variablelist><title>Developments window buttons</title>
- <varlistentry><term><filename>New</filename></term>
- <listitem>
- <para>
- To create a new Development the user needs to specify a name<footnote>
- <para>
- The name of the Development should be the name of the directory in
- which it lives. This is not a requirement, but the makefile
- automatically generated by matita in the root directory of the
- development will eventually generate a new Development with a name
- that follows this convention. Having more than one development for
- the same set of files is not an issue.
- </para>
- </footnote>
- and the root directory in which all scripts will be placed,
- eventually organized in subdirectories. The Development should be
- named as the directory in which it lives. A "makefile"
- file is placed in the specified root directory. That makefile
- supports the following targets:
- <variablelist>
- <varlistentry><term><filename>all</filename></term>
- <listitem>
- <para>
- Build the whole development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>clean</filename></term>
- <listitem>
- <para>
- Cleans the whole development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>cleanall</filename></term>
- <listitem>
- <para>
- Resets the user environment (i.e. deleting all the results
- of compilation of every development, including the contents
- of the database). This target should be used only in case
- something goes wrong and &appname; behaves incorrectly.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>scriptname.mo</filename></term>
- <listitem>
- <para>
- Compiles "scriptname.ma"
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Delete</filename></term>
- <listitem>
- <para>
- Decompiles the whole development and removes it.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Build</filename></term>
- <listitem>
- <para>
- Compiles all the scripts in the development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Clean</filename></term>
- <listitem>
- <para>
- Decompiles the whole development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Publish</filename></term>
- <listitem>
- <para>
- All the user developments live in the "user" space. That is, the
- result of the compilation of scripts is placed in his home directory
- and the tuples are placed in personal tables inside the database.
- Publishing a development means putting it in the "library" space. This
- means putting the result of compilation in the same place where the
- standard library lives. This feature will be improved in the future
- to support publishing the development in the "distributed
- library" space (making your development public).
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Close</filename></term>
- <listitem>
- <para>
- Closes the Developments window
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
+ A "root" file has to be placed in the root of a script set,
+ for example, consider the following files and directories, and
+ assume you keep files in "list" separated from files
+ in "sort" (for example the former directory may contain
+ functions and proofs about lists, while latter sorting algorithms
+ for lists):
+<programlisting><![CDATA[
+ list/
+ list.ma (* depending just on the standard library *)
+ utils/
+ swap.ma (* including list.ma *)
+ sort/
+ qsort.ma (* including utils/swap.ma *)
+]]></programlisting>
+ To be able to compile properly the contents of "list"
+ a file called root has to be placed in it. The file should be like
+ the following snippet.
+<programlisting><![CDATA[
+ baseuri=cic:/matita/mydatastructures
+]]></programlisting>
+ This file tells &appname; that objects generated by
+ "list.ma" have to be placed in
+ "cic:/matita/mydatastructures/list" while
+ objects generated by
+ "swap.ma" have to be placed in
+ "cic:/matita/mydatastructures/utils/swap".
+ </para>
+ <para>
+ Once you created the root file, you must generate a depend file.
+ Enter the "list" directory (the root of yuor file set)
+ and type "matitadep". Remember to regenerate the depend file
+ every time you alter the dependencies of your files (for example
+ including other scripts).
+ You can now compile you files typing "matitac".
+ </para>
+ <para>
+ To compile the "sort" directory, create a root file
+ in "sort/" like the following one and then run
+ "matitadep".
+<programlisting><![CDATA[
+ baseuri=cic:/matita/myalgorithms
+ include_paths=../list
+]]></programlisting>
+ The include_paths field can declare a list of paths separated by space.
+ Please omit any "/" from the end of base URIs or paths.
+ </para>
</sect2>
+ <sect2 id="authoringinterface">
+ <title>The authoring interface</title>
+ <para>&TODO;</para>
+ </sect2>
</sect1>
</chapter>
projects / helm.git / blobdiff