# HG changeset patch # User wenzelm # Date 1413233009 -7200 # Node ID 1891f17c612470dd91f9305ed9c00e836c3c209a # Parent d2a7b443ceb277155bad15a4ca77b80086f74f59 tuned signature; diff -r d2a7b443ceb2 -r 1891f17c6124 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Mon Oct 13 21:57:40 2014 +0200 +++ b/src/Doc/Implementation/Prelim.thy Mon Oct 13 22:43:29 2014 +0200 @@ -922,7 +922,7 @@ \end{mldecls} \begin{mldecls} @{index_ML_type Name_Space.naming} \\ - @{index_ML Name_Space.default_naming: Name_Space.naming} \\ + @{index_ML Name_Space.global_naming: Name_Space.naming} \\ @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\ @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\ \end{mldecls} @@ -975,9 +975,9 @@ \item Type @{ML_type Name_Space.naming} represents the abstract concept of a naming policy. - \item @{ML Name_Space.default_naming} is the default naming policy. - In a theory context, this is usually augmented by a path prefix - consisting of the theory name. + \item @{ML Name_Space.global_naming} is the default naming policy: it is + global and lacks any path prefix. In a regular theory context this is + augmented by a path prefix consisting of the theory name. \item @{ML Name_Space.add_path}~@{text "path naming"} augments the naming policy by extending its path component. diff -r d2a7b443ceb2 -r 1891f17c6124 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Oct 13 21:57:40 2014 +0200 +++ b/src/Pure/General/name_space.ML Mon Oct 13 22:43:29 2014 +0200 @@ -44,7 +44,7 @@ val parent_path: naming -> naming val mandatory_path: string -> naming -> naming val qualified_path: bool -> binding -> naming -> naming - val default_naming: naming + val global_naming: naming val local_naming: naming val transform_binding: naming -> binding -> binding val full_name: naming -> binding -> string @@ -324,8 +324,8 @@ fun qualified_path mandatory binding = map_path (fn path => path @ #2 (Binding.dest (Binding.qualified mandatory "" binding))); -val default_naming = make_naming (false, NONE, "", []); -val local_naming = default_naming |> add_path Long_Name.localN; +val global_naming = make_naming (false, NONE, "", []); +val local_naming = global_naming |> add_path Long_Name.localN; (* full name *) @@ -354,7 +354,7 @@ fun full_name naming = name_spec naming #> #2 #> map #1 #> Long_Name.implode; -val base_name = full_name default_naming #> Long_Name.base_name; +val base_name = full_name global_naming #> Long_Name.base_name; (* accesses *) @@ -411,9 +411,9 @@ structure Data_Args = struct type T = naming; - val empty = default_naming; - fun extend _ = default_naming; - fun merge _ = default_naming; + val empty = global_naming; + fun extend _ = global_naming; + fun merge _ = global_naming; fun init _ = local_naming; end; diff -r d2a7b443ceb2 -r 1891f17c6124 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Oct 13 21:57:40 2014 +0200 +++ b/src/Pure/Isar/class.ML Mon Oct 13 22:43:29 2014 +0200 @@ -326,7 +326,7 @@ fun guess_morphism_identity (b, rhs) phi1 phi2 = let (*FIXME proper concept to identify morphism instead of educated guess*) - val name_of_binding = Name_Space.full_name Name_Space.default_naming; + val name_of_binding = Name_Space.full_name Name_Space.global_naming; val n1 = (name_of_binding o Morphism.binding phi1) b; val n2 = (name_of_binding o Morphism.binding phi2) b; val rhs1 = Morphism.term phi1 rhs; diff -r d2a7b443ceb2 -r 1891f17c6124 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Oct 13 21:57:40 2014 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Oct 13 22:43:29 2014 +0200 @@ -1197,7 +1197,7 @@ fun update_cases is_proper args ctxt = let - val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming); + val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming); val cases = cases_of ctxt; val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0; val (cases', _) = fold (update_case context is_proper) args (cases, index); diff -r d2a7b443ceb2 -r 1891f17c6124 src/Pure/Tools/plugin.ML --- a/src/Pure/Tools/plugin.ML Mon Oct 13 21:57:40 2014 +0200 +++ b/src/Pure/Tools/plugin.ML Mon Oct 13 22:43:29 2014 +0200 @@ -54,7 +54,7 @@ fun define binding rhs thy = let - val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming); + val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy); val thy' = Data.put data' thy; in (name, thy') end; diff -r d2a7b443ceb2 -r 1891f17c6124 src/Pure/variable.ML --- a/src/Pure/variable.ML Mon Oct 13 21:57:40 2014 +0200 +++ b/src/Pure/variable.ML Mon Oct 13 22:43:29 2014 +0200 @@ -380,11 +380,11 @@ fun new_fixed ((x, x'), pos) ctxt = if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] else - let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in + let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming) in ctxt |> map_fixes (Name_Space.define context true (Binding.make (x', pos), x) #> snd #> - Name_Space.alias_table Name_Space.default_naming (Binding.make (x, pos)) x') + Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') |> declare_fixed x |> declare_constraints (Syntax.free x') end;