--- a/NEWS Thu Apr 09 18:46:16 2015 +0200
+++ b/NEWS Thu Apr 09 20:42:38 2015 +0200
@@ -7,17 +7,18 @@
*** General ***
* Local theory specification commands may have a 'private' or
-'restricted' modifier to limit name space accesses to the local scope,
+'qualified' modifier to restrict name space accesses to the local scope,
as provided by some "context begin ... end" block. For example:
context
begin
private definition ...
- private definition ...
private lemma ...
- lemma ...
+ qualified definition ...
+ qualified lemma ...
+
lemma ...
theorem ...
--- a/src/Doc/Isar_Ref/Spec.thy Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Apr 09 20:42:38 2015 +0200
@@ -115,7 +115,7 @@
@{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
@{keyword_def "private"} \\
- @{keyword_def "restricted"} \\
+ @{keyword_def "qualified"} \\
\end{matharray}
A local theory target is a specification context that is managed
@@ -162,16 +162,16 @@
(global) "end"} has a different meaning: it concludes the theory
itself (\secref{sec:begin-thy}).
- \item @{keyword "private"} or @{keyword "restricted"} may be given as
- modifiers before any local theory command. This limits name space accesses
- to the local scope, as determined by the enclosing @{command
+ \item @{keyword "private"} or @{keyword "qualified"} may be given as
+ modifiers before any local theory command. This restricts name space
+ accesses to the local scope, as determined by the enclosing @{command
"context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
scope, a @{keyword "private"} name is inaccessible, and a @{keyword
- "restricted"} name is only accessible with additional qualification.
+ "qualified"} name is only accessible with additional qualification.
Neither a global @{command theory} nor a @{command locale} target provides
a local scope by itself: an extra unnamed context is required to use
- @{keyword "private"} or @{keyword "restricted"} here.
+ @{keyword "private"} or @{keyword "qualified"} here.
\item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
theory command specifies an immediate target, e.g.\ ``@{command
--- a/src/FOL/FOL.thy Thu Apr 09 18:46:16 2015 +0200
+++ b/src/FOL/FOL.thy Thu Apr 09 20:42:38 2015 +0200
@@ -387,10 +387,10 @@
context
begin
-restricted definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
-restricted definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
-restricted definition "induct_equal(x, y) \<equiv> x = y"
-restricted definition "induct_conj(A, B) \<equiv> A \<and> B"
+qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
+qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
+qualified definition "induct_equal(x, y) \<equiv> x = y"
+qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
unfolding atomize_all induct_forall_def .
--- a/src/HOL/HOL.thy Thu Apr 09 18:46:16 2015 +0200
+++ b/src/HOL/HOL.thy Thu Apr 09 20:42:38 2015 +0200
@@ -1377,12 +1377,12 @@
context
begin
-restricted definition "induct_forall P \<equiv> \<forall>x. P x"
-restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
-restricted definition "induct_equal x y \<equiv> x = y"
-restricted definition "induct_conj A B \<equiv> A \<and> B"
-restricted definition "induct_true \<equiv> True"
-restricted definition "induct_false \<equiv> False"
+qualified definition "induct_forall P \<equiv> \<forall>x. P x"
+qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
+qualified definition "induct_equal x y \<equiv> x = y"
+qualified definition "induct_conj A B \<equiv> A \<and> B"
+qualified definition "induct_true \<equiv> True"
+qualified definition "induct_false \<equiv> False"
lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
by (unfold atomize_all induct_forall_def)
--- a/src/HOL/Library/AList.thy Thu Apr 09 18:46:16 2015 +0200
+++ b/src/HOL/Library/AList.thy Thu Apr 09 20:42:38 2015 +0200
@@ -20,7 +20,7 @@
subsection {* @{text update} and @{text updates} *}
-restricted primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
"update k v [] = [(k, v)]"
| "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
@@ -86,7 +86,7 @@
"x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
by (simp add: update_conv')
-restricted definition
+qualified definition
updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where "updates ks vs = fold (case_prod update) (zip ks vs)"
@@ -165,7 +165,7 @@
subsection {* @{text delete} *}
-restricted definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
lemma delete_simps [simp]:
@@ -217,7 +217,7 @@
subsection {* @{text restrict} *}
-restricted definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
lemma restr_simps [simp]:
@@ -301,7 +301,7 @@
subsection {* @{text clearjunk} *}
-restricted function clearjunk :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified function clearjunk :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
"clearjunk [] = []"
| "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
@@ -411,7 +411,7 @@
subsection {* @{text merge} *}
-restricted definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
lemma merge_simps [simp]:
@@ -479,7 +479,7 @@
subsection {* @{text compose} *}
-restricted function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
+qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
where
"compose [] ys = []"
| "compose (x # xs) ys =
@@ -644,7 +644,7 @@
subsection {* @{text map_entry} *}
-restricted fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
where
"map_entry k f [] = []"
| "map_entry k f (p # ps) =
--- a/src/Pure/General/binding.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/General/binding.ML Thu Apr 09 20:42:38 2015 +0200
@@ -30,9 +30,7 @@
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
- val private: scope -> binding -> binding
- val restricted: scope -> binding -> binding
- val limited_default: (bool * scope) option -> binding -> binding
+ val restricted_default: (bool * scope) option -> binding -> binding
val concealed: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
@@ -40,7 +38,7 @@
val bad: binding -> string
val check: binding -> unit
val name_spec: scope list -> (string * bool) list -> binding ->
- {limitation: bool option, concealed: bool, spec: (string * bool) list}
+ {restriction: bool option, concealed: bool, spec: (string * bool) list}
end;
structure Binding: BINDING =
@@ -48,7 +46,7 @@
(** representation **)
-(* scope of limited entries *)
+(* scope of restricted entries *)
datatype scope = Scope of serial;
@@ -58,19 +56,19 @@
(* binding *)
datatype binding = Binding of
- {limited: (bool * scope) option, (*entry is private (true) / restricted (false) to scope*)
- concealed: bool, (*entry is for foundational purposes -- please ignore*)
- prefix: (string * bool) list, (*system prefix*)
- qualifier: (string * bool) list, (*user qualifier*)
- name: bstring, (*base name*)
- pos: Position.T}; (*source position*)
+ {restricted: (bool * scope) option, (*entry is private (true) or qualified (false) wrt. scope*)
+ concealed: bool, (*entry is for foundational purposes -- please ignore*)
+ prefix: (string * bool) list, (*system prefix*)
+ qualifier: (string * bool) list, (*user qualifier*)
+ name: bstring, (*base name*)
+ pos: Position.T}; (*source position*)
-fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
- Binding {limited = limited, concealed = concealed, prefix = prefix,
+fun make_binding (restricted, concealed, prefix, qualifier, name, pos) =
+ Binding {restricted = restricted, concealed = concealed, prefix = prefix,
qualifier = qualifier, name = name, pos = pos};
-fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
- make_binding (f (limited, concealed, prefix, qualifier, name, pos));
+fun map_binding f (Binding {restricted, concealed, prefix, qualifier, name, pos}) =
+ make_binding (f (restricted, concealed, prefix, qualifier, name, pos));
fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
@@ -84,8 +82,8 @@
fun pos_of (Binding {pos, ...}) = pos;
fun set_pos pos =
- map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
- (limited, concealed, prefix, qualifier, name, pos));
+ map_binding (fn (restricted, concealed, prefix, qualifier, name, _) =>
+ (restricted, concealed, prefix, qualifier, name, pos));
fun name name = make (name, Position.none);
fun name_of (Binding {name, ...}) = name;
@@ -93,8 +91,8 @@
fun eq_name (b, b') = name_of b = name_of b';
fun map_name f =
- map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
- (limited, concealed, prefix, qualifier, f name, pos));
+ map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+ (restricted, concealed, prefix, qualifier, f name, pos));
val prefix_name = map_name o prefix;
val suffix_name = map_name o suffix;
@@ -107,13 +105,13 @@
fun qualify _ "" = I
| qualify mandatory qual =
- map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
- (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
+ map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+ (restricted, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
fun qualified mandatory name' =
- map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+ map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
- in (limited, concealed, prefix, qualifier', name', pos) end);
+ in (restricted, concealed, prefix, qualifier', name', pos) end);
fun qualified_name "" = empty
| qualified_name s =
@@ -126,8 +124,8 @@
fun prefix_of (Binding {prefix, ...}) = prefix;
fun map_prefix f =
- map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
- (limited, concealed, f prefix, qualifier, name, pos));
+ map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+ (restricted, concealed, f prefix, qualifier, name, pos));
fun prefix _ "" = I
| prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
@@ -135,20 +133,18 @@
(* visibility flags *)
-fun limited strict scope =
+fun restricted strict scope =
map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
(SOME (strict, scope), concealed, prefix, qualifier, name, pos));
-val private = limited true;
-val restricted = limited false;
-
-fun limited_default limited' =
- map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
- (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
+fun restricted_default restricted' =
+ map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+ (if is_some restricted then restricted else restricted',
+ concealed, prefix, qualifier, name, pos));
val concealed =
- map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
- (limited, true, prefix, qualifier, name, pos));
+ map_binding (fn (restricted, _, prefix, qualifier, name, pos) =>
+ (restricted, true, prefix, qualifier, name, pos));
(* print *)
@@ -181,11 +177,11 @@
fun name_spec scopes path binding =
let
- val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
+ val Binding {restricted, concealed, prefix, qualifier, name, ...} = binding;
val _ = Long_Name.is_qualified name andalso error (bad binding);
- val limitation =
- (case limited of
+ val restriction =
+ (case restricted of
NONE => NONE
| SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
@@ -196,7 +192,7 @@
val _ =
exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
andalso error (bad binding);
- in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
+ in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
end;
--- a/src/Pure/General/name_space.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/General/name_space.ML Thu Apr 09 20:42:38 2015 +0200
@@ -35,11 +35,11 @@
val get_scopes: naming -> Binding.scope list
val get_scope: naming -> Binding.scope option
val new_scope: naming -> Binding.scope * naming
- val limited: bool -> Position.T -> naming -> naming
+ val restricted: bool -> Position.T -> naming -> naming
val private_scope: Binding.scope -> naming -> naming
val private: Position.T -> naming -> naming
- val restricted_scope: Binding.scope -> naming -> naming
- val restricted: Position.T -> naming -> naming
+ val qualified_scope: Binding.scope -> naming -> naming
+ val qualified: Position.T -> naming -> naming
val concealed: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
@@ -300,21 +300,21 @@
datatype naming = Naming of
{scopes: Binding.scope list,
- limited: (bool * Binding.scope) option,
+ restricted: (bool * Binding.scope) option,
concealed: bool,
group: serial option,
theory_name: string,
path: (string * bool) list};
-fun make_naming (scopes, limited, concealed, group, theory_name, path) =
- Naming {scopes = scopes, limited = limited, concealed = concealed,
+fun make_naming (scopes, restricted, concealed, group, theory_name, path) =
+ Naming {scopes = scopes, restricted = restricted, concealed = concealed,
group = group, theory_name = theory_name, path = path};
-fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
- make_naming (f (scopes, limited, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, restricted, concealed, group, theory_name, path}) =
+ make_naming (f (scopes, restricted, concealed, group, theory_name, path));
-(* scope and access limitation *)
+(* scope and access restriction *)
fun get_scopes (Naming {scopes, ...}) = scopes;
val get_scope = try hd o get_scopes;
@@ -323,38 +323,38 @@
let
val scope = Binding.new_scope ();
val naming' =
- naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
- (scope :: scopes, limited, concealed, group, theory_name, path));
+ naming |> map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
+ (scope :: scopes, restricted, concealed, group, theory_name, path));
in (scope, naming') end;
-fun limited_scope strict scope =
+fun restricted_scope strict scope =
map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
(scopes, SOME (strict, scope), concealed, group, theory_name, path));
-fun limited strict pos naming =
+fun restricted strict pos naming =
(case get_scope naming of
- SOME scope => limited_scope strict scope naming
- | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
+ SOME scope => restricted_scope strict scope naming
+ | NONE => error ("Missing local scope -- cannot restrict name space accesses" ^ Position.here pos));
-val private_scope = limited_scope true;
-val private = limited true;
+val private_scope = restricted_scope true;
+val private = restricted true;
-val restricted_scope = limited_scope false;
-val restricted = limited false;
+val qualified_scope = restricted_scope false;
+val qualified = restricted false;
-val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
- (scopes, limited, true, group, theory_name, path));
+val concealed = map_naming (fn (scopes, restricted, _, group, theory_name, path) =>
+ (scopes, restricted, true, group, theory_name, path));
(* additional structural info *)
-fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
- (scopes, limited, concealed, group, theory_name, path));
+fun set_theory_name theory_name = map_naming (fn (scopes, restricted, concealed, group, _, path) =>
+ (scopes, restricted, concealed, group, theory_name, path));
fun get_group (Naming {group, ...}) = group;
-fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
- (scopes, limited, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, restricted, concealed, _, theory_name, path) =>
+ (scopes, restricted, concealed, group, theory_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
@@ -364,8 +364,8 @@
fun get_path (Naming {path, ...}) = path;
-fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
- (scopes, limited, concealed, group, theory_name, f path));
+fun map_path f = map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
+ (scopes, restricted, concealed, group, theory_name, f path));
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
val root_path = map_path (fn _ => []);
@@ -381,14 +381,14 @@
(* transform *)
-fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
- (case limited' of
- SOME (strict, scope) => limited_scope strict scope
+fun transform_naming (Naming {restricted = restricted', concealed = concealed', ...}) =
+ (case restricted' of
+ SOME (strict, scope) => restricted_scope strict scope
| NONE => I) #>
concealed' ? concealed;
-fun transform_binding (Naming {limited, concealed, ...}) =
- Binding.limited_default limited #>
+fun transform_binding (Naming {restricted, concealed, ...}) =
+ Binding.restricted_default restricted #>
concealed ? Binding.concealed;
@@ -416,10 +416,10 @@
fun accesses naming binding =
(case name_spec naming binding of
- {limitation = SOME true, ...} => ([], [])
- | {limitation, spec, ...} =>
+ {restriction = SOME true, ...} => ([], [])
+ | {restriction, spec, ...} =>
let
- val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
+ val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
val sfxs = restrict (mandatory_suffixes spec);
val pfxs = restrict (mandatory_prefixes spec);
in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
--- a/src/Pure/Isar/outer_syntax.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Apr 09 20:42:38 2015 +0200
@@ -163,7 +163,7 @@
local
val before_command =
- Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
+ Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
fun parse_command thy =
Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
--- a/src/Pure/Isar/parse.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/parse.ML Thu Apr 09 20:42:38 2015 +0200
@@ -104,7 +104,7 @@
val propp: (string * string list) parser
val termp: (string * string list) parser
val private: Position.T parser
- val restricted: Position.T parser
+ val qualified: Position.T parser
val target: (xstring * Position.T) parser
val opt_target: (xstring * Position.T) option parser
val args: Token.T list parser
@@ -401,7 +401,7 @@
(* target information *)
val private = position ($$$ "private") >> #2;
-val restricted = position ($$$ "restricted") >> #2;
+val qualified = position ($$$ "qualified") >> #2;
val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
val opt_target = Scan.option target;
--- a/src/Pure/Isar/proof_context.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 09 20:42:38 2015 +0200
@@ -38,8 +38,8 @@
val new_scope: Proof.context -> Binding.scope * Proof.context
val private_scope: Binding.scope -> Proof.context -> Proof.context
val private: Position.T -> Proof.context -> Proof.context
- val restricted_scope: Binding.scope -> Proof.context -> Proof.context
- val restricted: Position.T -> Proof.context -> Proof.context
+ val qualified_scope: Binding.scope -> Proof.context -> Proof.context
+ val qualified: Position.T -> Proof.context -> Proof.context
val concealed: Proof.context -> Proof.context
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
@@ -321,8 +321,8 @@
val private_scope = map_naming o Name_Space.private_scope;
val private = map_naming o Name_Space.private;
-val restricted_scope = map_naming o Name_Space.restricted_scope;
-val restricted = map_naming o Name_Space.restricted;
+val qualified_scope = map_naming o Name_Space.qualified_scope;
+val qualified = map_naming o Name_Space.qualified;
val concealed = map_naming Name_Space.concealed;
--- a/src/Pure/Isar/token.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/token.ML Thu Apr 09 20:42:38 2015 +0200
@@ -247,7 +247,7 @@
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
| keyword_with _ _ = false;
-val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
+val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified");
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
| ident_with _ _ = false;
--- a/src/Pure/Isar/token.scala Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/token.scala Thu Apr 09 20:42:38 2015 +0200
@@ -260,7 +260,7 @@
def is_end: Boolean = is_command && source == "end"
def is_command_modifier: Boolean =
- is_keyword && (source == "private" || source == "restricted")
+ is_keyword && (source == "private" || source == "qualified")
def is_begin_block: Boolean = is_command && source == "{"
def is_end_block: Boolean = is_command && source == "}"
--- a/src/Pure/Isar/toplevel.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Apr 09 20:42:38 2015 +0200
@@ -412,15 +412,16 @@
| NONE => raise UNDEF)
| _ => raise UNDEF));
-val limited_context =
- fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
+fun restricted_context (SOME (strict, scope)) =
+ Proof_Context.map_naming (Name_Space.restricted strict scope)
+ | restricted_context NONE = I;
-fun local_theory' limited target f = present_transaction (fn int =>
+fun local_theory' restricted target f = present_transaction (fn int =>
(fn Theory (gthy, _) =>
let
val (finish, lthy) = Named_Target.switch target gthy;
val lthy' = lthy
- |> limited_context limited
+ |> restricted_context restricted
|> Local_Theory.new_group
|> f int
|> Local_Theory.reset_group;
@@ -428,7 +429,7 @@
| _ => raise UNDEF))
(K ());
-fun local_theory limited target f = local_theory' limited target (K f);
+fun local_theory restricted target f = local_theory' restricted target (K f);
fun present_local_theory target = present_transaction (fn int =>
(fn Theory (gthy, _) =>
@@ -473,18 +474,18 @@
in
-fun local_theory_to_proof' limited target f = begin_proof
+fun local_theory_to_proof' restricted target f = begin_proof
(fn int => fn gthy =>
let
val (finish, lthy) = Named_Target.switch target gthy;
val prf = lthy
- |> limited_context limited
+ |> restricted_context restricted
|> Local_Theory.new_group
|> f int;
in (finish o Local_Theory.reset_group, prf) end);
-fun local_theory_to_proof limited target f =
- local_theory_to_proof' limited target (K f);
+fun local_theory_to_proof restricted target f =
+ local_theory_to_proof' restricted target (K f);
fun theory_to_proof f = begin_proof
(fn _ => fn gthy =>
--- a/src/Pure/Pure.thy Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Pure.thy Thu Apr 09 20:42:38 2015 +0200
@@ -11,7 +11,7 @@
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
- "overloaded" "pervasive" "private" "restricted" "shows"
+ "overloaded" "pervasive" "private" "qualified" "shows"
"structure" "unchecked" "where" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
--- a/src/Pure/sign.ML Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/sign.ML Thu Apr 09 20:42:38 2015 +0200
@@ -113,6 +113,8 @@
val local_path: theory -> theory
val private_scope: Binding.scope -> theory -> theory
val private: Position.T -> theory -> theory
+ val qualified_scope: Binding.scope -> theory -> theory
+ val qualified: Position.T -> theory -> theory
val concealed: theory -> theory
val hide_class: bool -> string -> theory -> theory
val hide_type: bool -> string -> theory -> theory
@@ -525,8 +527,8 @@
val private_scope = map_naming o Name_Space.private_scope;
val private = map_naming o Name_Space.private;
-val restricted_scope = map_naming o Name_Space.restricted_scope;
-val restricted = map_naming o Name_Space.restricted;
+val qualified_scope = map_naming o Name_Space.qualified_scope;
+val qualified = map_naming o Name_Space.qualified;
val concealed = map_naming Name_Space.concealed;