[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] "one line" form of abstracts



On Thu, 8 Aug 2002, Artur Kornilowicz wrote:

> On Thu, 8 Aug 2002, Freek Wiedijk wrote:
> 
> > >Grep is not bad,
> >
> > The main problem for me is the crossing of lines.  It would
> > be useful to have a version of the MML abstracts in which
> > each statement is printed in exactly one long line, and using
> > some standard style of spacing.
> >
> > Freek
> >
> 
> 
> Four, five years ago I was wondering if we should distribute such a
> version of the MML abstracts (useful for grepping). Maybe we should
> distribute a program, which will rewrite the abstracts to "one line" form
> and each user will prepare such version locally.
> I will do such a program in a few days.


It is a fix, but I would prefer to have such functions in Query. It is not
difficult - both Perl and SQL support regexp searching, some SQL's even
regexp indexing - and the Query results can be linked to other Query 
tools.

Josef