1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Jul 01 17:59:56 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Jul 01 20:43:51 2014 +0200
     1.3 @@ -315,35 +315,6 @@
     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.margin_default: "int Unsynchronized.ref"} \\
    1.12 -  \end{mldecls}
    1.13 -
    1.14 -  \begin{tabular}{rcll}
    1.15 -    @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ %FIXME move?
    1.16 -  \end{tabular}
    1.17 -
    1.18 -  \begin{description}
    1.19 -
    1.20 -  \item @{ML Pretty.margin_default} indicates the global default for
    1.21 -  the right margin of the built-in pretty printer, with initial value
    1.22 -  76.  Note that user-interfaces typically control margins
    1.23 -  automatically when resizing windows, or even bypass the formatting
    1.24 -  engine of Isabelle/ML altogether and do it within the front end via
    1.25 -  Isabelle/Scala.
    1.26 -
    1.27 -  \item @{attribute ML_print_depth} limits the printing depth of the
    1.28 -  ML toplevel pretty printer; the precise effect depends on the ML
    1.29 -  compiler and run-time system.  Typically the limit should be less
    1.30 -  than 10.  Bigger values such as 100--1000 are useful for debugging.
    1.31 -
    1.32 -  \end{description}
    1.33 -*}
    1.34 -
    1.35 -
    1.36  section {* Mixfix annotations \label{sec:mixfix} *}
    1.37  
    1.38  text {* Mixfix annotations specify concrete \emph{inner syntax} of

     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Tue Jul 01 17:59:56 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Tue Jul 01 20:43:51 2014 +0200
     2.3 @@ -1010,6 +1010,11 @@
     2.4      @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.5      @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     2.6    \end{matharray}
     2.7 +  \begin{tabular}{rcll}
     2.8 +    @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
     2.9 +    @{attribute_def ML_source_trace} & : & @{text attribute} & default @{text false} \\
    2.10 +    @{attribute_def ML_exception_trace} & : & @{text attribute} & default @{text false} \\
    2.11 +  \end{tabular}
    2.12  
    2.13    @{rail \<open>
    2.14      (@@{command SML_file} | @@{command ML_file}) @{syntax name}
    2.15 @@ -1091,6 +1096,33 @@
    2.16            let val context' = context
    2.17            in context' end)) *}
    2.18  
    2.19 +text {*
    2.20 +  \begin{description}
    2.21 +
    2.22 +  \item @{attribute ML_print_depth} controls the printing depth of the ML
    2.23 +  toplevel pretty printer; the precise effect depends on the ML compiler and
    2.24 +  run-time system. Typically the limit should be less than 10. Bigger values
    2.25 +  such as 100--1000 are occasionally useful for debugging.
    2.26 +
    2.27 +  \item @{attribute ML_source_trace} indicates whether the source text that
    2.28 +  is given to the ML compiler should be output: it shows the raw Standard ML
    2.29 +  after expansion of Isabelle/ML antiquotations.
    2.30 +
    2.31 +  \item @{attribute ML_exception_trace} indicates whether the ML run-time
    2.32 +  system should print a detailed stack trace on exceptions. The result is
    2.33 +  dependent on the particular ML compiler version. Note that after Poly/ML
    2.34 +  5.3 some optimizations in the run-time systems may hinder exception
    2.35 +  traces.
    2.36 +
    2.37 +  The boundary for the exception trace is the current Isar command
    2.38 +  transactions. It is occasionally better to insert the combinator @{ML
    2.39 +  Runtime.exn_trace} into ML code for debugging
    2.40 +  \cite{isabelle-implementation}, closer to the point where it actually
    2.41 +  happens.
    2.42 +
    2.43 +  \end{description}
    2.44 +*}
    2.45 +
    2.46  
    2.47  section {* Primitive specification elements *}
    2.48