1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 16:53:53 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 19:14:13 2010 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4  text {*
     1.5    \begin{mldecls}
     1.6      @{index_ML Pretty.setdepth: "int -> unit"} \\
     1.7 -    @{index_ML Pretty.setmargin: "int -> unit"} \\
     1.8 +    @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
     1.9      @{index_ML print_depth: "int -> unit"} \\
    1.10    \end{mldecls}
    1.11  
    1.12 @@ -227,10 +227,12 @@
    1.13    printing to an arbitrary depth.  Other useful values for @{text d}
    1.14    are 10 and 20.
    1.15  
    1.16 -  \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
    1.17 -  assume a right margin (page width) of @{text m}.  The initial margin
    1.18 -  is 76, but user interfaces might adapt the margin automatically when
    1.19 -  resizing windows.
    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 @{ML print_depth}~@{text n} limits the printing depth of the
    1.28    ML toplevel pretty printer; the precise effect depends on the ML

     2.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 16:53:53 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 19:14:13 2010 +0200
     2.3 @@ -232,7 +232,7 @@
     2.4  \begin{isamarkuptext}%
     2.5  \begin{mldecls}
     2.6      \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
     2.7 -    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
     2.8 +    \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
     2.9      \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
    2.10    \end{mldecls}
    2.11  
    2.12 @@ -246,10 +246,12 @@
    2.13    printing to an arbitrary depth.  Other useful values for \isa{d}
    2.14    are 10 and 20.
    2.15  
    2.16 -  \item \verb|Pretty.setmargin|~\isa{m} tells the pretty printer to
    2.17 -  assume a right margin (page width) of \isa{m}.  The initial margin
    2.18 -  is 76, but user interfaces might adapt the margin automatically when
    2.19 -  resizing windows.
    2.20 +  \item \verb|Pretty.margin_default| indicates the global default for
    2.21 +  the right margin of the built-in pretty printer, with initial value
    2.22 +  76.  Note that user-interfaces typically control margins
    2.23 +  automatically when resizing windows, or even bypass the formatting
    2.24 +  engine of Isabelle/ML altogether and do it within the front end via
    2.25 +  Isabelle/Scala.
    2.26  
    2.27    \item \verb|print_depth|~\isa{n} limits the printing depth of the
    2.28    ML toplevel pretty printer; the precise effect depends on the ML

     3.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Sat May 08 16:53:53 2010 +0200
     3.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Sat May 08 19:14:13 2010 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4    "gcd m n = (if n=0 then m else gcd n (m mod n))"
     3.5  
     3.6  
     3.7 -ML "Pretty.setmargin 64"
     3.8 +ML "Pretty.margin_default := 64"
     3.9  ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
    3.10  
    3.11  

     4.1 --- a/doc-src/TutorialI/Sets/Examples.thy	Sat May 08 16:53:53 2010 +0200
     4.2 +++ b/doc-src/TutorialI/Sets/Examples.thy	Sat May 08 19:14:13 2010 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4  theory Examples imports Main Binomial begin
     4.5  
     4.6  ML "Unsynchronized.reset eta_contract"
     4.7 -ML "Pretty.setmargin 64"
     4.8 +ML "Pretty.margin_default := 64"
     4.9  
    4.10  text{*membership, intersection *}
    4.11  text{*difference and empty set*}

     5.1 --- a/doc-src/TutorialI/Sets/Functions.thy	Sat May 08 16:53:53 2010 +0200
     5.2 +++ b/doc-src/TutorialI/Sets/Functions.thy	Sat May 08 19:14:13 2010 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  (* ID:         $Id$ *)
     5.5  theory Functions imports Main begin
     5.6  
     5.7 -ML "Pretty.setmargin 64"
     5.8 +ML "Pretty.margin_default := 64"
     5.9  
    5.10  
    5.11  text{*

     6.1 --- a/doc-src/TutorialI/Sets/Recur.thy	Sat May 08 16:53:53 2010 +0200
     6.2 +++ b/doc-src/TutorialI/Sets/Recur.thy	Sat May 08 19:14:13 2010 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (* ID:         $Id$ *)
     6.5  theory Recur imports Main begin
     6.6  
     6.7 -ML "Pretty.setmargin 64"
     6.8 +ML "Pretty.margin_default := 64"
     6.9  
    6.10  
    6.11  text{*

     7.1 --- a/doc-src/TutorialI/Sets/Relations.thy	Sat May 08 16:53:53 2010 +0200
     7.2 +++ b/doc-src/TutorialI/Sets/Relations.thy	Sat May 08 19:14:13 2010 +0200
     7.3 @@ -1,7 +1,7 @@
     7.4  (* ID:         $Id$ *)
     7.5  theory Relations imports Main begin
     7.6  
     7.7 -ML "Pretty.setmargin 64"
     7.8 +ML "Pretty.margin_default := 64"
     7.9  
    7.10  (*Id is only used in UNITY*)
    7.11  (*refl, antisym,trans,univalent,\<dots> ho hum*)

     8.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Sat May 08 16:53:53 2010 +0200
     8.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Sat May 08 19:14:13 2010 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4  imports Complex_Main
     8.5  begin
     8.6  
     8.7 -ML "Pretty.setmargin 64"
     8.8 +ML "Pretty.margin_default := 64"
     8.9  ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)
    8.10  
    8.11  text{*

     9.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Sat May 08 16:53:53 2010 +0200
     9.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Sat May 08 19:14:13 2010 +0200
     9.3 @@ -26,7 +26,7 @@
     9.4  %
     9.5  \isatagML
     9.6  \isacommand{ML}\isamarkupfalse%
     9.7 -\ {\isachardoublequoteopen}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
     9.8 +\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
     9.9  \isacommand{ML}\isamarkupfalse%
    9.10  \ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
    9.11  \endisatagML

    10.1 --- a/doc-src/more_antiquote.ML	Sat May 08 16:53:53 2010 +0200
    10.2 +++ b/doc-src/more_antiquote.ML	Sat May 08 19:14:13 2010 +0200
    10.3 @@ -51,7 +51,7 @@
    10.4  
    10.5  local
    10.6  
    10.7 -val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str;
    10.8 +val pr_text = enclose "\\isa{" "}" o Pretty.output NONE o Pretty.str;
    10.9  
   10.10  fun pr_class ctxt = ProofContext.read_class ctxt
   10.11    #> Type.extern_class (ProofContext.tsig_of ctxt)

    11.1 --- a/src/Pure/General/pretty.ML	Sat May 08 16:53:53 2010 +0200
    11.2 +++ b/src/Pure/General/pretty.ML	Sat May 08 19:14:13 2010 +0200
    11.3 @@ -52,14 +52,14 @@
    11.4    val big_list: string -> T list -> T
    11.5    val indent: int -> T -> T
    11.6    val unbreakable: T -> T
    11.7 -  val setmargin: int -> unit
    11.8 -  val setmp_margin_CRITICAL: int -> ('a -> 'b) -> 'a -> 'b
    11.9 +  val margin_default: int Unsynchronized.ref
   11.10    val setdepth: int -> unit
   11.11    val to_ML: T -> ML_Pretty.pretty
   11.12    val from_ML: ML_Pretty.pretty -> T
   11.13    val symbolicN: string
   11.14 -  val output_buffer: T -> Buffer.T
   11.15 -  val output: T -> output
   11.16 +  val output_buffer: int option -> T -> Buffer.T
   11.17 +  val output: int option -> T -> output
   11.18 +  val string_of_margin: int -> T -> string
   11.19    val string_of: T -> string
   11.20    val str_of: T -> string
   11.21    val writeln: T -> unit
   11.22 @@ -181,14 +181,7 @@
   11.23  
   11.24  (* margin *)
   11.25  
   11.26 -fun make_margin_info m =
   11.27 - {margin = m,                   (*right margin, or page width*)
   11.28 -  breakgain = m div 20,         (*minimum added space required of a break*)
   11.29 -  emergencypos = m div 2};      (*position too far to right*)
   11.30 -
   11.31 -val margin_info = Unsynchronized.ref (make_margin_info 76);
   11.32 -fun setmargin m = margin_info := make_margin_info m;
   11.33 -fun setmp_margin_CRITICAL m f = setmp_CRITICAL margin_info (make_margin_info m) f;
   11.34 +val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
   11.35  
   11.36  
   11.37  (* depth limitation *)
   11.38 @@ -259,42 +252,45 @@
   11.39    | forcenext (Break _ :: es) = fbrk :: es
   11.40    | forcenext (e :: es) = e :: forcenext es;
   11.41  
   11.42 -(*es is list of expressions to print;
   11.43 -  blockin is the indentation of the current block;
   11.44 -  after is the width of the following context until next break.*)
   11.45 -fun format ([], _, _) text = text
   11.46 -  | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
   11.47 -      (case e of
   11.48 -        Block ((bg, en), bes, indent, _) =>
   11.49 -          let
   11.50 -            val {emergencypos, ...} = ! margin_info;
   11.51 -            val pos' = pos + indent;
   11.52 -            val pos'' = pos' mod emergencypos;
   11.53 -            val block' =
   11.54 -              if pos' < emergencypos then (ind |> add_indent indent, pos')
   11.55 -              else (add_indent pos'' Buffer.empty, pos'');
   11.56 -            val btext: text = text
   11.57 -              |> control bg
   11.58 -              |> format (bes, block', breakdist (es, after))
   11.59 -              |> control en;
   11.60 -            (*if this block was broken then force the next break*)
   11.61 -            val es' = if nl < #nl btext then forcenext es else es;
   11.62 -          in format (es', block, after) btext end
   11.63 -      | Break (force, wd) =>
   11.64 -          let val {margin, breakgain, ...} = ! margin_info in
   11.65 -            (*no break if text to next break fits on this line
   11.66 -              or if breaking would add only breakgain to space*)
   11.67 -            format (es, block, after)
   11.68 -              (if not force andalso
   11.69 -                  pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   11.70 -                then text |> blanks wd  (*just insert wd blanks*)
   11.71 -                else text |> newline |> indentation block)
   11.72 -          end
   11.73 -      | String str => format (es, block, after) (string str text));
   11.74 -
   11.75  in
   11.76  
   11.77 -fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
   11.78 +fun formatted margin input =
   11.79 +  let
   11.80 +    val breakgain = margin div 20;     (*minimum added space required of a break*)
   11.81 +    val emergencypos = margin div 2;   (*position too far to right*)
   11.82 +
   11.83 +    (*es is list of expressions to print;
   11.84 +      blockin is the indentation of the current block;
   11.85 +      after is the width of the following context until next break.*)
   11.86 +    fun format ([], _, _) text = text
   11.87 +      | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
   11.88 +          (case e of
   11.89 +            Block ((bg, en), bes, indent, _) =>
   11.90 +              let
   11.91 +                val pos' = pos + indent;
   11.92 +                val pos'' = pos' mod emergencypos;
   11.93 +                val block' =
   11.94 +                  if pos' < emergencypos then (ind |> add_indent indent, pos')
   11.95 +                  else (add_indent pos'' Buffer.empty, pos'');
   11.96 +                val btext: text = text
   11.97 +                  |> control bg
   11.98 +                  |> format (bes, block', breakdist (es, after))
   11.99 +                  |> control en;
  11.100 +                (*if this block was broken then force the next break*)
  11.101 +                val es' = if nl < #nl btext then forcenext es else es;
  11.102 +              in format (es', block, after) btext end
  11.103 +          | Break (force, wd) =>
  11.104 +              (*no break if text to next break fits on this line
  11.105 +                or if breaking would add only breakgain to space*)
  11.106 +              format (es, block, after)
  11.107 +                (if not force andalso
  11.108 +                    pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
  11.109 +                  then text |> blanks wd  (*just insert wd blanks*)
  11.110 +                  else text |> newline |> indentation block)
  11.111 +          | String str => format (es, block, after) (string str text));
  11.112 +  in
  11.113 +    #tx (format ([prune input], (Buffer.empty, 0), 0) empty)
  11.114 +  end;
  11.115  
  11.116  end;
  11.117  
  11.118 @@ -336,12 +332,13 @@
  11.119  
  11.120  val symbolicN = "pretty_symbolic";
  11.121  
  11.122 -fun output_buffer prt =
  11.123 +fun output_buffer margin prt =
  11.124    if print_mode_active symbolicN then symbolic prt
  11.125 -  else formatted prt;
  11.126 +  else formatted (the_default (! margin_default) margin) prt;
  11.127  
  11.128 -val output = Buffer.content o output_buffer;
  11.129 -val string_of = Output.escape o output;
  11.130 +val output = Buffer.content oo output_buffer;
  11.131 +fun string_of_margin margin = Output.escape o output (SOME margin);
  11.132 +val string_of = Output.escape o output NONE;
  11.133  val str_of = Output.escape o Buffer.content o unformatted;
  11.134  val writeln = Output.writeln o string_of;
  11.135  

    12.1 --- a/src/Pure/General/pretty.scala	Sat May 08 16:53:53 2010 +0200
    12.2 +++ b/src/Pure/General/pretty.scala	Sat May 08 19:14:13 2010 +0200
    12.3 @@ -78,9 +78,9 @@
    12.4            Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
    12.5      }
    12.6  
    12.7 -  private val default_margin = 76
    12.8 +  private val margin_default = 76
    12.9  
   12.10 -  def formatted(input: List[XML.Tree], margin: Int = default_margin): List[XML.Tree] =
   12.11 +  def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] =
   12.12    {
   12.13      val breakgain = margin / 20
   12.14      val emergencypos = margin / 2
   12.15 @@ -115,7 +115,7 @@
   12.16      format(input.flatMap(standard_format), 0, 0, Text()).content
   12.17    }
   12.18  
   12.19 -  def string_of(input: List[XML.Tree], margin: Int = default_margin): String =
   12.20 +  def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
   12.21      formatted(input).iterator.flatMap(XML.content).mkString
   12.22  
   12.23  

    13.1 --- a/src/Pure/Isar/class.ML	Sat May 08 16:53:53 2010 +0200
    13.2 +++ b/src/Pure/Isar/class.ML	Sat May 08 19:14:13 2010 +0200
    13.3 @@ -202,7 +202,7 @@
    13.4        |> Expression.cert_declaration supexpr I inferred_elems;
    13.5      fun check_vars e vs = if null vs
    13.6        then error ("No type variable in part of specification element "
    13.7 -        ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
    13.8 +        ^ (Pretty.output NONE o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
    13.9        else ();
   13.10      fun check_element (e as Element.Fixes fxs) =
   13.11            map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs

    14.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat May 08 16:53:53 2010 +0200
    14.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat May 08 19:14:13 2010 +0200
    14.3 @@ -313,7 +313,7 @@
    14.4  
    14.5  (* pretty_setmargin *)
    14.6  
    14.7 -fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
    14.8 +fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
    14.9  
   14.10  
   14.11  (* print parts of theory and proof context *)

    15.1 --- a/src/Pure/Thy/thy_output.ML	Sat May 08 16:53:53 2010 +0200
    15.2 +++ b/src/Pure/Thy/thy_output.ML	Sat May 08 19:14:13 2010 +0200
    15.3 @@ -428,7 +428,7 @@
    15.4    ("break", setmp_CRITICAL break o boolean),
    15.5    ("quotes", setmp_CRITICAL quotes o boolean),
    15.6    ("mode", fn s => fn f => PrintMode.with_modes [s] f),
    15.7 -  ("margin", Pretty.setmp_margin_CRITICAL o integer),
    15.8 +  ("margin", setmp_CRITICAL Pretty.margin_default o integer),
    15.9    ("indent", setmp_CRITICAL indent o integer),
   15.10    ("source", setmp_CRITICAL source o boolean),
   15.11    ("goals_limit", setmp_CRITICAL goals_limit o integer)];

    16.1 --- a/src/Pure/codegen.ML	Sat May 08 16:53:53 2010 +0200
    16.2 +++ b/src/Pure/codegen.ML	Sat May 08 19:14:13 2010 +0200
    16.3 @@ -109,9 +109,7 @@
    16.4  
    16.5  val margin = Unsynchronized.ref 80;
    16.6  
    16.7 -fun string_of p = (Pretty.string_of |>
    16.8 -  PrintMode.setmp [] |>
    16.9 -  Pretty.setmp_margin_CRITICAL (!margin)) p;
   16.10 +fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
   16.11  
   16.12  val str = PrintMode.setmp [] Pretty.str;
   16.13  

    17.1 --- a/src/Tools/Code/code_printer.ML	Sat May 08 16:53:53 2010 +0200
    17.2 +++ b/src/Tools/Code/code_printer.ML	Sat May 08 19:14:13 2010 +0200
    17.3 @@ -116,8 +116,8 @@
    17.4  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    17.5  fun indent i = PrintMode.setmp [] (Pretty.indent i);
    17.6  
    17.7 -fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n";
    17.8 -fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p;
    17.9 +fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
   17.10 +fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
   17.11  
   17.12  
   17.13  (** names and variable name contexts **)

    18.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Sat May 08 16:53:53 2010 +0200
    18.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Sat May 08 19:14:13 2010 +0200
    18.3 @@ -143,7 +143,7 @@
    18.4  fun html_thm ctxt (n, (thmref, thm)) =
    18.5    let
    18.6      val string_of_thm =
    18.7 -      Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
    18.8 +      Output.output o Pretty.string_of_margin 100 o
    18.9          setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
   18.10    in
   18.11      tag' "tr" (class ("row" ^ Int.toString (n mod 2)))