# HG changeset patch # User wenzelm # Date 1273341191 -7200 # Node ID 7361d5dde9ce332aa6029e966acaa05ffdd4bf77 # Parent 6e7704471eaa43db44b812ca80882c01e55a7e4b discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally; diff -r 6e7704471eaa -r 7361d5dde9ce doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat May 08 19:18:28 2010 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat May 08 19:53:11 2010 +0200 @@ -212,7 +212,6 @@ text {* \begin{mldecls} - @{index_ML Pretty.setdepth: "int -> unit"} \\ @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\ @{index_ML print_depth: "int -> unit"} \\ \end{mldecls} @@ -221,12 +220,6 @@ \begin{description} - \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to - limit the printing depth to @{text d}. This affects the display of - types, terms, theorems etc. The default value is 0, which permits - printing to an arbitrary depth. Other useful values for @{text d} - are 10 and 20. - \item @{ML Pretty.margin_default} indicates the global default for the right margin of the built-in pretty printer, with initial value 76. Note that user-interfaces typically control margins diff -r 6e7704471eaa -r 7361d5dde9ce doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat May 08 19:18:28 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat May 08 19:53:11 2010 +0200 @@ -231,7 +231,6 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\ \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\ \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\ \end{mldecls} @@ -240,12 +239,6 @@ \begin{description} - \item \verb|Pretty.setdepth|~\isa{d} tells the pretty printer to - limit the printing depth to \isa{d}. This affects the display of - types, terms, theorems etc. The default value is 0, which permits - printing to an arbitrary depth. Other useful values for \isa{d} - are 10 and 20. - \item \verb|Pretty.margin_default| indicates the global default for the right margin of the built-in pretty printer, with initial value 76. Note that user-interfaces typically control margins diff -r 6e7704471eaa -r 7361d5dde9ce src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Sat May 08 19:18:28 2010 +0200 +++ b/src/Pure/General/pretty.ML Sat May 08 19:53:11 2010 +0200 @@ -53,7 +53,6 @@ val indent: int -> T -> T val unbreakable: T -> T val margin_default: int Unsynchronized.ref - val setdepth: int -> unit val to_ML: T -> ML_Pretty.pretty val from_ML: ML_Pretty.pretty -> T val symbolicN: string @@ -184,22 +183,6 @@ val margin_default = Unsynchronized.ref 76; (*right margin, or page width*) -(* depth limitation *) - -val depth = Unsynchronized.ref 0; (*maximum depth; 0 means no limit*) -fun setdepth dp = (depth := dp); - -local - fun pruning dp (Block (m, bes, indent, _)) = - if dp > 0 - then block_markup m (indent, map (pruning (dp - 1)) bes) - else str "..." - | pruning _ e = e; -in - fun prune e = if ! depth > 0 then pruning (! depth) e else e; -end; - - (* formatted output *) local @@ -289,7 +272,7 @@ else text |> newline |> indentation block) | String str => format (es, block, after) (string str text)); in - #tx (format ([prune input], (Buffer.empty, 0), 0) empty) + #tx (format ([input], (Buffer.empty, 0), 0) empty) end; end; @@ -314,7 +297,7 @@ fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en | fmt (String (s, _)) = Buffer.add s | fmt (Break (_, wd)) = Buffer.add (output_spaces wd); - in fmt (prune prt) Buffer.empty end; + in fmt prt Buffer.empty end; (* ML toplevel pretty printing *)