[Ur] time measurement

[Ron de Bruijn]

Op vrijdag 27-01-2012 om 04:52 uur [tijdzone -0500], schreef Gergely
Buday:
> Hi,
> 
> as I see, time measurement is in seconds in Ur/Web:
> 
> val diffInSeconds : time -> time -> int
> 
> is there any reason that we cannot measure time in milliseconds? I
> would need it for profiling.
The reason is that nobody needed it yet. I think the general approach is
to only add things based on needs. 

That said, I did take a short look at how it could be implemented.
Basically you just need to add something to urweb.c that calls:
gettimeofday (see man gettimeofday). 

You would also add a version to urweb.js (IIRC) and then there was some
file in which all of these functions that are listed (you can find it on
the mailinglist) to which this symbol then should be added. 

Then recompile urweb and you should have what you need. 

-- 
Best regards,
  Ron de Bruijn