1.1 --- a/NEWS	Fri Aug 27 00:09:56 2010 +0200
     1.2 +++ b/NEWS	Fri Aug 27 12:40:20 2010 +0200
     1.3 @@ -23,6 +23,22 @@
     1.4  at the cost of clarity of file dependencies.  Recall that Isabelle/ML
     1.5  files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
     1.6  
     1.7 +* Various options that affect document antiquotations are now properly
     1.8 +handled within the context via configuration options, instead of
     1.9 +unsynchronized references.  There are both ML Config.T entities and
    1.10 +Isar declaration attributes to access these.
    1.11 +
    1.12 +  ML:                       Isar:
    1.13 +
    1.14 +  Thy_Output.display        thy_output_display
    1.15 +  Thy_Output.quotes         thy_output_quotes
    1.16 +  Thy_Output.indent         thy_output_indent
    1.17 +  Thy_Output.source         thy_output_source
    1.18 +  Thy_Output.break          thy_output_break
    1.19 +
    1.20 +Note that the corresponding "..._default" references may be only
    1.21 +changed globally at the ROOT session setup, but *not* within a theory.
    1.22 +
    1.23  
    1.24  *** Pure ***
    1.25  

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

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

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

     5.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Fri Aug 27 00:09:56 2010 +0200
     5.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Fri Aug 27 12:40:20 2010 +0200
     5.3 @@ -10,9 +10,9 @@
     5.4     Syntax.pretty_typ ctxt T)
     5.5  
     5.6  val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
     5.7 -  (fn {source, context, ...} => fn arg =>
     5.8 -    Thy_Output.output
     5.9 -      (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    5.10 +  (fn {source, context = ctxt, ...} => fn arg =>
    5.11 +    Thy_Output.output ctxt
    5.12 +      (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]));
    5.13  *}
    5.14  (*>*)
    5.15  text{*

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

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

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

     9.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Fri Aug 27 00:09:56 2010 +0200
     9.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Fri Aug 27 12:40:20 2010 +0200
     9.3 @@ -26,16 +26,16 @@
     9.4  %
     9.5  \isatagML
     9.6  \isacommand{ML}\isamarkupfalse%
     9.7 -\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
     9.8 -\isacommand{ML}\isamarkupfalse%
     9.9 -\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
    9.10 +\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}%
    9.11  \endisatagML
    9.12  {\isafoldML}%
    9.13  %
    9.14  \isadelimML
    9.15 +\isanewline
    9.16  %
    9.17  \endisadelimML
    9.18 -%
    9.19 +\isacommand{declare}\isamarkupfalse%
    9.20 +\ {\isacharbrackleft}{\isacharbrackleft}thy{\isacharunderscore}output{\isacharunderscore}indent\ {\isacharequal}\ {\isadigit{0}}{\isacharbrackright}{\isacharbrackright}%
    9.21  \begin{isamarkuptext}%
    9.22  numeric literals; default simprules; can re-orient%
    9.23  \end{isamarkuptext}%

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

    11.1 --- a/doc-src/antiquote_setup.ML	Fri Aug 27 00:09:56 2010 +0200
    11.2 +++ b/doc-src/antiquote_setup.ML	Fri Aug 27 12:40:20 2010 +0200
    11.3 @@ -71,8 +71,8 @@
    11.4      in
    11.5        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    11.6        (txt'
    11.7 -      |> (if ! Thy_Output.quotes then quote else I)
    11.8 -      |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    11.9 +      |> (if Config.get ctxt Thy_Output.quotes then quote else I)
   11.10 +      |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   11.11            else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
   11.12      end);
   11.13  
   11.14 @@ -93,18 +93,18 @@
   11.15    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   11.16    (fn {context = ctxt, ...} =>
   11.17      map (apfst (Thy_Output.pretty_thm ctxt))
   11.18 -    #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
   11.19 -    #> (if ! Thy_Output.display
   11.20 +    #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
   11.21 +    #> (if Config.get ctxt Thy_Output.display
   11.22          then
   11.23            map (fn (p, name) =>
   11.24 -            Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
   11.25 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
   11.26 +            Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
   11.27 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
   11.28            #> space_implode "\\par\\smallskip%\n"
   11.29            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   11.30          else
   11.31            map (fn (p, name) =>
   11.32              Output.output (Pretty.str_of p) ^
   11.33 -            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
   11.34 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
   11.35            #> space_implode "\\par\\smallskip%\n"
   11.36            #> enclose "\\isa{" "}"));
   11.37  
   11.38 @@ -112,7 +112,8 @@
   11.39  (* theory file *)
   11.40  
   11.41  val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
   11.42 -  (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
   11.43 +  (fn {context = ctxt, ...} =>
   11.44 +    fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
   11.45  
   11.46  
   11.47  (* Isabelle/Isar entities (with index) *)
   11.48 @@ -152,8 +153,9 @@
   11.49            idx ^
   11.50            (Output.output name
   11.51              |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
   11.52 -            |> (if ! Thy_Output.quotes then quote else I)
   11.53 -            |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   11.54 +            |> (if Config.get ctxt Thy_Output.quotes then quote else I)
   11.55 +            |> (if Config.get ctxt Thy_Output.display
   11.56 +                then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   11.57                  else hyper o enclose "\\mbox{\\isa{" "}}"))
   11.58          else error ("Bad " ^ kind ^ " " ^ quote name)
   11.59        end);

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

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

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

    15.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 27 00:09:56 2010 +0200
    15.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 27 12:40:20 2010 +0200
    15.3 @@ -6,11 +6,16 @@
    15.4  
    15.5  signature THY_OUTPUT =
    15.6  sig
    15.7 -  val display: bool Unsynchronized.ref
    15.8 -  val quotes: bool Unsynchronized.ref
    15.9 -  val indent: int Unsynchronized.ref
   15.10 -  val source: bool Unsynchronized.ref
   15.11 -  val break: bool Unsynchronized.ref
   15.12 +  val display_default: bool Unsynchronized.ref
   15.13 +  val quotes_default: bool Unsynchronized.ref
   15.14 +  val indent_default: int Unsynchronized.ref
   15.15 +  val source_default: bool Unsynchronized.ref
   15.16 +  val break_default: bool Unsynchronized.ref
   15.17 +  val display: bool Config.T
   15.18 +  val quotes: bool Config.T
   15.19 +  val indent: int Config.T
   15.20 +  val source: bool Config.T
   15.21 +  val break: bool Config.T
   15.22    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   15.23    val add_option: string -> (string -> Proof.context -> Proof.context) -> unit
   15.24    val defined_command: string -> bool
   15.25 @@ -25,12 +30,13 @@
   15.26    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   15.27    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
   15.28      (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
   15.29 -  val pretty_text: string -> Pretty.T
   15.30 +  val pretty_text: Proof.context -> string -> Pretty.T
   15.31    val pretty_term: Proof.context -> term -> Pretty.T
   15.32    val pretty_thm: Proof.context -> thm -> Pretty.T
   15.33    val str_of_source: Args.src -> string
   15.34 -  val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
   15.35 -  val output: Pretty.T list -> string
   15.36 +  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
   15.37 +    Args.src -> 'a list -> Pretty.T list
   15.38 +  val output: Proof.context -> Pretty.T list -> string
   15.39  end;
   15.40  
   15.41  structure Thy_Output: THY_OUTPUT =
   15.42 @@ -38,11 +44,20 @@
   15.43  
   15.44  (** global options **)
   15.45  
   15.46 -val display = Unsynchronized.ref false;
   15.47 -val quotes = Unsynchronized.ref false;
   15.48 -val indent = Unsynchronized.ref 0;
   15.49 -val source = Unsynchronized.ref false;
   15.50 -val break = Unsynchronized.ref false;
   15.51 +val display_default = Unsynchronized.ref false;
   15.52 +val quotes_default = Unsynchronized.ref false;
   15.53 +val indent_default = Unsynchronized.ref 0;
   15.54 +val source_default = Unsynchronized.ref false;
   15.55 +val break_default = Unsynchronized.ref false;
   15.56 +
   15.57 +val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
   15.58 +val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
   15.59 +val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
   15.60 +val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
   15.61 +val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
   15.62 +
   15.63 +val _ = Context.>> (Context.map_theory
   15.64 + (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
   15.65  
   15.66  
   15.67  structure Wrappers = Proof_Data
   15.68 @@ -438,22 +453,23 @@
   15.69  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
   15.70  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
   15.71  val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
   15.72 -val _ = add_option "display" (add_wrapper o setmp_CRITICAL display o boolean);
   15.73 -val _ = add_option "break" (add_wrapper o setmp_CRITICAL break o boolean);
   15.74 -val _ = add_option "quotes" (add_wrapper o setmp_CRITICAL quotes o boolean);
   15.75 +val _ = add_option "display" (Config.put display o boolean);
   15.76 +val _ = add_option "break" (Config.put break o boolean);
   15.77 +val _ = add_option "quotes" (Config.put quotes o boolean);
   15.78  val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
   15.79  val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);
   15.80 -val _ = add_option "indent" (add_wrapper o setmp_CRITICAL indent o integer);
   15.81 -val _ = add_option "source" (add_wrapper o setmp_CRITICAL source o boolean);
   15.82 +val _ = add_option "indent" (Config.put indent o integer);
   15.83 +val _ = add_option "source" (Config.put source o boolean);
   15.84  val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer);
   15.85  
   15.86  
   15.87  (* basic pretty printing *)
   15.88  
   15.89 -fun tweak_line s =
   15.90 -  if ! display then s else Symbol.strip_blanks s;
   15.91 +fun tweak_line ctxt s =
   15.92 +  if Config.get ctxt display then s else Symbol.strip_blanks s;
   15.93  
   15.94 -val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
   15.95 +fun pretty_text ctxt =
   15.96 +  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o Library.split_lines;
   15.97  
   15.98  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
   15.99  
  15.100 @@ -502,19 +518,19 @@
  15.101  
  15.102  val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
  15.103  
  15.104 -fun maybe_pretty_source pretty src xs =
  15.105 -  map pretty xs  (*always pretty in order to exhibit errors!*)
  15.106 -  |> (if ! source then K [pretty_text (str_of_source src)] else I);
  15.107 +fun maybe_pretty_source pretty ctxt src xs =
  15.108 +  map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
  15.109 +  |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
  15.110  
  15.111 -fun output prts =
  15.112 +fun output ctxt prts =
  15.113    prts
  15.114 -  |> (if ! quotes then map Pretty.quote else I)
  15.115 -  |> (if ! display then
  15.116 -    map (Output.output o Pretty.string_of o Pretty.indent (! indent))
  15.117 +  |> (if Config.get ctxt quotes then map Pretty.quote else I)
  15.118 +  |> (if Config.get ctxt display then
  15.119 +    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
  15.120      #> space_implode "\\isasep\\isanewline%\n"
  15.121      #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
  15.122    else
  15.123 -    map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of))
  15.124 +    map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
  15.125      #> space_implode "\\isasep\\isanewline%\n"
  15.126      #> enclose "\\isa{" "}");
  15.127  
  15.128 @@ -527,11 +543,12 @@
  15.129  local
  15.130  
  15.131  fun basic_entities name scan pretty = antiquotation name scan
  15.132 -  (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
  15.133 +  (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
  15.134  
  15.135  fun basic_entities_style name scan pretty = antiquotation name scan
  15.136    (fn {source, context, ...} => fn (style, xs) =>
  15.137 -    output (maybe_pretty_source (fn x => pretty context (style, x)) source xs));
  15.138 +    output context
  15.139 +      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
  15.140  
  15.141  fun basic_entity name scan = basic_entities name (scan >> single);
  15.142  
  15.143 @@ -545,7 +562,7 @@
  15.144  val _ = basic_entity "const" (Args.const_proper false) pretty_const;
  15.145  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
  15.146  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
  15.147 -val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
  15.148 +val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
  15.149  val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
  15.150  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
  15.151  val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
  15.152 @@ -566,7 +583,7 @@
  15.153    | _ => error "No proof state");
  15.154  
  15.155  fun goal_state name main_goal = antiquotation name (Scan.succeed ())
  15.156 -  (fn {state, ...} => fn () => output
  15.157 +  (fn {state, context, ...} => fn () => output context
  15.158      [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
  15.159  
  15.160  in
  15.161 @@ -590,7 +607,7 @@
  15.162        val _ = context
  15.163          |> Proof.theorem NONE (K I) [[(prop, [])]]
  15.164          |> Proof.global_terminal_proof methods;
  15.165 -    in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
  15.166 +    in output context (maybe_pretty_source pretty_term context prop_src [prop]) end);
  15.167  
  15.168  
  15.169  (* ML text *)
  15.170 @@ -601,8 +618,8 @@
  15.171    (fn {context, ...} => fn (txt, pos) =>
  15.172     (ML_Context.eval_in (SOME context) false pos (ml pos txt);
  15.173      Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
  15.174 -    |> (if ! quotes then quote else I)
  15.175 -    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
  15.176 +    |> (if Config.get context quotes then quote else I)
  15.177 +    |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
  15.178      else
  15.179        split_lines
  15.180        #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")