src/Pure/Thy/thy_output.ML
changeset 38767 d8da44a8dd25
parent 38766 8891f4520d16
child 38832 fc0aa40a1b08
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 27 00:09:56 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 27 12:40:20 2010 +0200
     1.3 @@ -6,11 +6,16 @@
     1.4  
     1.5  signature THY_OUTPUT =
     1.6  sig
     1.7 -  val display: bool Unsynchronized.ref
     1.8 -  val quotes: bool Unsynchronized.ref
     1.9 -  val indent: int Unsynchronized.ref
    1.10 -  val source: bool Unsynchronized.ref
    1.11 -  val break: bool Unsynchronized.ref
    1.12 +  val display_default: bool Unsynchronized.ref
    1.13 +  val quotes_default: bool Unsynchronized.ref
    1.14 +  val indent_default: int Unsynchronized.ref
    1.15 +  val source_default: bool Unsynchronized.ref
    1.16 +  val break_default: bool Unsynchronized.ref
    1.17 +  val display: bool Config.T
    1.18 +  val quotes: bool Config.T
    1.19 +  val indent: int Config.T
    1.20 +  val source: bool Config.T
    1.21 +  val break: bool Config.T
    1.22    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
    1.23    val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
    1.24    val defined_command: string -> bool
    1.25 @@ -25,12 +30,13 @@
    1.26    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    1.27    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    1.28      (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
    1.29 -  val pretty_text: string -> Pretty.T
    1.30 +  val pretty_text: Proof.context -> string -> Pretty.T
    1.31    val pretty_term: Proof.context -> term -> Pretty.T
    1.32    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.33    val str_of_source: Args.src -> string
    1.34 -  val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
    1.35 -  val output: Pretty.T list -> string
    1.36 +  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
    1.37 +    Args.src -> 'a list -> Pretty.T list
    1.38 +  val output: Proof.context -> Pretty.T list -> string
    1.39  end;
    1.40  
    1.41  structure Thy_Output: THY_OUTPUT =
    1.42 @@ -38,11 +44,20 @@
    1.43  
    1.44  (** global options **)
    1.45  
    1.46 -val display = Unsynchronized.ref false;
    1.47 -val quotes = Unsynchronized.ref false;
    1.48 -val indent = Unsynchronized.ref 0;
    1.49 -val source = Unsynchronized.ref false;
    1.50 -val break = Unsynchronized.ref false;
    1.51 +val display_default = Unsynchronized.ref false;
    1.52 +val quotes_default = Unsynchronized.ref false;
    1.53 +val indent_default = Unsynchronized.ref 0;
    1.54 +val source_default = Unsynchronized.ref false;
    1.55 +val break_default = Unsynchronized.ref false;
    1.56 +
    1.57 +val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
    1.58 +val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
    1.59 +val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
    1.60 +val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
    1.61 +val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
    1.62 +
    1.63 +val _ = Context.>> (Context.map_theory
    1.64 + (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
    1.65  
    1.66  
    1.67  structure Wrappers = Proof_Data
    1.68 @@ -438,22 +453,23 @@
    1.69  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
    1.70  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
    1.71  val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
    1.72 -val _ = add_option "display" (add_wrapper o setmp_CRITICAL display o boolean);
    1.73 -val _ = add_option "break" (add_wrapper o setmp_CRITICAL break o boolean);
    1.74 -val _ = add_option "quotes" (add_wrapper o setmp_CRITICAL quotes o boolean);
    1.75 +val _ = add_option "display" (Config.put display o boolean);
    1.76 +val _ = add_option "break" (Config.put break o boolean);
    1.77 +val _ = add_option "quotes" (Config.put quotes o boolean);
    1.78  val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
    1.79  val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
    1.80 -val _ = add_option "indent" (add_wrapper o setmp_CRITICAL indent o integer);
    1.81 -val _ = add_option "source" (add_wrapper o setmp_CRITICAL source o boolean);
    1.82 +val _ = add_option "indent" (Config.put indent o integer);
    1.83 +val _ = add_option "source" (Config.put source o boolean);
    1.84  val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
    1.85  
    1.86  
    1.87  (* basic pretty printing *)
    1.88  
    1.89 -fun tweak_line s =
    1.90 -  if ! display then s else Symbol.strip_blanks s;
    1.91 +fun tweak_line ctxt s =
    1.92 +  if Config.get ctxt display then s else Symbol.strip_blanks s;
    1.93  
    1.94 -val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
    1.95 +fun pretty_text ctxt =
    1.96 +  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o Library.split_lines;
    1.97  
    1.98  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    1.99  
   1.100 @@ -502,19 +518,19 @@
   1.101  
   1.102  val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
   1.103  
   1.104 -fun maybe_pretty_source pretty src xs =
   1.105 -  map pretty xs  (*always pretty in order to exhibit errors!*)
   1.106 -  |> (if ! source then K [pretty_text (str_of_source src)] else I);
   1.107 +fun maybe_pretty_source pretty ctxt src xs =
   1.108 +  map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
   1.109 +  |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
   1.110  
   1.111 -fun output prts =
   1.112 +fun output ctxt prts =
   1.113    prts
   1.114 -  |> (if ! quotes then map Pretty.quote else I)
   1.115 -  |> (if ! display then
   1.116 -    map (Output.output o Pretty.string_of o Pretty.indent (! indent))
   1.117 +  |> (if Config.get ctxt quotes then map Pretty.quote else I)
   1.118 +  |> (if Config.get ctxt display then
   1.119 +    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
   1.120      #> space_implode "\\isasep\\isanewline%\n"
   1.121      #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   1.122    else
   1.123 -    map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of))
   1.124 +    map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
   1.125      #> space_implode "\\isasep\\isanewline%\n"
   1.126      #> enclose "\\isa{" "}");
   1.127  
   1.128 @@ -527,11 +543,12 @@
   1.129  local
   1.130  
   1.131  fun basic_entities name scan pretty = antiquotation name scan
   1.132 -  (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
   1.133 +  (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
   1.134  
   1.135  fun basic_entities_style name scan pretty = antiquotation name scan
   1.136    (fn {source, context, ...} => fn (style, xs) =>
   1.137 -    output (maybe_pretty_source (fn x => pretty context (style, x)) source xs));
   1.138 +    output context
   1.139 +      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
   1.140  
   1.141  fun basic_entity name scan = basic_entities name (scan >> single);
   1.142  
   1.143 @@ -545,7 +562,7 @@
   1.144  val _ = basic_entity "const" (Args.const_proper false) pretty_const;
   1.145  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
   1.146  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
   1.147 -val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
   1.148 +val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
   1.149  val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
   1.150  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
   1.151  val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
   1.152 @@ -566,7 +583,7 @@
   1.153    | _ => error "No proof state");
   1.154  
   1.155  fun goal_state name main_goal = antiquotation name (Scan.succeed ())
   1.156 -  (fn {state, ...} => fn () => output
   1.157 +  (fn {state, context, ...} => fn () => output context
   1.158      [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
   1.159  
   1.160  in
   1.161 @@ -590,7 +607,7 @@
   1.162        val _ = context
   1.163          |> Proof.theorem NONE (K I) [[(prop, [])]]
   1.164          |> Proof.global_terminal_proof methods;
   1.165 -    in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
   1.166 +    in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
   1.167  
   1.168  
   1.169  (* ML text *)
   1.170 @@ -601,8 +618,8 @@
   1.171    (fn {context, ...} => fn (txt, pos) =>
   1.172     (ML_Context.eval_in (SOME context) false pos (ml pos txt);
   1.173      Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
   1.174 -    |> (if ! quotes then quote else I)
   1.175 -    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   1.176 +    |> (if Config.get context quotes then quote else I)
   1.177 +    |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   1.178      else
   1.179        split_lines
   1.180        #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")