some documentation of show_markup;
authorwenzelm
Thu Oct 04 13:56:32 2012 +0200 (2012-10-04)
changeset 496991301ed115729
parent 49698 f68e237e8c10
child 49700 2d1cbdf6a68b
child 49713 3d07ddf70f8b
some documentation of show_markup;
NEWS
src/Doc/IsarRef/Inner_Syntax.thy
     1.1 --- a/NEWS	Thu Oct 04 11:45:56 2012 +0200
     1.2 +++ b/NEWS	Thu Oct 04 13:56:32 2012 +0200
     1.3 @@ -16,6 +16,11 @@
     1.4      . more plugin options and preferences, based on Isabelle/Scala;
     1.5      . uniform Java 7 platform on Linux, Mac OS X, Windows;
     1.6  
     1.7 +* Configuration option show_markup controls direct inlining of markup
     1.8 +into the printed representation of formal entities --- notably type
     1.9 +and sort constraints.  This enables Prover IDE users to retrieve that
    1.10 +information via tooltips in the output window, for example.
    1.11 +
    1.12  * Command 'ML_file' evaluates ML text from a file directly within the
    1.13  theory, without any predeclaration via 'uses' in the theory header.
    1.14  
     2.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Thu Oct 04 11:45:56 2012 +0200
     2.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Thu Oct 04 13:56:32 2012 +0200
     2.3 @@ -126,6 +126,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{tabular}{rcll}
     2.7 +    @{attribute_def show_markup} & : & @{text attribute} \\
     2.8      @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
     2.9      @{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
    2.10      @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
    2.11 @@ -149,11 +150,21 @@
    2.12  
    2.13    \begin{description}
    2.14  
    2.15 +  \item @{attribute show_markup} controls direct inlining of markup
    2.16 +  into the printed representation of formal entities --- notably type
    2.17 +  and sort constraints.  This enables Prover IDE users to retrieve
    2.18 +  that information via tooltips or popups while hovering with the
    2.19 +  mouse over the output window, for example.  Consequently, this
    2.20 +  option is enabled by default for Isabelle/jEdit, but disabled for
    2.21 +  TTY and Proof~General~/Emacs where document markup would not work.
    2.22 +
    2.23    \item @{attribute show_types} and @{attribute show_sorts} control
    2.24    printing of type constraints for term variables, and sort
    2.25    constraints for type variables.  By default, neither of these are
    2.26    shown in output.  If @{attribute show_sorts} is enabled, types are
    2.27 -  always shown as well.
    2.28 +  always shown as well.  In Isabelle/jEdit, manual setting of these
    2.29 +  options is normally not required thanks to @{attribute show_markup}
    2.30 +  above.
    2.31  
    2.32    Note that displaying types and sorts may explain why a polymorphic
    2.33    inference rule fails to resolve with some goal, or why a rewrite