[isabelle-dev] NEWS: document_tags (update)

2018-06-26 Thread Makarius 
*** Document preparation ***

* System option "document_tags" specifies alternative command tags. This
is occasionally useful to control the global visibility of commands via
session options (e.g. in ROOT).


This refers to Isabelle/88b0e63d58a5, which also provides the updated
documentation. The motivation is the HOL-Analysis manual, which could
use options like this:

  document_variants = "document:manual=-proof,-ML,-unimportant"

  document_tags =
"theorem%important,corollary%important,proposition%important,%unimportant"

This means that the above theorem statements are visible by default, and
if their proof is not tagged otherwise it retains its default tagging.

In contrast, an explicit "lemma %important" in the text makes its proof
also important, and something like "proof %unimportant" will be required
to hide it.


That is a rather minimal change to the previous version of
document_tags, and hopefully sufficient for the release.

Here are further spots for improvement (after the release):

  * improved handling of whitespace surrounding hidden material

  * improved handling (replacement?) of old (*<*)...(*>*) vs. tags

  * ways to specify command tags for a whole region of text (maybe just
in the Prover IDE, not in the source)


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: document_tags

2017-12-06 Thread Tobias Nipkow 


On 05/12/2017 17:21, Makarius wrote:

*** Document preparation ***

* System option "document_tags" specifies a default for otherwise
untagged commands. This is occasionally useful to control the global
visibility of commands via session options (e.g. in ROOT).

* Document markup commands ('section', 'text' etc.) are implicitly
tagged as "document" and visible by default. This avoids the application
of option "document_tags" to these commands.


Thanks for this. Just a bit of context info: this simplifies the creation of 
documents where only a few key parts of a theory are shown (eg main definitions 
and thms). This in turn can be used to produce readable documentation for large 
sessions (like HOL-Analysis).


Tobias



This refers to Isabelle/386a31d6d17a.

An example session is attached.


Makarius



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: document_tags

2017-12-05 Thread Makarius 
*** Document preparation ***

* System option "document_tags" specifies a default for otherwise
untagged commands. This is occasionally useful to control the global
visibility of commands via session options (e.g. in ROOT).

* Document markup commands ('section', 'text' etc.) are implicitly
tagged as "document" and visible by default. This avoids the application
of option "document_tags" to these commands.


This refers to Isabelle/386a31d6d17a.

An example session is attached.


Makarius


Test_Tags.tar.gz
Description: application/gzip
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev