# HG changeset patch # User wenzelm # Date 1302954525 -7200 # Node ID b47d41d9f4b5266dc6ec6d400a7ff99a3942db71 # Parent 3305f573294ebf4ca7451b932b45ccd0f8744d55 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references; diff -r 3305f573294e -r b47d41d9f4b5 NEWS --- a/NEWS Sat Apr 16 12:46:18 2011 +0200 +++ b/NEWS Sat Apr 16 13:48:45 2011 +0200 @@ -37,6 +37,13 @@ Note that automated detection from the file-system or search path has been discontinued. INCOMPATIBILITY. +* Name space: proper configuration options "long_names", +"short_names", "unique_names" instead of former unsynchronized +references. Minor INCOMPATIBILITY, need to declare options in context +like this: + + declare [[unique_names = false]] + *** HOL *** diff -r 3305f573294e -r b47d41d9f4b5 doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Sat Apr 16 13:48:45 2011 +0200 @@ -22,6 +22,6 @@ setup {* Code_Target.set_default_code_width 74 *} -ML_command {* unique_names := false *} +declare [[unique_names = false]] end diff -r 3305f573294e -r b47d41d9f4b5 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sat Apr 16 13:48:45 2011 +0200 @@ -1112,7 +1112,7 @@ @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\ @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\ - @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\ + @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\ @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"} \end{mldecls} @@ -1187,7 +1187,7 @@ (or their derivatives for @{ML_type theory} and @{ML_type Proof.context}). - \item @{ML Name_Space.extern}~@{text "space name"} externalizes a + \item @{ML Name_Space.extern}~@{text "ctxt space name"} externalizes a (fully qualified) internal name. This operation is mostly for printing! User code should not rely on diff -r 3305f573294e -r b47d41d9f4b5 doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Apr 16 13:48:45 2011 +0200 @@ -1610,7 +1610,7 @@ \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline% \verb| string * Name_Space.T| \\ \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\ - \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\ + \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\ \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool| \end{mldecls} @@ -1679,7 +1679,7 @@ (or their derivatives for \verb|theory| and \verb|Proof.context|). - \item \verb|Name_Space.extern|~\isa{space\ name} externalizes a + \item \verb|Name_Space.extern|~\isa{ctxt\ space\ name} externalizes a (fully qualified) internal name. This operation is mostly for printing! User code should not rely on diff -r 3305f573294e -r b47d41d9f4b5 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Apr 16 13:48:45 2011 +0200 @@ -100,10 +100,10 @@ @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\ @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\ @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\ - @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\ - @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\ - @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\ @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\ + @{index_ML Name_Space.long_names: "bool Config.T"} & default @{ML false} \\ + @{index_ML Name_Space.short_names: "bool Config.T"} & default @{ML false} \\ + @{index_ML Name_Space.unique_names: "bool Config.T"} & default @{ML true} \\ @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\ @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\ @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\ @@ -144,11 +144,6 @@ \item @{ML show_abbrevs} controls folding of constant abbreviations. - \item @{ML long_names}, @{ML short_names}, and @{ML unique_names} - control the way of printing fully qualified internal names in - external form. See also \secref{sec:antiq} for the document - antiquotation options of the same names. - \item @{ML show_brackets} controls bracketing in pretty printed output. If set to @{ML true}, all sub-expressions of the pretty printing tree will be parenthesized, even if this produces malformed @@ -156,6 +151,12 @@ pretty printed entities may occasionally help to diagnose problems with operator priorities, for example. + \item @{ML Name_Space.long_names}, @{ML Name_Space.short_names}, and + @{ML Name_Space.unique_names} control the way of printing fully + qualified internal names in external form. See also + \secref{sec:antiq} for the document antiquotation options of the + same names. + \item @{ML eta_contract} controls @{text "\"}-contracted printing of terms. diff -r 3305f573294e -r b47d41d9f4b5 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Apr 16 13:48:45 2011 +0200 @@ -122,10 +122,10 @@ \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\ \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\ - \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\ - \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\ - \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\ \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\ + \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\ + \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\ + \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\ \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\ \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\ \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\ @@ -165,11 +165,6 @@ \item \verb|show_abbrevs| controls folding of constant abbreviations. - \item \verb|long_names|, \verb|short_names|, and \verb|unique_names| - control the way of printing fully qualified internal names in - external form. See also \secref{sec:antiq} for the document - antiquotation options of the same names. - \item \verb|show_brackets| controls bracketing in pretty printed output. If set to \verb|true|, all sub-expressions of the pretty printing tree will be parenthesized, even if this produces malformed @@ -177,6 +172,12 @@ pretty printed entities may occasionally help to diagnose problems with operator priorities, for example. + \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and + \verb|Name_Space.unique_names| control the way of printing fully + qualified internal names in external form. See also + \secref{sec:antiq} for the document antiquotation options of the + same names. + \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of terms. diff -r 3305f573294e -r b47d41d9f4b5 doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Sat Apr 16 13:48:45 2011 +0200 @@ -152,11 +152,8 @@ the qualified name, for example @{text "T.length"}, where @{text T} is the theory it is defined in, to distinguish it from the predefined @{const[source] "List.length"}. In case there is no danger of confusion, you can insist on -short names (no qualifiers) by setting \verb!short_names!, typically -in \texttt{ROOT.ML}: -\begin{quote} -@{ML "short_names := true"}\verb!;! -\end{quote} +short names (no qualifiers) by setting the \verb!short_names! +configuration option in the context. *} subsection {*Variable names\label{sec:varnames}*} diff -r 3305f573294e -r b47d41d9f4b5 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Sat Apr 16 13:48:45 2011 +0200 @@ -195,11 +195,8 @@ If there are multiple declarations of the same name, Isabelle prints the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on -short names (no qualifiers) by setting \verb!short_names!, typically -in \texttt{ROOT.ML}: -\begin{quote} -\verb|short_names := true|\verb!;! -\end{quote}% +short names (no qualifiers) by setting the \verb!short_names! +configuration option in the context.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 3305f573294e -r b47d41d9f4b5 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/TutorialI/Misc/Itrev.thy Sat Apr 16 13:48:45 2011 +0200 @@ -2,7 +2,7 @@ theory Itrev imports Main begin -ML"unique_names := false" +declare [[unique_names = false]] (*>*) section{*Induction Heuristics*} @@ -141,6 +141,6 @@ \index{induction heuristics|)} *} (*<*) -ML"unique_names := true" +declare [[unique_names = true]] end (*>*) diff -r 3305f573294e -r b47d41d9f4b5 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Sat Apr 16 13:48:45 2011 +0200 @@ -15,19 +15,6 @@ % \endisadelimtheory % -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% \isamarkupsection{Induction Heuristics% } \isamarkuptrue% @@ -216,19 +203,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% \isadelimtheory % \endisadelimtheory diff -r 3305f573294e -r b47d41d9f4b5 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Apr 16 13:48:45 2011 +0200 @@ -848,8 +848,8 @@ th |> backquote_thm else let - val name1 = Facts.extern facts name0 - val name2 = Name_Space.extern full_space name0 + val name1 = Facts.extern ctxt facts name0 + val name2 = Name_Space.extern ctxt full_space name0 in case find_first check_thms [name1, name2, name0] of SOME name => make_name reserved multi j name diff -r 3305f573294e -r b47d41d9f4b5 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Apr 16 13:48:45 2011 +0200 @@ -151,7 +151,7 @@ val (tab, monos) = get_inductives ctxt; val space = Consts.space_of (ProofContext.consts_of ctxt); in - [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))), + [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))), Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] |> Pretty.chunks |> Pretty.writeln end; diff -r 3305f573294e -r b47d41d9f4b5 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/HOL/Tools/record.ML Sat Apr 16 13:48:45 2011 +0200 @@ -914,7 +914,7 @@ fun record_tr' ctxt t = let val thy = ProofContext.theory_of ctxt; - val extern = Consts.extern (ProofContext.consts_of ctxt); + val extern = Consts.extern ctxt (ProofContext.consts_of ctxt); fun strip_fields t = (case strip_comb t of @@ -957,7 +957,7 @@ fun dest_update ctxt c = (case try Lexicon.unmark_const c of - SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d) + SOME d => try (unsuffix updateN) (Consts.extern ctxt (ProofContext.consts_of ctxt) d) | NONE => NONE); fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) = diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/General/name_space.ML Sat Apr 16 13:48:45 2011 +0200 @@ -7,16 +7,8 @@ type xstring = string; (*external names*) -signature BASIC_NAME_SPACE = -sig - val long_names: bool Unsynchronized.ref - val short_names: bool Unsynchronized.ref - val unique_names: bool Unsynchronized.ref -end; - signature NAME_SPACE = sig - include BASIC_NAME_SPACE val hidden: string -> string val is_hidden: string -> bool type T @@ -27,9 +19,16 @@ val markup_entry: T -> string -> Markup.T val is_concealed: T -> string -> bool val intern: T -> xstring -> string - val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} -> - T -> string -> xstring - val extern: T -> string -> xstring + val long_names_default: bool Unsynchronized.ref + val long_names_raw: Config.raw + val long_names: bool Config.T + val short_names_default: bool Unsynchronized.ref + val short_names_raw: Config.raw + val short_names: bool Config.T + val unique_names_default: bool Unsynchronized.ref + val unique_names_raw: Config.raw + val unique_names: bool Config.T + val extern: Proof.context -> T -> string -> xstring val hide: bool -> string -> T -> T val merge: T * T -> T type naming @@ -55,8 +54,8 @@ val merge_tables: 'a table * 'a table -> 'a table val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table - val dest_table: 'a table -> (string * 'a) list - val extern_table: 'a table -> (xstring * 'a) list + val dest_table: Proof.context -> 'a table -> (string * 'a) list + val extern_table: Proof.context -> 'a table -> (xstring * 'a) list end; structure Name_Space: NAME_SPACE = @@ -154,8 +153,25 @@ fun intern space xname = #1 (lookup space xname); -fun extern_flags {long_names, short_names, unique_names} space name = + +val long_names_default = Unsynchronized.ref false; +val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default)); +val long_names = Config.bool long_names_raw; + +val short_names_default = Unsynchronized.ref false; +val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default)); +val short_names = Config.bool short_names_raw; + +val unique_names_default = Unsynchronized.ref true; +val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default)); +val unique_names = Config.bool unique_names_raw; + +fun extern ctxt space name = let + val long_names = Config.get ctxt long_names; + val short_names = Config.get ctxt short_names; + val unique_names = Config.get ctxt unique_names; + fun valid require_unique xname = let val (name', is_unique) = lookup space xname in name = name' andalso (not require_unique orelse is_unique) end; @@ -168,16 +184,6 @@ else ext (get_accesses space name) end; -val long_names = Unsynchronized.ref false; -val short_names = Unsynchronized.ref false; -val unique_names = Unsynchronized.ref true; - -fun extern space name = - extern_flags - {long_names = ! long_names, - short_names = ! short_names, - unique_names = ! unique_names} space name; - (* modify internals *) @@ -385,15 +391,12 @@ fun join_tables f ((space1, tab1), (space2, tab2)) = (merge (space1, space2), Symtab.join f (tab1, tab2)); -fun ext_table (space, tab) = - Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab [] +fun ext_table ctxt (space, tab) = + Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab [] |> Library.sort_wrt (#2 o #1); -fun dest_table tab = map (apfst #1) (ext_table tab); -fun extern_table tab = map (apfst #2) (ext_table tab); +fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab); +fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab); end; -structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space; -open Basic_Name_Space; - diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Isar/attrib.ML Sat Apr 16 13:48:45 2011 +0200 @@ -73,11 +73,12 @@ fun print_attributes thy = let + val ctxt = ProofContext.init_global thy; val attribs = Attributes.get thy; fun prt_attr (name, (_, comment)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in - [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))] + [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))] |> Pretty.chunks |> Pretty.writeln end; @@ -90,7 +91,7 @@ val intern = Name_Space.intern o #1 o Attributes.get; val intern_src = Args.map_name o intern; -val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of; +fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt))); (* pretty printing *) @@ -341,7 +342,7 @@ Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1, Pretty.str (Config.print_value value)] end; - val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy); + val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy); in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; @@ -408,6 +409,9 @@ register_config Printer.show_question_marks_raw #> register_config Syntax.ambiguity_level_raw #> register_config Syntax_Trans.eta_contract_raw #> + register_config Name_Space.long_names_raw #> + register_config Name_Space.short_names_raw #> + register_config Name_Space.unique_names_raw #> register_config ML_Context.trace_raw #> register_config ProofContext.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Isar/expression.ML Sat Apr 16 13:48:45 2011 +0200 @@ -616,7 +616,7 @@ fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args => if length args = n then Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) - Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) + Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args) else raise Match); (* define one predicate including its intro rule and axioms diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 16 13:48:45 2011 +0200 @@ -399,11 +399,11 @@ val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => let - val thy = Toplevel.theory_of state; - val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy); + val ctxt = Toplevel.context_of state; + val {classes = (space, algebra), ...} = Type.rep_tsig (ProofContext.tsig_of ctxt); val classes = Sorts.classes_of algebra; fun entry (c, (i, (_, cs))) = - (i, {name = Name_Space.extern space c, ID = c, parents = cs, + (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs, dir = "", unfold = true, path = ""}); val gr = Graph.fold (cons o entry) classes [] diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Isar/locale.ML Sat Apr 16 13:48:45 2011 +0200 @@ -162,7 +162,7 @@ ); val intern = Name_Space.intern o #1 o Locales.get; -val extern = Name_Space.extern o #1 o Locales.get; +fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy)); val get_locale = Symtab.lookup o #2 o Locales.get; val defined = Symtab.defined o #2 o Locales.get; @@ -630,7 +630,8 @@ val all_locales = Symtab.keys o snd o Locales.get; fun print_locales thy = - Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy))) + Pretty.strs ("locales:" :: + map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy))) |> Pretty.writeln; fun print_locale thy show_facts raw_name = diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Isar/method.ML Sat Apr 16 13:48:45 2011 +0200 @@ -334,11 +334,12 @@ fun print_methods thy = let + val ctxt = ProofContext.init_global thy; val meths = Methods.get thy; fun prt_meth (name, (_, comment)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in - [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))] + [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))] |> Pretty.chunks |> Pretty.writeln end; diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat Apr 16 13:48:45 2011 +0200 @@ -304,8 +304,8 @@ val global_facts = Global_Theory.facts_of (theory_of ctxt); in if is_some (Facts.lookup (Context.Proof ctxt) local_facts name) - then Facts.extern local_facts name - else Facts.extern global_facts name + then Facts.extern ctxt local_facts name + else Facts.extern ctxt global_facts name end; @@ -1152,7 +1152,8 @@ | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t)); - val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts [])); + val abbrevs = + Name_Space.extern_table ctxt (space, Symtab.make (Symtab.fold add_abbr consts [])); in if null abbrevs then [] else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Sat Apr 16 13:48:45 2011 +0200 @@ -124,7 +124,7 @@ bool_pref Goal_Display.show_consts_default "show-consts" "Show types of consts in Isabelle goal display", - bool_pref long_names + bool_pref Name_Space.long_names_default "long-names" "Show fully qualified names in Isabelle terms", bool_pref Printer.show_brackets_default diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Apr 16 13:48:45 2011 +0200 @@ -517,12 +517,15 @@ local -fun theory_facts name = +fun theory_facts thy = + (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy); + +fun thms_of_thy name = let val thy = Thy_Info.get_theory name - in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end; + in map fst (theory_facts thy |-> Facts.extern_static (ProofContext.init_global thy)) end; -fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static); -fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static); +fun qualified_thms_of_thy name = + map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static); in diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Apr 16 13:48:45 2011 +0200 @@ -605,6 +605,8 @@ fun unparse_t t_to_ast prt_t markup ctxt t = let val syn = ProofContext.syn_of ctxt; + val tsig = ProofContext.tsig_of ctxt; + val consts = ProofContext.consts_of ctxt; fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) @@ -620,9 +622,9 @@ SOME "" => ([], c) | SOME b => markup_extern b | NONE => c |> Lexicon.unmark - {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x), - case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x), - case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x), + {case_class = fn x => ([Markup.tclass x], Type.extern_class ctxt tsig x), + case_type = fn x => ([Markup.tycon x], Type.extern_type ctxt tsig x), + case_const = fn x => ([Markup.const x], Consts.extern ctxt consts x), case_fixed = fn x => free_or_skolem ctxt x, case_default = fn x => ([], x)}); in diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Sat Apr 16 13:48:45 2011 +0200 @@ -450,9 +450,9 @@ val _ = add_option "show_structs" (Config.put show_structs o boolean); val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean); val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean); -val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); -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 "long_names" (Config.put Name_Space.long_names o boolean); +val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean); +val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean); val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean); val _ = add_option "display" (Config.put display o boolean); val _ = add_option "break" (Config.put break o boolean); @@ -510,11 +510,11 @@ in ProofContext.pretty_term_abbrev ctxt' eq end; fun pretty_class ctxt = - Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt; + Pretty.str o Type.extern_class ctxt (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt; fun pretty_type ctxt s = let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s - in Pretty.str (Type.extern_type (ProofContext.tsig_of ctxt) name) end; + in Pretty.str (Type.extern_type ctxt (ProofContext.tsig_of ctxt) name) end; fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/Tools/find_theorems.ML Sat Apr 16 13:48:45 2011 +0200 @@ -381,8 +381,11 @@ val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt)); val shorten = - Name_Space.extern_flags - {long_names = false, short_names = false, unique_names = false} space; + Name_Space.extern + (ctxt + |> Config.put Name_Space.long_names false + |> Config.put Name_Space.short_names false + |> Config.put Name_Space.unique_names false) space; fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = nicer_name (shorten x, i) (shorten y, j) diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/consts.ML --- a/src/Pure/consts.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/consts.ML Sat Apr 16 13:48:45 2011 +0200 @@ -22,9 +22,9 @@ val alias: Name_Space.naming -> binding -> string -> T -> T val is_concealed: T -> string -> bool val intern: T -> xstring -> string - val extern: T -> string -> xstring + val extern: Proof.context -> T -> string -> xstring val intern_syntax: T -> xstring -> string - val extern_syntax: T -> string -> xstring + val extern_syntax: Proof.context -> T -> string -> xstring val read_const: T -> string -> term val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list @@ -129,16 +129,16 @@ val is_concealed = Name_Space.is_concealed o space_of; val intern = Name_Space.intern o space_of; -val extern = Name_Space.extern o space_of; +fun extern ctxt = Name_Space.extern ctxt o space_of; fun intern_syntax consts s = (case try Lexicon.unmark_const s of SOME c => c | NONE => intern consts s); -fun extern_syntax consts s = +fun extern_syntax ctxt consts s = (case try Lexicon.unmark_const s of - SOME c => extern consts c + SOME c => extern ctxt consts c | NONE => s); diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/display.ML --- a/src/Pure/display.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/display.ML Sat Apr 16 13:48:45 2011 +0200 @@ -187,25 +187,25 @@ val {restricts, reducts} = Defs.dest defs; val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy; val {constants, constraints} = Consts.dest consts; - val extern_const = Name_Space.extern (#1 constants); + val extern_const = Name_Space.extern ctxt (#1 constants); val {classes, default, types, ...} = Type.rep_tsig tsig; val (class_space, class_algebra) = classes; val classes = Sorts.classes_of class_algebra; val arities = Sorts.arities_of class_algebra; - val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes)); - val tdecls = Name_Space.dest_table types; - val arties = Name_Space.dest_table (Sign.type_space thy, arities); + val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes)); + val tdecls = Name_Space.dest_table ctxt types; + val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities); fun prune_const c = not verbose andalso Consts.is_concealed consts c; - val cnsts = Name_Space.extern_table (#1 constants, + val cnsts = Name_Space.extern_table ctxt (#1 constants, Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants)))); val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; - val cnstrs = Name_Space.extern_table constraints; + val cnstrs = Name_Space.extern_table ctxt constraints; - val axms = Name_Space.extern_table axioms; + val axms = Name_Space.extern_table ctxt axioms; val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts |> map (fn (lhs, rhs) => @@ -225,7 +225,7 @@ Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), Pretty.big_list "axioms:" (map pretty_axm axms), - Pretty.strs ("oracles:" :: Thm.extern_oracles thy), + Pretty.strs ("oracles:" :: Thm.extern_oracles ctxt), Pretty.big_list "definitions:" [pretty_finals reds0, Pretty.big_list "non-overloaded:" (map pretty_reduct reds1), diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/facts.ML --- a/src/Pure/facts.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/facts.ML Sat Apr 16 13:48:45 2011 +0200 @@ -23,12 +23,12 @@ val space_of: T -> Name_Space.T val is_concealed: T -> string -> bool val intern: T -> xstring -> string - val extern: T -> string -> xstring + val extern: Proof.context -> T -> string -> xstring val lookup: Context.generic -> T -> string -> (bool * thm list) option val defined: T -> string -> bool val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a val dest_static: T list -> T -> (string * thm list) list - val extern_static: T list -> T -> (xstring * thm list) list + val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list val props: T -> thm list val could_unify: T -> term -> thm list val merge: T * T -> T @@ -141,7 +141,7 @@ val is_concealed = Name_Space.is_concealed o space_of; val intern = Name_Space.intern o space_of; -val extern = Name_Space.extern o space_of; +fun extern ctxt = Name_Space.extern ctxt o space_of; val defined = Symtab.defined o table_of; @@ -165,8 +165,8 @@ fun dest_static prev_facts facts = sort_wrt #1 (diff_table prev_facts facts); -fun extern_static prev_facts facts = - sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts))); +fun extern_static ctxt prev_facts facts = + sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts))); (* indexed props *) diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/sign.ML Sat Apr 16 13:48:45 2011 +0200 @@ -233,11 +233,11 @@ fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; val intern_class = Name_Space.intern o class_space; -val extern_class = Name_Space.extern o class_space; +fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy); val intern_type = Name_Space.intern o type_space; -val extern_type = Name_Space.extern o type_space; +fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy); val intern_const = Name_Space.intern o const_space; -val extern_const = Name_Space.extern o const_space; +fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy); diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/thm.ML Sat Apr 16 13:48:45 2011 +0200 @@ -147,7 +147,7 @@ val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq - val extern_oracles: theory -> xstring list + val extern_oracles: Proof.context -> xstring list val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory end; @@ -1734,7 +1734,8 @@ fun merge data : T = Name_Space.merge_tables data; ); -val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get; +fun extern_oracles ctxt = + map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt))); fun add_oracle (b, oracle) thy = let diff -r 3305f573294e -r b47d41d9f4b5 src/Pure/type.ML --- a/src/Pure/type.ML Sat Apr 16 12:46:18 2011 +0200 +++ b/src/Pure/type.ML Sat Apr 16 13:48:45 2011 +0200 @@ -28,7 +28,7 @@ val class_space: tsig -> Name_Space.T val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig val intern_class: tsig -> xstring -> string - val extern_class: tsig -> string -> xstring + val extern_class: Proof.context -> tsig -> string -> xstring val defaultS: tsig -> sort val logical_types: tsig -> string list val eq_sort: tsig -> sort * sort -> bool @@ -49,7 +49,7 @@ val type_space: tsig -> Name_Space.T val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig val intern_type: tsig -> xstring -> string - val extern_type: tsig -> string -> xstring + val extern_type: Proof.context -> tsig -> string -> xstring val is_logtype: tsig -> string -> bool val the_decl: tsig -> string -> decl val cert_typ_mode: mode -> tsig -> typ -> typ @@ -192,7 +192,7 @@ ((Name_Space.alias naming binding name space, classes), default, types)); val intern_class = Name_Space.intern o class_space; -val extern_class = Name_Space.extern o class_space; +fun extern_class ctxt = Name_Space.extern ctxt o class_space; fun defaultS (TSig {default, ...}) = default; fun logical_types (TSig {log_types, ...}) = log_types; @@ -237,7 +237,7 @@ (classes, default, (Name_Space.alias naming binding name space, types))); val intern_type = Name_Space.intern o type_space; -val extern_type = Name_Space.extern o type_space; +fun extern_type ctxt = Name_Space.extern ctxt o type_space; val is_logtype = member (op =) o logical_types;