NEWS
changeset 17047 e2e2d75bb37b
parent 17016 73c74cb1d744
child 17092 16971afe75f6
equal deleted inserted replaced
17046:8da7f68d0893 17047:e2e2d75bb37b
    49 LaTeX packages (depending on comments in isabellesym.sty) are
    49 LaTeX packages (depending on comments in isabellesym.sty) are
    50 displayed properly, everything else is left verbatim.  isatool display
    50 displayed properly, everything else is left verbatim.  isatool display
    51 and isatool print are used as front ends (these are subject to the
    51 and isatool print are used as front ends (these are subject to the
    52 DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
    52 DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
    53 
    53 
    54 * There is now a flag to control hiding of proofs and some other
    54 * Command tags control specific markup of certain regions of text,
    55 commands (such as 'ML' or 'parse/print_translation') in document
    55 notably folding and hiding.  Predefined tags include "theory" (for
    56 output.  Hiding is enabled by default, and can be disabled by the
    56 theory begin and end), "proof" for proof commands, and "ML" for
    57 option '-H false' of isatool usedir or by resetting the reference
    57 commands involving ML code; the additional tags "visible" and
    58 variable IsarOutput.hide_commands in ML.  Additional commands to be
    58 "invisible" are unused by default.  Users may give explicit tag
    59 hidden may be declared using IsarOutput.add_hidden_commands.
    59 specifications in the text, e.g. ''by %invisible (auto)''.  The
       
    60 interpretation of tags is determined by the LaTeX job during document
       
    61 preparation: see option -V of isatool usedir, or options -n and -t of
       
    62 isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag,
       
    63 \isadroptag.
       
    64 
       
    65 Several document versions may be produced at the same time via isatool
       
    66 usedir (the generated index.html will link all of them).  Typical
       
    67 specifications include ''-V document=theory,proof,ML'' to present
       
    68 theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold
       
    69 proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit
       
    70 these parts without any formal replacement text.  The Isabelle site
       
    71 default settings produce ''document'' and ''outline'' versions as
       
    72 specified above.
    60 
    73 
    61 * Several new antiquotation:
    74 * Several new antiquotation:
    62 
    75 
    63   @{term_type term} prints a term with its type annotated;
    76   @{term_type term} prints a term with its type annotated;
    64 
    77