unified/simplified Pretty.margin_default;
discontinued special Pretty.setmargin etc;
explicit margin argument for Pretty.string_of_margin etc.;

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 16:53:53 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 19:14:13 2010 +0200
@@ -213,7 +213,7 @@
 text {*
   \begin{mldecls}
     @{index_ML Pretty.setdepth: "int -> unit"} \\
-    @{index_ML Pretty.setmargin: "int -> unit"} \\
+    @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
     @{index_ML print_depth: "int -> unit"} \\
   \end{mldecls}
 
@@ -227,10 +227,12 @@
   printing to an arbitrary depth.  Other useful values for @{text d}
   are 10 and 20.
 
-  \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
-  assume a right margin (page width) of @{text m}.  The initial margin
-  is 76, but user interfaces might adapt the margin automatically when
-  resizing windows.
+  \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
+  automatically when resizing windows, or even bypass the formatting
+  engine of Isabelle/ML altogether and do it within the front end via
+  Isabelle/Scala.
 
   \item @{ML print_depth}~@{text n} limits the printing depth of the
   ML toplevel pretty printer; the precise effect depends on the ML

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 16:53:53 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 19:14:13 2010 +0200
@@ -232,7 +232,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
     \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
-    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: 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}
 
@@ -246,10 +246,12 @@
   printing to an arbitrary depth.  Other useful values for \isa{d}
   are 10 and 20.
 
-  \item \verb|Pretty.setmargin|~\isa{m} tells the pretty printer to
-  assume a right margin (page width) of \isa{m}.  The initial margin
-  is 76, but user interfaces might adapt the margin automatically when
-  resizing windows.
+  \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
+  automatically when resizing windows, or even bypass the formatting
+  engine of Isabelle/ML altogether and do it within the front end via
+  Isabelle/Scala.
 
   \item \verb|print_depth|~\isa{n} limits the printing depth of the
   ML toplevel pretty printer; the precise effect depends on the ML

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

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

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

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

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

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

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

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

--- a/src/Pure/General/pretty.ML	Sat May 08 16:53:53 2010 +0200
+++ b/src/Pure/General/pretty.ML	Sat May 08 19:14:13 2010 +0200
@@ -52,14 +52,14 @@
   val big_list: string -> T list -> T
   val indent: int -> T -> T
   val unbreakable: T -> T
-  val setmargin: int -> unit
-  val setmp_margin_CRITICAL: int -> ('a -> 'b) -> 'a -> 'b
+  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
-  val output_buffer: T -> Buffer.T
-  val output: T -> output
+  val output_buffer: int option -> T -> Buffer.T
+  val output: int option -> T -> output
+  val string_of_margin: int -> T -> string
   val string_of: T -> string
   val str_of: T -> string
   val writeln: T -> unit
@@ -181,14 +181,7 @@
 
 (* margin *)
 
-fun make_margin_info m =
- {margin = m,                   (*right margin, or page width*)
-  breakgain = m div 20,         (*minimum added space required of a break*)
-  emergencypos = m div 2};      (*position too far to right*)
-
-val margin_info = Unsynchronized.ref (make_margin_info 76);
-fun setmargin m = margin_info := make_margin_info m;
-fun setmp_margin_CRITICAL m f = setmp_CRITICAL margin_info (make_margin_info m) f;
+val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
 
 
 (* depth limitation *)
@@ -259,42 +252,45 @@
   | forcenext (Break _ :: es) = fbrk :: es
   | forcenext (e :: es) = e :: forcenext es;
 
-(*es is list of expressions to print;
-  blockin is the indentation of the current block;
-  after is the width of the following context until next break.*)
-fun format ([], _, _) text = text
-  | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
-      (case e of
-        Block ((bg, en), bes, indent, _) =>
-          let
-            val {emergencypos, ...} = ! margin_info;
-            val pos' = pos + indent;
-            val pos'' = pos' mod emergencypos;
-            val block' =
-              if pos' < emergencypos then (ind |> add_indent indent, pos')
-              else (add_indent pos'' Buffer.empty, pos'');
-            val btext: text = text
-              |> control bg
-              |> format (bes, block', breakdist (es, after))
-              |> control en;
-            (*if this block was broken then force the next break*)
-            val es' = if nl < #nl btext then forcenext es else es;
-          in format (es', block, after) btext end
-      | Break (force, wd) =>
-          let val {margin, breakgain, ...} = ! margin_info in
-            (*no break if text to next break fits on this line
-              or if breaking would add only breakgain to space*)
-            format (es, block, after)
-              (if not force andalso
-                  pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
-                then text |> blanks wd  (*just insert wd blanks*)
-                else text |> newline |> indentation block)
-          end
-      | String str => format (es, block, after) (string str text));
-
 in
 
-fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
+fun formatted margin input =
+  let
+    val breakgain = margin div 20;     (*minimum added space required of a break*)
+    val emergencypos = margin div 2;   (*position too far to right*)
+
+    (*es is list of expressions to print;
+      blockin is the indentation of the current block;
+      after is the width of the following context until next break.*)
+    fun format ([], _, _) text = text
+      | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
+          (case e of
+            Block ((bg, en), bes, indent, _) =>
+              let
+                val pos' = pos + indent;
+                val pos'' = pos' mod emergencypos;
+                val block' =
+                  if pos' < emergencypos then (ind |> add_indent indent, pos')
+                  else (add_indent pos'' Buffer.empty, pos'');
+                val btext: text = text
+                  |> control bg
+                  |> format (bes, block', breakdist (es, after))
+                  |> control en;
+                (*if this block was broken then force the next break*)
+                val es' = if nl < #nl btext then forcenext es else es;
+              in format (es', block, after) btext end
+          | Break (force, wd) =>
+              (*no break if text to next break fits on this line
+                or if breaking would add only breakgain to space*)
+              format (es, block, after)
+                (if not force andalso
+                    pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
+                  then text |> blanks wd  (*just insert wd blanks*)
+                  else text |> newline |> indentation block)
+          | String str => format (es, block, after) (string str text));
+  in
+    #tx (format ([prune input], (Buffer.empty, 0), 0) empty)
+  end;
 
 end;
 
@@ -336,12 +332,13 @@
 
 val symbolicN = "pretty_symbolic";
 
-fun output_buffer prt =
+fun output_buffer margin prt =
   if print_mode_active symbolicN then symbolic prt
-  else formatted prt;
+  else formatted (the_default (! margin_default) margin) prt;
 
-val output = Buffer.content o output_buffer;
-val string_of = Output.escape o output;
+val output = Buffer.content oo output_buffer;
+fun string_of_margin margin = Output.escape o output (SOME margin);
+val string_of = Output.escape o output NONE;
 val str_of = Output.escape o Buffer.content o unformatted;
 val writeln = Output.writeln o string_of;
 

--- a/src/Pure/General/pretty.scala	Sat May 08 16:53:53 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sat May 08 19:14:13 2010 +0200
@@ -78,9 +78,9 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  private val default_margin = 76
+  private val margin_default = 76
 
-  def formatted(input: List[XML.Tree], margin: Int = default_margin): List[XML.Tree] =
+  def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] =
   {
     val breakgain = margin / 20
     val emergencypos = margin / 2
@@ -115,7 +115,7 @@
     format(input.flatMap(standard_format), 0, 0, Text()).content
   }
 
-  def string_of(input: List[XML.Tree], margin: Int = default_margin): String =
+  def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
     formatted(input).iterator.flatMap(XML.content).mkString
 
 

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

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

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

--- a/src/Pure/codegen.ML	Sat May 08 16:53:53 2010 +0200
+++ b/src/Pure/codegen.ML	Sat May 08 19:14:13 2010 +0200
@@ -109,9 +109,7 @@
 
 val margin = Unsynchronized.ref 80;
 
-fun string_of p = (Pretty.string_of |>
-  PrintMode.setmp [] |>
-  Pretty.setmp_margin_CRITICAL (!margin)) p;
+fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
 
 val str = PrintMode.setmp [] Pretty.str;
 

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

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