--- a/src/Doc/IsarRef/Inner_Syntax.thy Thu Oct 04 11:45:56 2012 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Thu Oct 04 13:56:32 2012 +0200
@@ -126,6 +126,7 @@
text {*
\begin{tabular}{rcll}
+ @{attribute_def show_markup} & : & @{text attribute} \\
@{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
@{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
@{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
@@ -149,11 +150,21 @@
\begin{description}
+ \item @{attribute show_markup} controls direct inlining of markup
+ into the printed representation of formal entities --- notably type
+ and sort constraints. This enables Prover IDE users to retrieve
+ that information via tooltips or popups while hovering with the
+ mouse over the output window, for example. Consequently, this
+ option is enabled by default for Isabelle/jEdit, but disabled for
+ TTY and Proof~General~/Emacs where document markup would not work.
+
\item @{attribute show_types} and @{attribute show_sorts} control
printing of type constraints for term variables, and sort
constraints for type variables. By default, neither of these are
shown in output. If @{attribute show_sorts} is enabled, types are
- always shown as well.
+ always shown as well. In Isabelle/jEdit, manual setting of these
+ options is normally not required thanks to @{attribute show_markup}
+ above.
Note that displaying types and sorts may explain why a polymorphic
inference rule fails to resolve with some goal, or why a rewrite