From: Stefano Zacchiroli Date: Mon, 12 Jun 2006 11:22:00 +0000 (+0000) Subject: - better formatting/factorization of tables used for grammar description X-Git-Tag: 0.4.95@7852~1341 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=af9c6c84fe2d1a44517c5a7eca569889d452f7cd;p=helm.git - better formatting/factorization of tables used for grammar description - improved rendering toward TeX --- diff --git a/matita/help/C/Makefile b/matita/help/C/Makefile index 329473d06..a25effd58 100644 --- a/matita/help/C/Makefile +++ b/matita/help/C/Makefile @@ -57,10 +57,10 @@ pdf-stamp: $(patsubst %.xml,%.pdf,$(MAIN)) %.fo: %.xml xsltproc $(FO_XSL) $< | xmllint --format - > $@ ifeq ($(TEX_METHOD),docbook2tex) -%.tex: %.xml +%.tex: %.xml $(DEPS) docbook2tex $< else ifeq ($(TEX_METHOD),xsl) -%.tex: %.xml $(TEX_XSL) +%.tex: %.xml $(TEX_XSL) $(DEPS) xsltproc $(TEX_XSL) $< > $@ endif @@ -77,6 +77,5 @@ endif %.ps: %.dvi dvips $< -.PRECIOUS: matita.tex - +.PRECIOUS: matita.tex matita.dvi diff --git a/matita/help/C/matita-tex.xsl b/matita/help/C/matita-tex.xsl index 79a402178..5f51e7cbc 100644 --- a/matita/help/C/matita-tex.xsl +++ b/matita/help/C/matita-tex.xsl @@ -10,5 +10,22 @@ \usepackage{txfonts} \SetUnicodeOption{mathletters} % prefer math-mode letters + 0 + + + + + \begin{tabular}{rcll} + + + \end{tabular} + + + + + \paragraph*{ + + } + diff --git a/matita/help/C/matita-xhtml.xsl b/matita/help/C/matita-xhtml.xsl index e67b48973..099c390f0 100644 --- a/matita/help/C/matita-xhtml.xsl +++ b/matita/help/C/matita-xhtml.xsl @@ -7,6 +7,7 @@ docbook.css + - id"> - uri"> - char"> - uri-step"> - nat"> - term"> - match_pattern"> - args"> - args2"> - sterm"> - intros-spec"> - pattern"> - reduction-kind"> + id"> + uri"> + char"> + uri-step"> + nat"> + term"> + rec_def"> + match_pattern"> + match_branch"> + args"> + args2"> + sterm"> + intros-spec"> + pattern"> + reduction-kind"> ]> diff --git a/matita/help/C/sec_install.xml b/matita/help/C/sec_install.xml index be9ddaa11..eb4cfb17e 100644 --- a/matita/help/C/sec_install.xml +++ b/matita/help/C/sec_install.xml @@ -274,57 +274,60 @@ Quite a few (optional) arguments may be passed to the configure command line to change build time - parameters. They are listed in the table below, together with their - default values. + parameters. They are listed below, together with their + default values: - + <application>configure</application> command line arguments - - - - Argument - Default - Description - - - - - - --with-runtime-dir=dir - - /usr/local/matita/ - Runtime base directory where all &appname; stuff - (executables, configuration files, standard - library, ...) will be installed - - - - --with-dbhost=host - - localhost - Default SQL server hostname. Will be used while - building the standard library during the installation and to - create the default &appname; configuration. May be changed - later in configuration file. - - - --enable-debug - disabled - Enable debugging code. Not for the casual user. - - - - -
- + + + --with-runtime-dir=dir + + + + (Default: + /usr/local/matita) Runtime base directory + where all &appname; stuff (executables, configuration files, + standard library, ...) will be installed + + + + + + + --with-dbhost=host + + + + (Default: localhost) Default SQL server + hostname. Will be used while building the standard library + during the installation and to create the default &appname; + configuration. May be changed later in configuration file. + + + + + + + --enable-debug + + + + (Default: disabled) Enable debugging code. + Not for the casual user. + + + + Then you will manage the build and install process using make as usual. Below are reported the targets you have to invoke in sequence - to build and install. + to build and install: + <application>make</application> targets @@ -357,8 +360,6 @@ - - diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index d2594c718..ab26aae48 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -26,78 +26,90 @@ Terms & co. Lexical conventions - - +
id - &id; + &id; ::= - 〈〈any sequence of letters, underscores or valid XML digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉 + 〈〈any sequence of letters, underscores or valid XML digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉
- +
nat - &nat; + &nat; ::= - 〈〈any sequence of valid XML digits + 〈〈any sequence of valid XML digits〉〉
- +
char - &char; + &char; ::= [a-zA-Z0-9_-]
- +
uri-step - &uri-step; + &uri-step; ::= &char;[&char;]…
- +
uri - &uri; + &uri; ::= [cic:/|theory:/]&uri-step;[/&uri-step;]….&id;[.&id;]…[#xpointer(&nat;/&nat;[/&nat;]…)]
- Terms + + + + - +
Terms - &term; + &term; ::= &sterm; simple or delimited term @@ -141,11 +153,10 @@ | - let - [co]rec - &id; [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term; + + let + [co]rec + &rec_def; (co)recursive definitions @@ -153,10 +164,7 @@ - [and - [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term;]… + [and &rec_def;]… @@ -174,16 +182,32 @@ …user provided notation + + &rec_def; + ::= + + &id; [&id;|(&id;[,&term;]… :&term;)]… + + + + + + + [on &nat;] + [: &term;] + ≝ &term;] + +
- +
Simple terms - &sterm; + &sterm; ::= (&term;) @@ -252,11 +276,9 @@ [ - &match_pattern; ⇒ &term; - [ - | - &match_pattern; ⇒ &term; - ]…] + &match_branch;[|&match_branch;]… + ] + @@ -275,12 +297,12 @@
- +
Arguments - &args; + &args; ::= _[: &term;] @@ -307,16 +329,8 @@ (&id;[,&id;]…[: &term;]) - - -
- - - Miscellaneous arguments - - - &args2; + &args2; ::= &id; @@ -331,12 +345,17 @@
- +
Pattern matching + + &match_branch; + ::= + &match_pattern; ⇒ &term; + - &match_pattern; + &match_pattern; ::= &id; 0-ary constructor @@ -485,12 +504,12 @@ intros-spec -
+
intros-spec - &intros-spec; + &intros-spec; ::= [&nat;] [([&id;]…)] @@ -502,12 +521,12 @@ pattern -
+
pattern - &pattern; + &pattern; ::= &TODO; @@ -522,12 +541,12 @@ Reduction kinds are normalization functions that transform a term to a convertible but simpler one. Each reduction kind can be used both as a tactic argument and as a stand-alone tactic. -
+
reduction-kind - &reduction-kind; + &reduction-kind; ::= demodulate @@ -553,8 +572,8 @@ | unfold [&sterm;] - δ-reduces the constant or variable specified, or that - in head position if none is specified + δ-reduces the constant or variable if specified, or that + in head position