X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=e18f3a0675cd208debb5f985e62f9a010128a980;hb=e91e815449698c6f2595958f94cd06c10ba10398;hp=8680f4b4371eaf8118950eaa322cb9afd1e9acd7;hpb=a3dec92d472a53ec1f87e927e1ef118b4e04a5bd;p=helm.git
diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml
index 8680f4b43..e18f3a067 100644
--- a/helm/software/matita/help/C/sec_gettingstarted.xml
+++ b/helm/software/matita/help/C/sec_gettingstarted.xml
@@ -16,19 +16,37 @@
Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".
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
- "Ω".
+ 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
+ "â"
- 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 "â").
+
+ 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 "â".
+
+
+ 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.
+
+
+ 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 "â»".
+
Browsing and searching
@@ -88,134 +106,65 @@
Authoring
-
- How to use developments
-
- 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.
-
+
+ How to compile a script
- 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.
- The "Developments..." item the File menu (or pressing
- Ctrl+D) opens the Developments window.
-
- The Developments window
-
-
-
-
- Screenshot of the Developments window.
-
-
-
- Developments window buttons
- New
-
-
- To create a new Development the user needs to specify a name
-
- 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.
-
-
- 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:
-
- all
-
-
- Build the whole development.
-
-
-
- clean
-
-
- Cleans the whole development.
-
-
-
- cleanall
-
-
- 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.
-
-
-
- scriptname.mo
-
-
- Compiles "scriptname.ma"
-
-
-
-
-
-
-
- Delete
-
-
- Decompiles the whole development and removes it.
-
-
-
- Build
-
-
- Compiles all the scripts in the development.
-
-
-
- Clean
-
-
- Decompiles the whole development.
-
-
-
- Publish
-
-
- 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).
-
-
-
- Close
-
-
- Closes the Developments window
-
-
-
-
-
+ 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):
+
+ 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.
+
+ 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".
+
+
+ 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".
+
+
+ To compile the "sort" directory, create a root file
+ in "sort/" like the following one and then run
+ "matitadep".
+
+ The include_paths field can declare a list of paths separated by space.
+ Please omit any "/" from the end of base URIs or paths.
+
+
+ The authoring interface
+ &TODO;
+