proper context for various Thy_Output options, via official configuration options in ML and Isar;

--- a/NEWS	Fri Aug 27 00:09:56 2010 +0200
+++ b/NEWS	Fri Aug 27 12:40:20 2010 +0200
@@ -23,6 +23,22 @@
 at the cost of clarity of file dependencies.  Recall that Isabelle/ML
 files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
 
+* Various options that affect document antiquotations are now properly
+handled within the context via configuration options, instead of
+unsynchronized references.  There are both ML Config.T entities and
+Isar declaration attributes to access these.
+
+  ML:                       Isar:
+
+  Thy_Output.display        thy_output_display
+  Thy_Output.quotes         thy_output_quotes
+  Thy_Output.indent         thy_output_indent
+  Thy_Output.source         thy_output_source
+  Thy_Output.break          thy_output_break
+
+Note that the corresponding "..._default" references may be only
+changed globally at the ROOT session setup, but *not* within a theory.
+
 
 *** Pure ***
 

--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set Thy_Output.source;
+Thy_Output.source_default := true;
 use "../../antiquote_setup.ML";
 
 use_thy "HOLCF_Specific";

--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set Thy_Output.source;
+Thy_Output.source_default := true;
 use "../../antiquote_setup.ML";
 
 use_thy "ZF_Specific";

--- a/doc-src/IsarRef/Thy/ROOT.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -1,5 +1,5 @@
-Unsynchronized.set quick_and_dirty;
-Unsynchronized.set Thy_Output.source;
+quick_and_dirty := true;
+Thy_Output.source_default := true;
 use "../../antiquote_setup.ML";
 
 use_thys [

--- a/doc-src/Main/Docs/Main_Doc.thy	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Fri Aug 27 12:40:20 2010 +0200
@@ -10,9 +10,9 @@
    Syntax.pretty_typ ctxt T)
 
 val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
-  (fn {source, context, ...} => fn arg =>
-    Thy_Output.output
-      (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
+  (fn {source, context = ctxt, ...} => fn arg =>
+    Thy_Output.output ctxt
+      (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]));
 *}
 (*>*)
 text{*

--- a/doc-src/System/Thy/ROOT.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/System/Thy/ROOT.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -1,4 +1,4 @@
-Unsynchronized.set Thy_Output.source;
+Thy_Output.source_default := true;
 use "../../antiquote_setup.ML";
 
 use_thys ["Basics", "Interfaces", "Presentation", "Misc"];

--- a/doc-src/TutorialI/Rules/Primes.thy	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Aug 27 12:40:20 2010 +0200
@@ -1,4 +1,3 @@
-(* ID:         $Id$ *)
 (* EXTRACT from HOL/ex/Primes.thy*)
 
 (*Euclid's algorithm 
@@ -10,7 +9,7 @@
 
 
 ML "Pretty.margin_default := 64"
-ML "Thy_Output.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
+declare [[thy_output_indent = 5]]  (*that is, Doc/TutorialI/settings.ML*)
 
 
 text {*Now in Basic.thy!

--- a/doc-src/TutorialI/Types/Numbers.thy	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Fri Aug 27 12:40:20 2010 +0200
@@ -3,7 +3,7 @@
 begin
 
 ML "Pretty.margin_default := 64"
-ML "Thy_Output.indent := 0"  (*we don't want 5 for listing theorems*)
+declare [[thy_output_indent = 0]]  (*we don't want 5 for listing theorems*)
 
 text{*
 

--- a/doc-src/TutorialI/Types/document/Numbers.tex	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Fri Aug 27 12:40:20 2010 +0200
@@ -26,16 +26,16 @@
 %
 \isatagML
 \isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}%
 \endisatagML
 {\isafoldML}%
 %
 \isadelimML
+\isanewline
 %
 \endisadelimML
-%
+\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}thy{\isacharunderscore}output{\isacharunderscore}indent\ {\isacharequal}\ {\isadigit{0}}{\isacharbrackright}{\isacharbrackright}%
 \begin{isamarkuptext}%
 numeric literals; default simprules; can re-orient%
 \end{isamarkuptext}%

--- a/doc-src/TutorialI/settings.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/TutorialI/settings.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -1,3 +1,1 @@
-(* $Id$ *)
-
-Thy_Output.indent := 5;
+Thy_Output.indent_default := 5;

--- a/doc-src/antiquote_setup.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/antiquote_setup.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -71,8 +71,8 @@
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
       (txt'
-      |> (if ! Thy_Output.quotes then quote else I)
-      |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+      |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+      |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
           else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
     end);
 
@@ -93,18 +93,18 @@
   (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   (fn {context = ctxt, ...} =>
     map (apfst (Thy_Output.pretty_thm ctxt))
-    #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
-    #> (if ! Thy_Output.display
+    #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
+    #> (if Config.get ctxt Thy_Output.display
         then
           map (fn (p, name) =>
-            Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
-            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
+            Output.output (Pretty.string_of (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}"
         else
           map (fn (p, name) =>
             Output.output (Pretty.str_of p) ^
-            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
+            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
           #> space_implode "\\par\\smallskip%\n"
           #> enclose "\\isa{" "}"));
 
@@ -112,7 +112,8 @@
 (* theory file *)
 
 val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
-  (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
+  (fn {context = ctxt, ...} =>
+    fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
 
 
 (* Isabelle/Isar entities (with index) *)
@@ -152,8 +153,9 @@
           idx ^
           (Output.output name
             |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
-            |> (if ! Thy_Output.quotes then quote else I)
-            |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+            |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+            |> (if Config.get ctxt Thy_Output.display
+                then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
                 else hyper o enclose "\\mbox{\\isa{" "}}"))
         else error ("Bad " ^ kind ^ " " ^ quote name)
       end);

--- a/doc-src/more_antiquote.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/more_antiquote.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -95,7 +95,7 @@
       |> snd
       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
       |> map (holize o no_vars ctxt o AxClass.overload thy);
-  in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end;
+  in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
 
 in
 

--- a/doc-src/rail.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/doc-src/rail.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -97,8 +97,9 @@
     (idx ^
     (Output.output name
       |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
-      |> (if ! Thy_Output.quotes then quote else I)
-      |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+      |> (if Config.get ctxt Thy_Output.quotes then quote else I)
+      |> (if Config.get ctxt Thy_Output.display
+          then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
           else hyper o enclose "\\mbox{\\isa{" "}}")), style)
   else ("Bad " ^ kind ^ " " ^ name, false)
   end;

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -257,7 +257,9 @@
            Pretty.str " =" :: Pretty.brk 1 ::
            flat (separate [Pretty.brk 1, Pretty.str "| "]
              (map (single o pretty_constr) cos)));
-    in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end);
+    in
+      Thy_Output.output ctxt (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
+    end);
 
 
 

--- a/src/Pure/Thy/thy_output.ML	Fri Aug 27 00:09:56 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Aug 27 12:40:20 2010 +0200
@@ -6,11 +6,16 @@
 
 signature THY_OUTPUT =
 sig
-  val display: bool Unsynchronized.ref
-  val quotes: bool Unsynchronized.ref
-  val indent: int Unsynchronized.ref
-  val source: bool Unsynchronized.ref
-  val break: bool Unsynchronized.ref
+  val display_default: bool Unsynchronized.ref
+  val quotes_default: bool Unsynchronized.ref
+  val indent_default: int Unsynchronized.ref
+  val source_default: bool Unsynchronized.ref
+  val break_default: bool Unsynchronized.ref
+  val display: bool Config.T
+  val quotes: bool Config.T
+  val indent: int Config.T
+  val source: bool Config.T
+  val break: bool Config.T
   val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
   val defined_command: string -> bool
@@ -25,12 +30,13 @@
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
-  val pretty_text: string -> Pretty.T
+  val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val str_of_source: Args.src -> string
-  val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
-  val output: Pretty.T list -> string
+  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
+    Args.src -> 'a list -> Pretty.T list
+  val output: Proof.context -> Pretty.T list -> string
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -38,11 +44,20 @@
 
 (** global options **)
 
-val display = Unsynchronized.ref false;
-val quotes = Unsynchronized.ref false;
-val indent = Unsynchronized.ref 0;
-val source = Unsynchronized.ref false;
-val break = Unsynchronized.ref false;
+val display_default = Unsynchronized.ref false;
+val quotes_default = Unsynchronized.ref false;
+val indent_default = Unsynchronized.ref 0;
+val source_default = Unsynchronized.ref false;
+val break_default = Unsynchronized.ref false;
+
+val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
+val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
+val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
+val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
+val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
+
+val _ = Context.>> (Context.map_theory
+ (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
 
 
 structure Wrappers = Proof_Data
@@ -438,22 +453,23 @@
 val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
 val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
 val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
-val _ = add_option "display" (add_wrapper o setmp_CRITICAL display o boolean);
-val _ = add_option "break" (add_wrapper o setmp_CRITICAL break o boolean);
-val _ = add_option "quotes" (add_wrapper o setmp_CRITICAL quotes o boolean);
+val _ = add_option "display" (Config.put display o boolean);
+val _ = add_option "break" (Config.put break o boolean);
+val _ = add_option "quotes" (Config.put quotes o boolean);
 val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
 val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
-val _ = add_option "indent" (add_wrapper o setmp_CRITICAL indent o integer);
-val _ = add_option "source" (add_wrapper o setmp_CRITICAL source o boolean);
+val _ = add_option "indent" (Config.put indent o integer);
+val _ = add_option "source" (Config.put source o boolean);
 val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
 
 
 (* basic pretty printing *)
 
-fun tweak_line s =
-  if ! display then s else Symbol.strip_blanks s;
+fun tweak_line ctxt s =
+  if Config.get ctxt display then s else Symbol.strip_blanks s;
 
-val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
+fun pretty_text ctxt =
+  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o Library.split_lines;
 
 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
 
@@ -502,19 +518,19 @@
 
 val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
 
-fun maybe_pretty_source pretty src xs =
-  map pretty xs  (*always pretty in order to exhibit errors!*)
-  |> (if ! source then K [pretty_text (str_of_source src)] else I);
+fun maybe_pretty_source pretty ctxt src xs =
+  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 output prts =
+fun output ctxt prts =
   prts
-  |> (if ! quotes then map Pretty.quote else I)
-  |> (if ! display then
-    map (Output.output o Pretty.string_of o Pretty.indent (! indent))
+  |> (if Config.get ctxt quotes then map Pretty.quote else I)
+  |> (if Config.get ctxt display then
+    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of))
+    map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 
@@ -527,11 +543,12 @@
 local
 
 fun basic_entities name scan pretty = antiquotation name scan
-  (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
+  (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) =>
-    output (maybe_pretty_source (fn x => pretty context (style, x)) source xs));
+    output context
+      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
 
 fun basic_entity name scan = basic_entities name (scan >> single);
 
@@ -545,7 +562,7 @@
 val _ = basic_entity "const" (Args.const_proper false) pretty_const;
 val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
 val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
-val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
+val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
 val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
 val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
 val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
@@ -566,7 +583,7 @@
   | _ => error "No proof state");
 
 fun goal_state name main_goal = antiquotation name (Scan.succeed ())
-  (fn {state, ...} => fn () => output
+  (fn {state, context, ...} => fn () => output context
     [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
 
 in
@@ -590,7 +607,7 @@
       val _ = context
         |> Proof.theorem NONE (K I) [[(prop, [])]]
         |> Proof.global_terminal_proof methods;
-    in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
+    in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
 
 
 (* ML text *)
@@ -601,8 +618,8 @@
   (fn {context, ...} => fn (txt, pos) =>
    (ML_Context.eval_in (SOME context) false pos (ml pos txt);
     Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
-    |> (if ! quotes then quote else I)
-    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+    |> (if Config.get context quotes then quote else I)
+    |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
     else
       split_lines
       #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")