# HG changeset patch # User wenzelm # Date 1282905620 -7200 # Node ID d8da44a8dd2562fb8587a8dbdbdc6b095c11886a # Parent 8891f4520d1656d32347f27c551c224921c04e83 proper context for various Thy_Output options, via official configuration options in ML and Isar; diff -r 8891f4520d16 -r d8da44a8dd25 NEWS --- 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 *** diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/IsarRef/Thy/ROOT-HOLCF.ML --- 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"; diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/IsarRef/Thy/ROOT-ZF.ML --- 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"; diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/IsarRef/Thy/ROOT.ML --- 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 [ diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/Main/Docs/Main_Doc.thy --- 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{* diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/System/Thy/ROOT.ML --- 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"]; diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/TutorialI/Rules/Primes.thy --- 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! diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/TutorialI/Types/Numbers.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{* diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/TutorialI/Types/document/Numbers.tex --- 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}% diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/TutorialI/settings.ML --- 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; diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/antiquote_setup.ML --- 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); diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/more_antiquote.ML --- 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 diff -r 8891f4520d16 -r d8da44a8dd25 doc-src/rail.ML --- 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; diff -r 8891f4520d16 -r d8da44a8dd25 src/HOL/Tools/Datatype/datatype_data.ML --- 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); diff -r 8891f4520d16 -r d8da44a8dd25 src/Pure/Thy/thy_output.ML --- 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 "|")