RE: [racket-users] css and js files when using scribble

[Jos Koot]

Thanks for the clear answer.
I'll try raco pkg install ...,
but command line stuff is troublesome on windows.
But I'll try.
Jos

  _  

From: Matthew Butterick [mailto:m...@mbtype.com] 
Sent: viernes, 25 de noviembre de 2016 23:03
To: Jos Koot
Cc: Racket Users
Subject: Re: [racket-users] css and js files when using scribble



On Nov 25, 2016, at 12:54 PM, Jos Koot <jos.k...@gmail.com> wrote:


Every time I click Scribble HTML in DrRacket 

for a scribble/manual module in a separate directory 
I find that a number of css files and two js files are produced in the same 
directory (Windows 7) 

Are these files always the same? 
If so can't we put them in Appdata.Roaming, in order to avoid multiple copies? 
Or may be they can be pre-included in the Racket tree? 

I expect there is a good reason for generating a new set of css and js files 
for every (HTML) file produced by scribble,

but I have not the slightest idea why. 


IIUC, when you click "Scribble HTML", Scribble makes a self-contained render, 
which necessarily includes the CSS and JavaScript
files that the HTML files depend on. (Corollary: this render has no 
dependencies on local resources, so it can be moved anywhere,
e.g., a remote web server.)

But when you install a package normally (e.g., via `raco pkg install ...`), 
Racket can rely on the shared copy of those files used
by all documentation, so they are not duplicated.


-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] css and js files when using scribble

[Matthew Butterick]

On Nov 25, 2016, at 12:54 PM, Jos Koot  wrote:

> Every time I click Scribble HTML in DrRacket
> 
> for a scribble/manual module in a separate directory 
> I find that a number of css files and two js files are produced in the same 
> directory (Windows 7)
> 
> Are these files always the same? 
> If so can't we put them in Appdata.Roaming, in order to avoid multiple 
> copies? 
> Or may be they can be pre-included in the Racket tree?
> 
> I expect there is a good reason for generating a new set of css and js files 
> for every (HTML) file produced by scribble,
> 
> but I have not the slightest idea why.
> 


IIUC, when you click "Scribble HTML", Scribble makes a self-contained render, 
which necessarily includes the CSS and JavaScript files that the HTML files 
depend on. (Corollary: this render has no dependencies on local resources, so 
it can be moved anywhere, e.g., a remote web server.)

But when you install a package normally (e.g., via `raco pkg install ...`), 
Racket can rely on the shared copy of those files used by all documentation, so 
they are not duplicated.


-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] css and js files when using scribble

[Jos Koot]

Hi,

Every time I click Scribble HTML in DrRacket
for a scribble/manual module in a separate directory
I find that a number of css files and two js files are produced in the same 
directory (Windows 7)

Are these files always the same?
If so can't we put them in Appdata.Roaming, in order to avoid multiple copies?
Or may be they can be pre-included in the Racket tree?

I expect there is a good reason for generating a new set of css and js files 
for every (HTML) file produced by scribble,
but I have not the slightest idea why.

Thanks, Jos



-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.