[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] vocabularies
On Wed, 7 Jan 2009, Adam Naumowicz wrote:
Hi Josef,
On Wed, 7 Jan 2009, Josef Urban wrote:
On Wed, 7 Jan 2009, trybulec wrote:
Freek Wiedijk wrote:
Of course you could also have a _separate_ tool that would
find all theorems used by your article, and then update the
article if necessary, by adding missing references to the
theorems directive.
OK with me. You have to write new SCANNER. If SCANNER would pass the
token as the file name,
then action for PARSER is clear: take the spelling and write in on a file
or somewhere.
something like:
perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;]*);/g)
{@a=$1=~m/[\s,](\w*)\s*:/g; @h{@a}=()} print join(",", sort keys %h),"\n"'
foo.miz
I like your 'constructive' argument in the discussion very much :-) Indeed,
it seems to work fast enough to simply put it in the user interface (either
the mizf script or Emacs mode) as an independent pass and not complicate the
parser at all.
which will (rightfully) make Windoze users suffer for their choice of
(non)operating system (why would a mere "user" need a thing like Perl
shipped with OS?? (give him Ms. Word with Mr. Clippy instead! :-))
the usual solution (if we care about them) is to rewrite it in Emacs Lisp,
or really use Pascal and ship another binary; or just tell them to install
Perl if they care, or to use a real OS
But I noticed that your hack, as it stands now, won't work
well with iterative equalities (no semicolon after some by's),
yes, I also ignored "from" which is probably easy
if a reference
starts the justification of the first iteration step (no extra space or
comma) and also if terms like the Cartesian product ([:X,Y:]) occur in the
equalities. Still, a slightly modified version passed a few tests I could
think of right now:
perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;.]*)(;|\.)/g)
{@a=$1=~m/,?(\w*)\s*:/g; @h{@a}=()}
print join(",", sort keys %h),"\n"' foo.miz
looks OK to me
Josef