1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:48:19 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:49:46 2008 +0100
     1.3 @@ -96,6 +96,132 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Printing limits *}
     1.8 +
     1.9 +text {*
    1.10 +  \begin{mldecls}
    1.11 +    @{index_ML Pretty.setdepth: "int -> unit"} \\
    1.12 +    @{index_ML Pretty.setmargin: "int -> unit"} \\
    1.13 +    @{index_ML print_depth: "int -> unit"} \\
    1.14 +  \end{mldecls}
    1.15 +
    1.16 +  These ML functions set limits for pretty printed text output.
    1.17 +
    1.18 +  \begin{description}
    1.19 +
    1.20 +  \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
    1.21 +  limit the printing depth to @{text d}.  This affects the display of
    1.22 +  types, terms, theorems etc.  The default value is 0, which permits
    1.23 +  printing to an arbitrary depth.  Useful values for @{text d} are 10
    1.24 +  and 20.
    1.25 +
    1.26 +  \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
    1.27 +  assume a right margin (page width) of @{text m}.  The initial margin
    1.28 +  is 76.  User interfaces may adapt this default automatically, when
    1.29 +  resizing windows etc.
    1.30 +
    1.31 +  \item @{ML print_depth}~@{text n} limits the printing depth of the
    1.32 +  ML toplevel pretty printer; the precise effect depends on the ML
    1.33 +  compiler and run-time system.  Typically @{text n} should be less
    1.34 +  than 10.  Bigger values such as 100--1000 are useful for debugging.
    1.35 +
    1.36 +  \end{description}
    1.37 +*}
    1.38 +
    1.39 +
    1.40 +subsection {* Details of printed content *}
    1.41 +
    1.42 +text {*
    1.43 +  \begin{mldecls} 
    1.44 +    @{index_ML show_types: "bool ref"} & default @{ML false} \\
    1.45 +    @{index_ML show_sorts: "bool ref"} & default @{ML false} \\
    1.46 +    @{index_ML show_consts: "bool ref"} & default @{ML false} \\
    1.47 +    @{index_ML long_names: "bool ref"} & default @{ML false} \\
    1.48 +    @{index_ML short_names: "bool ref"} & default @{ML false} \\
    1.49 +    @{index_ML unique_names: "bool ref"} & default @{ML true} \\
    1.50 +    @{index_ML show_brackets: "bool ref"} & default @{ML false} \\
    1.51 +    @{index_ML eta_contract: "bool ref"} \\
    1.52 +    @{index_ML goals_limit: "int ref"} & default @{ML 10} \\
    1.53 +    @{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\
    1.54 +    @{index_ML show_hyps: "bool ref"} & default @{ML false} \\
    1.55 +    @{index_ML show_tags: "bool ref"} & default @{ML false} \\
    1.56 +  \end{mldecls}
    1.57 +
    1.58 +  These global ML variables control the detail of information that is
    1.59 +  displayed for types, terms, theorems, goals etc.
    1.60 +
    1.61 +  \begin{description}
    1.62 +
    1.63 +  \item @{ML show_types} and @{ML show_sorts} control printing of type
    1.64 +  constraints for term variables, and sort constraints for type
    1.65 +  variables.  By default, neither of these are shown in output.  If
    1.66 +  @{ML show_sorts} is set to @{ML true}, types are always shown as
    1.67 +  well.
    1.68 +
    1.69 +  Note that displaying types and sorts may explain why a polymorphic
    1.70 +  inference rule fails to resolve with some goal, or why a rewrite
    1.71 +  rule does not apply as expected.
    1.72 +
    1.73 +  \item @{ML show_consts} controls printing of types of constants when
    1.74 +  printing proof states.  Note that the output can be enormous as
    1.75 +  polymorphic constants often occur at several different type
    1.76 +  instances.
    1.77 +
    1.78 +  \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
    1.79 +  modify the way of printing qualified names in external form.  See
    1.80 +  also the description of document antiquotation options in
    1.81 +  \secref{sec:antiq}.
    1.82 +
    1.83 +  \item @{ML show_brackets} controls insertion of bracketing in pretty
    1.84 +  printed output.  If set to @{ML true}, all sub-expressions of the
    1.85 +  pretty printing tree will be parenthesized, even if this produces
    1.86 +  malformed term syntax!  This crude way of showing the full structure
    1.87 +  of pretty printed entities might help to diagnose problems with
    1.88 +  operator priorities, for example.
    1.89 +
    1.90 +  \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
    1.91 +  terms.
    1.92 +
    1.93 +  The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
    1.94 +  provided @{text x} is not free in @{text f}.  It asserts
    1.95 +  \emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
    1.96 +  g x"} for all @{text x}.  Higher-order unification frequently puts
    1.97 +  terms into a fully @{text \<eta>}-expanded form.  For example, if @{text
    1.98 +  F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
    1.99 +  "\<lambda>h. F (\<lambda>x. h x)"}.
   1.100 +
   1.101 +  Setting @{ML eta_contract} makes Isabelle perform @{text
   1.102 +  \<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
   1.103 +  appears simply as @{text F}.
   1.104 +
   1.105 +  Note that the distinction between a term and its @{text \<eta>}-expanded
   1.106 +  form occasionally matters.
   1.107 +
   1.108 +
   1.109 +  \item @{ML goals_limit} controls the maximum number of subgoals to
   1.110 +  be shown in proof state output.
   1.111 +
   1.112 +  \item @{ML Proof.show_main_goal} controls whether the main result to
   1.113 +  be proven should be displayed.  This information might be relevant
   1.114 +  for schematic goals, to see the current claim being synthesized.
   1.115 +
   1.116 +  \item @{ML show_hyps} controls printing of implicit hypotheses of
   1.117 +  local facts.  Normally, only those hypotheses are displayed that are
   1.118 +  \emph{not} covered by the assumptions of the current context: this
   1.119 +  situation indicates a fault in some tool being used.
   1.120 +
   1.121 +  By setting @{ML show_hyps} to @{ML true}, output of all hypotheses
   1.122 +  can be enforced.  Which is occasionally usefule for diagnostic
   1.123 +  purposes.
   1.124 +
   1.125 +  \item @{ML show_tags} controls printing of extra annotations within
   1.126 +  theorems, such as the case names being attached by the attribute
   1.127 +  @{attribute case_names}.
   1.128 +
   1.129 +  \end{description}
   1.130 +*}
   1.131 +
   1.132 +
   1.133  section {* Mixfix annotations *}
   1.134  
   1.135  text {* Mixfix annotations specify concrete \emph{inner syntax} of

     2.1 --- a/doc-src/IsarRef/style.sty	Thu Nov 13 21:48:19 2008 +0100
     2.2 +++ b/doc-src/IsarRef/style.sty	Thu Nov 13 21:49:46 2008 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4  \newcommand{\Figref}[1]{Figure~\ref{#1}}
     2.5  
     2.6  %% ML
     2.7 -\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
     2.8 +\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
     2.9  \newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
    2.10  
    2.11  %% math