system option "pretty_margin" is superseded by "thy_output_margin";
authorwenzelm
Mon Dec 22 16:44:24 2014 +0100 (2014-12-22)
changeset 59175bf465f335e85
parent 59174 15a73dd9df51
child 59176 8cf1bad1c2e7
system option "pretty_margin" is superseded by "thy_output_margin";
NEWS
etc/options
src/Doc/ROOT
src/Doc/antiquote_setup.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/build.ML
     1.1 --- a/NEWS	Mon Dec 22 15:50:16 2014 +0100
     1.2 +++ b/NEWS	Mon Dec 22 16:44:24 2014 +0100
     1.3 @@ -244,6 +244,14 @@
     1.4  * Support for Proof General and Isar TTY loop has been discontinued.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* System option "pretty_margin" is superseded by "thy_output_margin",
     1.8 +which is also accessible via document antiquotation option "margin".
     1.9 +Only the margin for document output may be changed, but not the global
    1.10 +pretty printing: that is 76 for plain console output, and adapted
    1.11 +dynamically in GUI front-ends. Implementations of document
    1.12 +antiquotations need to observe the margin explicitly according to
    1.13 +Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
    1.14 +
    1.15  * Historical command-line terminator ";" is no longer accepted.  Minor
    1.16  INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
    1.17  semicolons from theory sources.
     2.1 --- a/etc/options	Mon Dec 22 15:50:16 2014 +0100
     2.2 +++ b/etc/options	Mon Dec 22 16:44:24 2014 +0100
     2.3 @@ -20,6 +20,8 @@
     2.4    -- "control line breaks in non-display material"
     2.5  option thy_output_quotes : bool = false
     2.6    -- "indicate if the output should be enclosed in double quotes"
     2.7 +option thy_output_margin : int = 76
     2.8 +  -- "right margin / page width for printing of display material"
     2.9  option thy_output_indent : int = 0
    2.10    -- "indentation for pretty printing of display material"
    2.11  option thy_output_source : bool = false
    2.12 @@ -56,9 +58,6 @@
    2.13  option eta_contract : bool = true
    2.14    -- "print terms in eta-contracted form"
    2.15  
    2.16 -option pretty_margin : int = 76
    2.17 -  -- "right margin / page width of pretty printer in Isabelle/ML"
    2.18 -
    2.19  option print_mode : string = ""
    2.20    -- "additional print modes for prover output (separated by commas)"
    2.21  
     3.1 --- a/src/Doc/ROOT	Mon Dec 22 15:50:16 2014 +0100
     3.2 +++ b/src/Doc/ROOT	Mon Dec 22 16:44:24 2014 +0100
     3.3 @@ -206,7 +206,7 @@
     3.4      "root.tex"
     3.5  
     3.6  session Locales (doc) in "Locales" = HOL +
     3.7 -  options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
     3.8 +  options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
     3.9    theories
    3.10      Examples1
    3.11      Examples2
    3.12 @@ -387,7 +387,7 @@
    3.13      "Documents/Documents"
    3.14    theories [document = ""]
    3.15      "Types/Setup"
    3.16 -  theories [pretty_margin = 64, thy_output_indent = 0]
    3.17 +  theories [thy_output_margin = 64, thy_output_indent = 0]
    3.18      "Types/Numbers"
    3.19      "Types/Pairs"
    3.20      "Types/Records"
    3.21 @@ -397,7 +397,7 @@
    3.22      "Rules/Basic"
    3.23      "Rules/Blast"
    3.24      "Rules/Force"
    3.25 -  theories [pretty_margin = 64, thy_output_indent = 5]
    3.26 +  theories [thy_output_margin = 64, thy_output_indent = 5]
    3.27      "Rules/TPrimes"
    3.28      "Rules/Forward"
    3.29      "Rules/Tacticals"
     4.1 --- a/src/Doc/antiquote_setup.ML	Mon Dec 22 15:50:16 2014 +0100
     4.2 +++ b/src/Doc/antiquote_setup.ML	Mon Dec 22 16:44:24 2014 +0100
     4.3 @@ -127,7 +127,9 @@
     4.4        #> (if Config.get ctxt Thy_Output.display
     4.5            then
     4.6              map (fn (p, name) =>
     4.7 -              Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
     4.8 +              Output.output
     4.9 +                (Thy_Output.string_of_margin ctxt
    4.10 +                  (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
    4.11                "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    4.12              #> space_implode "\\par\\smallskip%\n"
    4.13              #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
     5.1 --- a/src/Pure/Thy/thy_output.ML	Mon Dec 22 15:50:16 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Dec 22 16:44:24 2014 +0100
     5.3 @@ -8,6 +8,7 @@
     5.4  sig
     5.5    val display: bool Config.T
     5.6    val quotes: bool Config.T
     5.7 +  val margin: int Config.T
     5.8    val indent: int Config.T
     5.9    val source: bool Config.T
    5.10    val break: bool Config.T
    5.11 @@ -31,6 +32,7 @@
    5.12    val str_of_source: Token.src -> string
    5.13    val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
    5.14      Token.src -> 'a list -> Pretty.T list
    5.15 +  val string_of_margin: Proof.context -> Pretty.T -> string
    5.16    val output: Proof.context -> Pretty.T list -> string
    5.17    val verbatim_text: Proof.context -> string -> string
    5.18    val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
    5.19 @@ -46,6 +48,7 @@
    5.20  val display = Attrib.setup_option_bool ("thy_output_display", @{here});
    5.21  val break = Attrib.setup_option_bool ("thy_output_break", @{here});
    5.22  val quotes = Attrib.setup_option_bool ("thy_output_quotes", @{here});
    5.23 +val margin = Attrib.setup_option_int ("thy_output_margin", @{here});
    5.24  val indent = Attrib.setup_option_int ("thy_output_indent", @{here});
    5.25  val source = Attrib.setup_option_bool ("thy_output_source", @{here});
    5.26  val modes = Attrib.setup_option_string ("thy_output_modes", @{here});
    5.27 @@ -108,9 +111,8 @@
    5.28      val option_names = map #1 (Name_Space.markup_table ctxt options);
    5.29    in
    5.30      [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
    5.31 -      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
    5.32 -    |> Pretty.writeln_chunks
    5.33 -  end;
    5.34 +     Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
    5.35 +  end |> Pretty.writeln_chunks;
    5.36  
    5.37  fun antiquotation name scan body =
    5.38    add_command name
    5.39 @@ -471,7 +473,7 @@
    5.40    add_option @{binding break} (Config.put break o boolean) #>
    5.41    add_option @{binding quotes} (Config.put quotes o boolean) #>
    5.42    add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
    5.43 -  add_option @{binding margin} (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
    5.44 +  add_option @{binding margin} (Config.put margin o integer) #>
    5.45    add_option @{binding indent} (Config.put indent o integer) #>
    5.46    add_option @{binding source} (Config.put source o boolean) #>
    5.47    add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
    5.48 @@ -551,15 +553,18 @@
    5.49    map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
    5.50    |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
    5.51  
    5.52 +fun string_of_margin ctxt = Pretty.string_of_margin (Config.get ctxt margin);
    5.53 +
    5.54  fun output ctxt prts =
    5.55    prts
    5.56    |> Config.get ctxt quotes ? map Pretty.quote
    5.57    |> (if Config.get ctxt display then
    5.58 -        map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
    5.59 +        map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
    5.60          #> space_implode "\\isasep\\isanewline%\n"
    5.61          #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    5.62        else
    5.63 -        map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
    5.64 +        map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
    5.65 +          Output.output)
    5.66          #> space_implode "\\isasep\\isanewline%\n"
    5.67          #> enclose "\\isa{" "}");
    5.68  
    5.69 @@ -571,11 +576,12 @@
    5.70  
    5.71  local
    5.72  
    5.73 -fun basic_entities name scan pretty = antiquotation name scan
    5.74 -  (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
    5.75 +fun basic_entities name scan pretty =
    5.76 +  antiquotation name scan (fn {source, context, ...} =>
    5.77 +    output context o maybe_pretty_source pretty context source);
    5.78  
    5.79 -fun basic_entities_style name scan pretty = antiquotation name scan
    5.80 -  (fn {source, context, ...} => fn (style, xs) =>
    5.81 +fun basic_entities_style name scan pretty =
    5.82 +  antiquotation name scan (fn {source, context, ...} => fn (style, xs) =>
    5.83      output context
    5.84        (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
    5.85  
    5.86 @@ -612,9 +618,10 @@
    5.87    | _ => error "No proof state");
    5.88  
    5.89  fun goal_state name main = antiquotation name (Scan.succeed ())
    5.90 -  (fn {state, context = ctxt, ...} => fn () => output ctxt
    5.91 -    [Goal_Display.pretty_goal
    5.92 -      (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
    5.93 +  (fn {state, context = ctxt, ...} => fn () =>
    5.94 +    output ctxt
    5.95 +      [Goal_Display.pretty_goal
    5.96 +        (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
    5.97  
    5.98  in
    5.99  
     6.1 --- a/src/Pure/Tools/build.ML	Mon Dec 22 15:50:16 2014 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Mon Dec 22 16:44:24 2014 +0100
     6.3 @@ -109,8 +109,7 @@
     6.4      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     6.5      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     6.6      |> Multithreading.max_threads_setmp (Options.int options "threads")
     6.7 -    |> Unsynchronized.setmp Future.ML_statistics true
     6.8 -    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin");
     6.9 +    |> Unsynchronized.setmp Future.ML_statistics true;
    6.10  
    6.11  fun use_theories_condition last_timing (options, thys) =
    6.12    let val condition = space_explode "," (Options.string options "condition") in