X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=e18f3a0675cd208debb5f985e62f9a010128a980;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=b067e21ec409f004deffeafc2b4aa001a4a63778;hpb=cce6f6dc86e2891f87b2023f35ccc5d73a10a5dd;p=helm.git diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index b067e21ec..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; +