# HG changeset patch
# User wenzelm
# Date 1258465855 -3600
# Node ID 5ee13e0428d2f1f1452d172ede8ccdd433186388
# Parent  14d0dadd9517a5ec82496aa1a7aaa512a206a8c3
uniform new_group/reset_group;
tuned signature;

diff -r 14d0dadd9517 -r 5ee13e0428d2 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Nov 17 14:48:21 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Nov 17 14:50:55 2009 +0100
@@ -34,8 +34,11 @@
   type naming
   val default_naming: naming
   val conceal: naming -> naming
-  val set_group: serial -> naming -> naming
+  val get_group: naming -> serial option
+  val set_group: serial option -> naming -> naming
   val set_theory_name: string -> naming -> naming
+  val new_group: naming -> naming
+  val reset_group: naming -> naming
   val add_path: string -> naming -> naming
   val root_path: naming -> naming
   val parent_path: naming -> naming
@@ -241,12 +244,18 @@
 val conceal = map_naming (fn (_, group, theory_name, path) =>
   (true, group, theory_name, path));
 
-fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
-  (conceal, SOME group, theory_name, path));
-
 fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
   (conceal, group, theory_name, path));
 
+
+fun get_group (Naming {group, ...}) = group;
+
+fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
+  (conceal, group, theory_name, path));
+
+fun new_group naming = set_group (SOME (serial ())) naming;
+val reset_group = set_group NONE;
+
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
diff -r 14d0dadd9517 -r 5ee13e0428d2 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:48:21 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:50:55 2009 +0100
@@ -14,7 +14,8 @@
   val full_name: local_theory -> binding -> string
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
   val conceal: local_theory -> local_theory
-  val set_group: serial -> local_theory -> local_theory
+  val new_group: local_theory -> local_theory
+  val reset_group: local_theory -> local_theory
   val restore_naming: local_theory -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -42,7 +43,7 @@
   val term_syntax: bool -> declaration -> local_theory -> local_theory
   val declaration: bool -> declaration -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val init: string -> operations -> Proof.context -> local_theory
+  val init: serial option -> string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val reinit: local_theory -> local_theory
   val exit: local_theory -> Proof.context
@@ -114,7 +115,8 @@
   (f naming, theory_prefix, operations, target));
 
 val conceal = map_naming Name_Space.conceal;
-val set_group = map_naming o Name_Space.set_group;
+val new_group = map_naming Name_Space.new_group;
+val reset_group = map_naming Name_Space.reset_group;
 
 val restore_naming = map_naming o K o naming_of;
 
@@ -203,9 +205,10 @@
 
 (* init *)
 
-fun init theory_prefix operations target =
+fun init group theory_prefix operations target =
   let val naming =
     Sign.naming_of (ProofContext.theory_of target)
+    |> Name_Space.set_group group
     |> Name_Space.mandatory_path theory_prefix;
   in
     target |> Data.map
@@ -215,8 +218,8 @@
   end;
 
 fun restore lthy =
-  let val {theory_prefix, operations, target, ...} = get_lthy lthy
-  in init theory_prefix operations target end;
+  let val {naming, theory_prefix, operations, target} = get_lthy lthy
+  in init (Name_Space.get_group naming) theory_prefix operations target end;
 
 val reinit = checkpoint o operation #reinit;
 
diff -r 14d0dadd9517 -r 5ee13e0428d2 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Nov 17 14:48:21 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Nov 17 14:50:55 2009 +0100
@@ -324,7 +324,7 @@
 
 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   Data.put ta #>
-  Local_Theory.init (Long_Name.base_name target)
+  Local_Theory.init NONE (Long_Name.base_name target)
    {pretty = pretty ta,
     abbrev = abbrev ta,
     define = define ta,
diff -r 14d0dadd9517 -r 5ee13e0428d2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 17 14:48:21 2009 +0100
+++ b/src/Pure/sign.ML	Tue Nov 17 14:50:55 2009 +0100
@@ -121,6 +121,8 @@
   val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   val del_trrules_i: ast Syntax.trrule list -> theory -> theory
+  val new_group: theory -> theory
+  val reset_group: theory -> theory
   val add_path: string -> theory -> theory
   val root_path: theory -> theory
   val parent_path: theory -> theory
@@ -610,6 +612,9 @@
 
 (* naming *)
 
+val new_group = map_naming Name_Space.new_group;
+val reset_group = map_naming Name_Space.reset_group;
+
 val add_path = map_naming o Name_Space.add_path;
 val root_path = map_naming Name_Space.root_path;
 val parent_path = map_naming Name_Space.parent_path;