--- 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.
--- 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)"
--- 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"
--- 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}"
--- 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
--- 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