* non-html stuff that was installed in html/members/contract is now
installed in misc/contract.
* the html dir can now be changed as wished. This allows to have
both the "with frames" and the "without frames" versions on-line at
the same time.
* xhtml-content.html can now produce both the version with and without
frames
Great changes in all the stylesheets. Every page is now generated in two
phases:
1) A stylesheet from XML to XHTML that generates the page.
This stylesheet no more bothers with the layout of the page w.r.t. the
rest of the site (i.e. it doesn't add the link to CSS; it doesn't call
the head and foot templates)
2) A common stylesheet from XHTML to HTML that just adds the header, footer
and CSS link to the page.
The idea is that in this way it is easier to change the overall layout of
the site (e.g. removing frames). Moreover, less code is required.
Problem: xsltproc is too intelligent (= rather stupid), so that it
recognises XHTML pages and fails in applying the stylesheet. So, in the
Makefile, care (= sed) must be taken to remove the DOCTYPE definitions
from XHTML files.
* <I> ==> <em> everywhere
* xml/Makefile added: typing make checks the validity of every .xml file in
the xml directory
* every XML file now has a DTD. The files that are pure XHTML documents
use the on-line XHTML 1.0 Transitional DTD.
* A new DTD mowgli-xhtml1-transitional.dtd added. It is an extension of
the XHTML1 Transitional DTD to allow markup in the MOWGLI namespace.
* Notion of future and past events/deadlines introduced.
* Approaching deadlines added to the front page. Should we keep them?
* The stylesheet mess done by Luca has been fixed (i.e. removed) ;-)
1) A serious bug in deadline orderings has been fixed.
2) Events have been splitted (again) into MOWGLI Events and Other Events.
Both of them have a menu entry.
3) The kick-off MOWGLI Event has been added.
The list of persons in the "By Site" ordering is now also
ordered by member status inside the site. Probably, some
more informations will be added soon (e.g. "site leader",
or "work-package leader" etc.)
The list of persons in alphabetical order is now in the form Surname, Name.
The list ordered by site now also uses qualifications. But the output is
still not satisying to me because alphabetical order + qualifications is
quite bad. I will commit manually generated XML index files with a meaningful
order (from boss to slaves ;-)
1) a print_interval template has been put in common.xsl
2) events are now sorted by starting date
3) colors are used to differentiate between submissions, notifications,
and so on. Is this an improvement? ;-|
A new wonderful page that shows the deadlines ordered by date.
Moreover, I have added a new set of functions in commond.xsl
to pretty-print in English a date encoded as 20020218 (that is
easy to sort!).
Luca Padovani [Thu, 14 Feb 2002 21:55:02 +0000 (21:55 +0000)]
- main page now generated automatically
- latest news included in main page
- improved layout
- changed colours
- fix for IE (dismissed blockquote everywhere)
Project Management template added.
Not integrated in the site yet.
Maybe it will become a bunch of XML files once the management groups
will be formed (i.e. during the kick-off).
Deliverables are now described in XML.
The information comes from the table in Sect. 9.4 of the proposal.
Should we try to reproduce that table or is it uninteresting?
Deliverables added.
The idea is that for every deliverable we have an XML file.
When we write a deliverable, we encode it in XML in the same page,
we detect this in XSLT and we create the hyperlink to another page
that renders it.
The Work-Packages index page is no more a static HTML page, but it is
automatically generated from xml/work-packages/index.xml (that will be
also useful in the future).
Irene Schena [Fri, 1 Feb 2002 17:08:31 +0000 (17:08 +0000)]
----------------------------------------------------------------------
Modified Files:
1) arith.xsl mmlctop.xsl-0.14 mmlextension.xsl xslt_index.txt: added
mml presentation for (dis)equalities and new proof elements and some
additions for Algebra elements
Added Files:
2) mmlnotation.xsl: mml presentation notations
----------------------------------------------------------------------
Fixing of guarded_by_constructors completed.
This is the idea of the implementation:
1) The guarded_by_constructors is called on a term which is going to produce
an inductive type (in every branch).
2) The guarded_by_constructors now has also a parameter which is the list
of arguments that are applied to the inductive type that the term
we are cheking is going to produce.
3) Once the constructor is found, its type is "applied" to the list of
arguments its inductive type is applied to. This operation gives us
an instantiated constructor type.
4) Depending on the type of every argument in the instantiated constructor
type, we call either the does_not_occur or the guarded_by_constructors
on every term the constructor is applied to. In case we call the
guarded_by_constructors, we also compute the new parameter (list of
arguments the new inductive type was applied to).
Note that the analysis of the type of the constructors is based very closely
on the analysis of positivy of an inductive type.
Note also that some cases (e.g. a MutCase, a Fix or a CoFix in head position
in the backbone of the type of a constructor) has not been considered and
raises an exception.
PARTIAL COMMIT:
The whole logic of the guarded_by_constructors is being changed.
The new idea is this one:
1) The guarded_by_constructors is applied to a term t which must always
generate an inhabitant of an inductive data type or of a co-inductive
data type.
2) When it find a constructor in head position, then the constructor
must construct the inductive or co-inductive data type of 1).
3) The type of the formal parameter of a constructor determines what
condition is checked on the actual parameters of the constructors:
a) Not recursive: the function must not occur in the actual parameter
b) Simply recursive (to be defined): the function must occur in the
actual parameter only guarded by constructors (where the constructor
has already been found).
c) Imbricated (i.e. it is another inductive type applied to the one
that is going to be recursively defined): in this case the guarded
by constructors (where the constructor has already been found) must
be called, but:
I) the expected inductive data type is no more the old one, but
the one of the inductive data type that is in head position in
the type.
II) Once (if) one constructor of I) will be found, its type must
be considered only after the substitution of the left (?)
parameters and considering recursion IN THE CO-INDUCTIVE TYPE
THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX.
What is still wrong with this commit is that we don't have the notion of
imbricated argument yet. So, as soon as an imbricated argument is found,
the invariant 1-3 are broken and sooner or later an exception is raised
or false is returned.
projects / helm.git / log