uniform new_group/reset_group;
authorwenzelm
Tue Nov 17 14:50:55 2009 +0100 (2009-11-17)
changeset 337245ee13e0428d2
parent 33723 14d0dadd9517
child 33725 a8481da77270
uniform new_group/reset_group;
tuned signature;
src/Pure/General/name_space.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/theory_target.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Nov 17 14:48:21 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Nov 17 14:50:55 2009 +0100
     1.3 @@ -34,8 +34,11 @@
     1.4    type naming
     1.5    val default_naming: naming
     1.6    val conceal: naming -> naming
     1.7 -  val set_group: serial -> naming -> naming
     1.8 +  val get_group: naming -> serial option
     1.9 +  val set_group: serial option -> naming -> naming
    1.10    val set_theory_name: string -> naming -> naming
    1.11 +  val new_group: naming -> naming
    1.12 +  val reset_group: naming -> naming
    1.13    val add_path: string -> naming -> naming
    1.14    val root_path: naming -> naming
    1.15    val parent_path: naming -> naming
    1.16 @@ -241,12 +244,18 @@
    1.17  val conceal = map_naming (fn (_, group, theory_name, path) =>
    1.18    (true, group, theory_name, path));
    1.19  
    1.20 -fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
    1.21 -  (conceal, SOME group, theory_name, path));
    1.22 -
    1.23  fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
    1.24    (conceal, group, theory_name, path));
    1.25  
    1.26 +
    1.27 +fun get_group (Naming {group, ...}) = group;
    1.28 +
    1.29 +fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
    1.30 +  (conceal, group, theory_name, path));
    1.31 +
    1.32 +fun new_group naming = set_group (SOME (serial ())) naming;
    1.33 +val reset_group = set_group NONE;
    1.34 +
    1.35  fun add_path elems = map_path (fn path => path @ [(elems, false)]);
    1.36  val root_path = map_path (fn _ => []);
    1.37  val parent_path = map_path (perhaps (try (#1 o split_last)));
     2.1 --- a/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:48:21 2009 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:50:55 2009 +0100
     2.3 @@ -14,7 +14,8 @@
     2.4    val full_name: local_theory -> binding -> string
     2.5    val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
     2.6    val conceal: local_theory -> local_theory
     2.7 -  val set_group: serial -> local_theory -> local_theory
     2.8 +  val new_group: local_theory -> local_theory
     2.9 +  val reset_group: local_theory -> local_theory
    2.10    val restore_naming: local_theory -> local_theory -> local_theory
    2.11    val target_of: local_theory -> Proof.context
    2.12    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    2.13 @@ -42,7 +43,7 @@
    2.14    val term_syntax: bool -> declaration -> local_theory -> local_theory
    2.15    val declaration: bool -> declaration -> local_theory -> local_theory
    2.16    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.17 -  val init: string -> operations -> Proof.context -> local_theory
    2.18 +  val init: serial option -> string -> operations -> Proof.context -> local_theory
    2.19    val restore: local_theory -> local_theory
    2.20    val reinit: local_theory -> local_theory
    2.21    val exit: local_theory -> Proof.context
    2.22 @@ -114,7 +115,8 @@
    2.23    (f naming, theory_prefix, operations, target));
    2.24  
    2.25  val conceal = map_naming Name_Space.conceal;
    2.26 -val set_group = map_naming o Name_Space.set_group;
    2.27 +val new_group = map_naming Name_Space.new_group;
    2.28 +val reset_group = map_naming Name_Space.reset_group;
    2.29  
    2.30  val restore_naming = map_naming o K o naming_of;
    2.31  
    2.32 @@ -203,9 +205,10 @@
    2.33  
    2.34  (* init *)
    2.35  
    2.36 -fun init theory_prefix operations target =
    2.37 +fun init group theory_prefix operations target =
    2.38    let val naming =
    2.39      Sign.naming_of (ProofContext.theory_of target)
    2.40 +    |> Name_Space.set_group group
    2.41      |> Name_Space.mandatory_path theory_prefix;
    2.42    in
    2.43      target |> Data.map
    2.44 @@ -215,8 +218,8 @@
    2.45    end;
    2.46  
    2.47  fun restore lthy =
    2.48 -  let val {theory_prefix, operations, target, ...} = get_lthy lthy
    2.49 -  in init theory_prefix operations target end;
    2.50 +  let val {naming, theory_prefix, operations, target} = get_lthy lthy
    2.51 +  in init (Name_Space.get_group naming) theory_prefix operations target end;
    2.52  
    2.53  val reinit = checkpoint o operation #reinit;
    2.54  
     3.1 --- a/src/Pure/Isar/theory_target.ML	Tue Nov 17 14:48:21 2009 +0100
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Nov 17 14:50:55 2009 +0100
     3.3 @@ -324,7 +324,7 @@
     3.4  
     3.5  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
     3.6    Data.put ta #>
     3.7 -  Local_Theory.init (Long_Name.base_name target)
     3.8 +  Local_Theory.init NONE (Long_Name.base_name target)
     3.9     {pretty = pretty ta,
    3.10      abbrev = abbrev ta,
    3.11      define = define ta,
     4.1 --- a/src/Pure/sign.ML	Tue Nov 17 14:48:21 2009 +0100
     4.2 +++ b/src/Pure/sign.ML	Tue Nov 17 14:50:55 2009 +0100
     4.3 @@ -121,6 +121,8 @@
     4.4    val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
     4.5    val add_trrules_i: ast Syntax.trrule list -> theory -> theory
     4.6    val del_trrules_i: ast Syntax.trrule list -> theory -> theory
     4.7 +  val new_group: theory -> theory
     4.8 +  val reset_group: theory -> theory
     4.9    val add_path: string -> theory -> theory
    4.10    val root_path: theory -> theory
    4.11    val parent_path: theory -> theory
    4.12 @@ -610,6 +612,9 @@
    4.13  
    4.14  (* naming *)
    4.15  
    4.16 +val new_group = map_naming Name_Space.new_group;
    4.17 +val reset_group = map_naming Name_Space.reset_group;
    4.18 +
    4.19  val add_path = map_naming o Name_Space.add_path;
    4.20  val root_path = map_naming Name_Space.root_path;
    4.21  val parent_path = map_naming Name_Space.parent_path;