Changes

Summary

more readable output: whitespace is insignificant in HTML;
misc tuning and clarification;
modernized;
more operations;
more operations (see also properties.ML);
tuned signature: avoid conflict with "paragraph" as section heading;
tuned;
support for XML as HTML; tuned;
tuned;
more explicit rev (tip);
just one output file;

Changeset 64362:8a0fe5469ba0 by wenzelm: more readable output: whitespace is insignificant in HTML;
The file was modified	`src/Pure/Thy/html.scala` (diff)
Changeset 64361:07d910a58a14 by wenzelm: misc tuning and clarification;
The file was modified	`src/Pure/Admin/build_release.scala` (diff)
Changeset 64360:cfe8d7394642 by wenzelm: modernized;
The file was modified	`src/Pure/Admin/build_release.scala` (diff)
Changeset 64359:27739e1d7978 by wenzelm: more operations;
The file was modified	`src/Pure/Thy/html.scala` (diff)
Changeset 64358:15c90b744481 by wenzelm: more operations (see also properties.ML);
The file was modified	`src/Pure/General/properties.scala` (diff)
The file was modified	`src/Pure/PIDE/markup.scala` (diff)
The file was modified	`src/Pure/PIDE/xml.scala` (diff)
Changeset 64357:e10fa8afc96c by wenzelm: tuned signature: avoid conflict with "paragraph" as section heading;
The file was modified	`src/Pure/Thy/markdown.ML` (diff)
The file was modified	`src/Pure/Thy/thy_output.ML` (diff)
Changeset 64356:ebbe7cf0c2b8 by wenzelm: tuned;
The file was modified	`src/Pure/Thy/html.scala` (diff)
Changeset 64355:c6a1031cf925 by wenzelm: support for XML as HTML;<br>tuned;
The file was modified	`src/Pure/Thy/html.scala` (diff)
The file was modified	`src/Pure/library.scala` (diff)
Changeset 64354:d9c7a8e83c3d by wenzelm: tuned;
The file was modified	`src/Pure/PIDE/xml.scala` (diff)
Changeset 64353:8f628de5108b by wenzelm: more explicit rev (tip);
The file was modified	`src/Pure/Admin/build_history.scala` (diff)
Changeset 64352:74ece0e491b6 by wenzelm: just one output file;
The file was modified	`Admin/cronjob/crontab.lxbroy10` (diff)