# HG changeset patch # User wenzelm # Date 1256494662 -3600 # Node ID 50c4debfd5ae7a209b2c3176f6afd161a75b99dc # Parent b8fd9b6bba7c16f071aeb3c69b8e74ca3d871ba2 more direct access to naming; tuned signature; diff -r b8fd9b6bba7c -r 50c4debfd5ae src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sun Oct 25 19:14:46 2009 +0100 +++ b/src/Pure/Isar/proof.ML Sun Oct 25 19:17:42 2009 +0100 @@ -162,7 +162,8 @@ make_node (f (context, facts, mode, goal)); val init_context = - ProofContext.set_stmt true #> ProofContext.reset_naming; + ProofContext.set_stmt true #> + ProofContext.map_naming (K ProofContext.local_naming); fun init ctxt = State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); diff -r b8fd9b6bba7c -r 50c4debfd5ae src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Oct 25 19:14:46 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Sun Oct 25 19:17:42 2009 +0100 @@ -21,7 +21,10 @@ val restore_mode: Proof.context -> Proof.context -> Proof.context val abbrev_mode: Proof.context -> bool val set_stmt: bool -> Proof.context -> Proof.context + val local_naming: Name_Space.naming + val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context val naming_of: Proof.context -> Name_Space.naming + val restore_naming: Proof.context -> Proof.context -> Proof.context val full_name: Proof.context -> binding -> string val consts_of: Proof.context -> Consts.T val const_syntax_name: Proof.context -> string -> string @@ -92,11 +95,6 @@ val get_fact_single: Proof.context -> Facts.ref -> thm val get_thms: Proof.context -> xstring -> thm list val get_thm: Proof.context -> xstring -> thm - val add_path: string -> Proof.context -> Proof.context - val mandatory_path: string -> Proof.context -> Proof.context - val conceal: Proof.context -> Proof.context - val restore_naming: Proof.context -> Proof.context -> Proof.context - val reset_naming: Proof.context -> Proof.context val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context @@ -232,6 +230,7 @@ map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); val naming_of = #naming o rep_context; +val restore_naming = map_naming o K o naming_of val full_name = Name_Space.full_name o naming_of; val syntax_of = #syntax o rep_context; @@ -923,15 +922,6 @@ end; -(* name space operations *) - -val add_path = map_naming o Name_Space.add_path; -val mandatory_path = map_naming o Name_Space.mandatory_path; -val conceal = map_naming Name_Space.conceal; -val restore_naming = map_naming o K o naming_of; -val reset_naming = map_naming (K local_naming); - - (* facts *) local diff -r b8fd9b6bba7c -r 50c4debfd5ae src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Oct 25 19:14:46 2009 +0100 +++ b/src/Pure/sign.ML Sun Oct 25 19:17:42 2009 +0100 @@ -12,6 +12,7 @@ syn: Syntax.syntax, tsig: Type.tsig, consts: Consts.T} + val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory val naming_of: theory -> Name_Space.naming val full_name: theory -> binding -> string val full_name_path: theory -> string -> binding -> string @@ -125,7 +126,6 @@ val parent_path: theory -> theory val mandatory_path: string -> theory -> theory val local_path: theory -> theory - val conceal: theory -> theory val restore_naming: theory -> theory -> theory val hide_class: bool -> string -> theory -> theory val hide_type: bool -> string -> theory -> theory @@ -619,8 +619,6 @@ fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); -val conceal = map_naming Name_Space.conceal; - val restore_naming = map_naming o K o naming_of;