# HG changeset patch
# User wenzelm
# Date 1419263064 -3600
# Node ID bf465f335e8550c69d8ca274ab19f3052a04ab38
# Parent  15a73dd9df51171cdff4397413d055a6783e89a3
system option "pretty_margin" is superseded by "thy_output_margin";

diff -r 15a73dd9df51 -r bf465f335e85 NEWS
--- a/NEWS	Mon Dec 22 15:50:16 2014 +0100
+++ b/NEWS	Mon Dec 22 16:44:24 2014 +0100
@@ -244,6 +244,14 @@
 * Support for Proof General and Isar TTY loop has been discontinued.
 Minor INCOMPATIBILITY.
 
+* System option "pretty_margin" is superseded by "thy_output_margin",
+which is also accessible via document antiquotation option "margin".
+Only the margin for document output may be changed, but not the global
+pretty printing: that is 76 for plain console output, and adapted
+dynamically in GUI front-ends. Implementations of document
+antiquotations need to observe the margin explicitly according to
+Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
+
 * Historical command-line terminator ";" is no longer accepted.  Minor
 INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
 semicolons from theory sources.
diff -r 15a73dd9df51 -r bf465f335e85 etc/options
--- a/etc/options	Mon Dec 22 15:50:16 2014 +0100
+++ b/etc/options	Mon Dec 22 16:44:24 2014 +0100
@@ -20,6 +20,8 @@
   -- "control line breaks in non-display material"
 option thy_output_quotes : bool = false
   -- "indicate if the output should be enclosed in double quotes"
+option thy_output_margin : int = 76
+  -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
@@ -56,9 +58,6 @@
 option eta_contract : bool = true
   -- "print terms in eta-contracted form"
 
-option pretty_margin : int = 76
-  -- "right margin / page width of pretty printer in Isabelle/ML"
-
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"
 
diff -r 15a73dd9df51 -r bf465f335e85 src/Doc/ROOT
--- a/src/Doc/ROOT	Mon Dec 22 15:50:16 2014 +0100
+++ b/src/Doc/ROOT	Mon Dec 22 16:44:24 2014 +0100
@@ -206,7 +206,7 @@
     "root.tex"
 
 session Locales (doc) in "Locales" = HOL +
-  options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
+  options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
   theories
     Examples1
     Examples2
@@ -387,7 +387,7 @@
     "Documents/Documents"
   theories [document = ""]
     "Types/Setup"
-  theories [pretty_margin = 64, thy_output_indent = 0]
+  theories [thy_output_margin = 64, thy_output_indent = 0]
     "Types/Numbers"
     "Types/Pairs"
     "Types/Records"
@@ -397,7 +397,7 @@
     "Rules/Basic"
     "Rules/Blast"
     "Rules/Force"
-  theories [pretty_margin = 64, thy_output_indent = 5]
+  theories [thy_output_margin = 64, thy_output_indent = 5]
     "Rules/TPrimes"
     "Rules/Forward"
     "Rules/Tacticals"
diff -r 15a73dd9df51 -r bf465f335e85 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Mon Dec 22 15:50:16 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Mon Dec 22 16:44:24 2014 +0100
@@ -127,7 +127,9 @@
       #> (if Config.get ctxt Thy_Output.display
           then
             map (fn (p, name) =>
-              Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
+              Output.output
+                (Thy_Output.string_of_margin ctxt
+                  (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
               "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
             #> space_implode "\\par\\smallskip%\n"
             #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
diff -r 15a73dd9df51 -r bf465f335e85 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Dec 22 15:50:16 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Dec 22 16:44:24 2014 +0100
@@ -8,6 +8,7 @@
 sig
   val display: bool Config.T
   val quotes: bool Config.T
+  val margin: int Config.T
   val indent: int Config.T
   val source: bool Config.T
   val break: bool Config.T
@@ -31,6 +32,7 @@
   val str_of_source: Token.src -> string
   val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
     Token.src -> 'a list -> Pretty.T list
+  val string_of_margin: Proof.context -> Pretty.T -> string
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
   val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
@@ -46,6 +48,7 @@
 val display = Attrib.setup_option_bool ("thy_output_display", @{here});
 val break = Attrib.setup_option_bool ("thy_output_break", @{here});
 val quotes = Attrib.setup_option_bool ("thy_output_quotes", @{here});
+val margin = Attrib.setup_option_int ("thy_output_margin", @{here});
 val indent = Attrib.setup_option_int ("thy_output_indent", @{here});
 val source = Attrib.setup_option_bool ("thy_output_source", @{here});
 val modes = Attrib.setup_option_string ("thy_output_modes", @{here});
@@ -108,9 +111,8 @@
     val option_names = map #1 (Name_Space.markup_table ctxt options);
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
-      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
-    |> Pretty.writeln_chunks
-  end;
+     Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
+  end |> Pretty.writeln_chunks;
 
 fun antiquotation name scan body =
   add_command name
@@ -471,7 +473,7 @@
   add_option @{binding break} (Config.put break o boolean) #>
   add_option @{binding quotes} (Config.put quotes o boolean) #>
   add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
-  add_option @{binding margin} (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+  add_option @{binding margin} (Config.put margin o integer) #>
   add_option @{binding indent} (Config.put indent o integer) #>
   add_option @{binding source} (Config.put source o boolean) #>
   add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
@@ -551,15 +553,18 @@
   map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
   |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
 
+fun string_of_margin ctxt = Pretty.string_of_margin (Config.get ctxt margin);
+
 fun output ctxt prts =
   prts
   |> Config.get ctxt quotes ? map Pretty.quote
   |> (if Config.get ctxt display then
-        map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
+        map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
         #> space_implode "\\isasep\\isanewline%\n"
         #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
       else
-        map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
+        map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
+          Output.output)
         #> space_implode "\\isasep\\isanewline%\n"
         #> enclose "\\isa{" "}");
 
@@ -571,11 +576,12 @@
 
 local
 
-fun basic_entities name scan pretty = antiquotation name scan
-  (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
+fun basic_entities name scan pretty =
+  antiquotation name scan (fn {source, context, ...} =>
+    output context o maybe_pretty_source pretty context source);
 
-fun basic_entities_style name scan pretty = antiquotation name scan
-  (fn {source, context, ...} => fn (style, xs) =>
+fun basic_entities_style name scan pretty =
+  antiquotation name scan (fn {source, context, ...} => fn (style, xs) =>
     output context
       (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
 
@@ -612,9 +618,10 @@
   | _ => error "No proof state");
 
 fun goal_state name main = antiquotation name (Scan.succeed ())
-  (fn {state, context = ctxt, ...} => fn () => output ctxt
-    [Goal_Display.pretty_goal
-      (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
+  (fn {state, context = ctxt, ...} => fn () =>
+    output ctxt
+      [Goal_Display.pretty_goal
+        (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
 
 in
 
diff -r 15a73dd9df51 -r bf465f335e85 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Dec 22 15:50:16 2014 +0100
+++ b/src/Pure/Tools/build.ML	Mon Dec 22 16:44:24 2014 +0100
@@ -109,8 +109,7 @@
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Multithreading.max_threads_setmp (Options.int options "threads")
-    |> Unsynchronized.setmp Future.ML_statistics true
-    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin");
+    |> Unsynchronized.setmp Future.ML_statistics true;
 
 fun use_theories_condition last_timing (options, thys) =
   let val condition = space_explode "," (Options.string options "condition") in