new Binding module

--- a/src/HOL/Tools/inductive_package.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -638,8 +638,8 @@
     (* add definiton of recursive predicates to theory *)
 
     val rec_name =
-      if Name.is_nothing alt_name then
-        Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+      if Binding.is_nothing alt_name then
+        Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
       else alt_name;
 
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>

--- a/src/HOL/Tools/inductive_set_package.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -499,8 +499,8 @@
 
     (* convert theorems to set notation *)
     val rec_name =
-      if Name.is_nothing alt_name then
-        Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+      if Binding.is_nothing alt_name then
+        Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
       else alt_name;
     val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);

--- a/src/Pure/General/ROOT.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/General/ROOT.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -27,6 +27,7 @@
 use "ord_list.ML";
 use "balanced_tree.ML";
 use "graph.ML";
+use "binding.ML";
 use "name_space.ML";
 use "lazy.ML";
 use "path.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/binding.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -0,0 +1,75 @@
+(*  Title:      Pure/General/binding.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Structured name bindings.
+*)
+
+signature BASIC_BINDING =
+sig
+  val long_names: bool ref
+  val short_names: bool ref
+  val unique_names: bool ref
+end;
+
+signature BINDING =
+sig
+  include BASIC_BINDING
+  type T
+  val binding_pos: string * Position.T -> T
+  val binding: string -> T
+  val no_binding: T
+  val dest_binding: T -> (string * bool) list * string
+  val is_nothing: T -> bool
+  val pos_of: T -> Position.T
+ 
+  val map_binding: ((string * bool) list * string -> (string * bool) list * string)
+    -> T -> T
+  val add_prefix: bool -> string -> T -> T
+  val map_prefix: ((string * bool) list -> T -> T) -> T -> T
+  val display: T -> string
+end
+
+structure Binding : BINDING =
+struct
+
+(** global flags **)
+
+val long_names = ref false;
+val short_names = ref false;
+val unique_names = ref true;
+
+
+(** binding representation **)
+
+datatype T = Binding of ((string * bool) list * string) * Position.T;
+  (* (prefix components (with mandatory flag), base name, position) *)
+
+fun binding_pos (name, pos) = Binding (([], name), pos);
+fun binding name = binding_pos (name, Position.none);
+val no_binding = binding "";
+
+fun pos_of (Binding (_, pos)) = pos;
+fun dest_binding (Binding (prefix_name, _)) = prefix_name;
+
+fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
+
+fun is_nothing (Binding ((_, name), _)) = name = "";
+
+fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
+  else (map_binding o apfst) (cons (prfx, sticky)) b;
+
+fun map_prefix f (Binding ((prefix, name), pos)) =
+  f prefix (binding_pos (name, pos));
+
+fun display (Binding ((prefix, name), _)) =
+  let
+    fun mk_prefix (prfx, true) = prfx
+      | mk_prefix (prfx, false) = enclose "(" ")" prfx
+  in if not (! long_names) orelse null prefix orelse name = "" then name
+    else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
+  end;
+
+end;
+
+structure Basic_Binding : BASIC_BINDING = Binding;
+open Basic_Binding;

--- a/src/Pure/General/name_space.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/General/name_space.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/name_space.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Generic name spaces with declared and hidden entries.  Unknown names
@@ -9,29 +8,9 @@
 type bstring = string;    (*names to be bound*)
 type xstring = string;    (*external names*)
 
-signature BASIC_NAME_SPACE =
-sig
-  val long_names: bool ref
-  val short_names: bool ref
-  val unique_names: bool ref
-end;
-
-signature NAME_BINDING =
-sig
-  type binding
-  val binding_pos: string * Position.T -> binding
-  val binding: string -> binding
-  val no_binding: binding
-  val dest_binding: binding -> (string * bool) list * string
-  val is_nothing: binding -> bool
-  val pos_of: binding -> Position.T
-  val map_binding: ((string * bool) list * string -> (string * bool) list * string)
-    -> binding -> binding
-end
-
 signature NAME_SPACE =
 sig
-  include BASIC_NAME_SPACE
+  include BASIC_BINDING
   val hidden: string -> string
   val is_hidden: string -> bool
   val separator: string                 (*single char*)
@@ -60,14 +39,13 @@
   val no_base_names: naming -> naming
   val qualified_names: naming -> naming
   val sticky_prefix: string -> naming -> naming
-  include NAME_BINDING
-  val full_binding: naming -> binding -> string
-  val declare_binding: naming -> binding -> T -> string * T
+  val full_binding: naming -> Binding.T -> string
+  val declare_binding: naming -> Binding.T -> T -> string * T
   type 'a table = T * 'a Symtab.table
   val empty_table: 'a table
-  val table_declare: naming -> binding * 'a
+  val table_declare: naming -> Binding.T * 'a
     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
-  val table_declare_permissive: naming -> binding * 'a
+  val table_declare_permissive: naming -> Binding.T * 'a
     -> 'a table -> string * 'a table
   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
@@ -78,6 +56,9 @@
 structure NameSpace: NAME_SPACE =
 struct
 
+open Basic_Binding;
+
+
 (** long identifiers **)
 
 fun hidden name = "??." ^ name;
@@ -170,10 +151,6 @@
 
 fun intern space xname = #1 (lookup space xname);
 
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
-
 fun extern space name =
   let
     fun valid unique xname =
@@ -241,23 +218,6 @@
 
 
 
-(** generic name bindings **)
-
-datatype binding = Binding of ((string * bool) list * string) * Position.T;
-
-fun binding_pos (name, pos) = Binding (([], name), pos);
-fun binding name = binding_pos (name, Position.none);
-val no_binding = binding "";
-
-fun pos_of (Binding (_, pos)) = pos;
-fun dest_binding (Binding (prefix_name, _)) = prefix_name;
-
-fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
-
-fun is_nothing (Binding ((_, name), _)) = name = "";
-
-
-
 (** naming contexts **)
 
 (* datatype naming *)
@@ -321,8 +281,9 @@
       val (accs, accs') = pairself (map implode_name) (accesses naming names);
     in space |> fold (add_name name) accs |> put_accesses name accs' end;
 
-fun declare_binding bnaming (Binding ((prefix, bname), _)) =
+fun declare_binding bnaming b =
   let
+    val (prefix, bname) = Binding.dest_binding b;
     val naming = apply_prefix prefix bnaming;
     val name = full naming bname;
   in declare naming name #> pair name end;
@@ -343,8 +304,9 @@
 fun table_declare naming = gen_table_declare Symtab.update_new naming;
 fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
 
-fun full_binding naming (Binding ((prefix, bname), _)) =
-  full (apply_prefix prefix naming) bname;
+fun full_binding naming b =
+  let val (prefix, bname) = Binding.dest_binding b
+  in full (apply_prefix prefix naming) bname end;
 
 fun extend_table naming bentries (space, tab) =
   let val entries = map (apfst (full naming)) bentries
@@ -366,6 +328,3 @@
 val explode = explode_name;
 
 end;
-
-structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
-open BasicNameSpace;

--- a/src/Pure/Isar/args.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/args.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -171,7 +171,7 @@
 val name_source_position = named >> T.source_position_of;
 
 val name = named >> T.content_of;
-val binding = P.position name >> Name.binding_pos;
+val binding = P.position name >> Binding.binding_pos;
 val alt_name = alt_string >> T.content_of;
 val symbol = symbolic >> T.content_of;
 val liberal_name = symbol || name;

--- a/src/Pure/Isar/class.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/class.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -78,7 +78,7 @@
 val class_prefix = Logic.const_of_class o Sign.base_name;
 
 fun class_name_morphism class =
-  Name.map_prefix (K (Name.add_prefix false (class_prefix class)));
+  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
 
 fun activate_class_morphism thy class inst morphism =
   Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;

--- a/src/Pure/Isar/locale.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -947,8 +947,8 @@
         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
         val (lprfx, pprfx) = param_prefix name params;
-        val add_prefices = pprfx <> "" ? Name.add_prefix false pprfx
-          #> Name.add_prefix false lprfx;
+        val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx
+          #> Binding.add_prefix false lprfx;
         val elem_morphism =
           Element.rename_morphism ren $>
           Morphism.name_morphism add_prefices $>
@@ -1634,10 +1634,10 @@
 
 fun name_morph phi_name (lprfx, pprfx) b =
   b
-  |> (if not (Name.is_nothing b) andalso pprfx <> ""
-        then Name.add_prefix false pprfx else I)
-  |> (if not (Name.is_nothing b)
-        then Name.add_prefix false lprfx else I)
+  |> (if not (Binding.is_nothing b) andalso pprfx <> ""
+        then Binding.add_prefix false pprfx else I)
+  |> (if not (Binding.is_nothing b)
+        then Binding.add_prefix false lprfx else I)
   |> phi_name;
 
 fun inst_morph thy phi_name param_prfx insts prems eqns export =
@@ -2442,11 +2442,11 @@
   end;
 
 fun standard_name_morph interp_prfx b =
-  if Name.is_nothing b then b
-  else Name.map_prefix (fn ((lprfx, _) :: pprfx) =>
-    fold (Name.add_prefix false o fst) pprfx
-    #> interp_prfx <> "" ? Name.add_prefix true interp_prfx
-    #> Name.add_prefix false lprfx
+  if Binding.is_nothing b then b
+  else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
+    fold (Binding.add_prefix false o fst) pprfx
+    #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
+    #> Binding.add_prefix false lprfx
   ) b;
 
 in

--- a/src/Pure/Isar/outer_parse.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -228,7 +228,7 @@
 (* names and text *)
 
 val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Name.binding_pos;
+val binding = position name >> Binding.binding_pos;
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 val path = group "file name/path specification" name >> Path.explode;

--- a/src/Pure/Isar/proof_context.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -971,7 +971,7 @@
 
 fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   let
-    val pos = Name.pos_of b;
+    val pos = Binding.pos_of b;
     val name = full_binding ctxt b;
     val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
 
@@ -1128,7 +1128,7 @@
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of b));
+      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
 in

--- a/src/Pure/Isar/specification.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -190,7 +190,7 @@
             val y = Name.name_of b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
-                Position.str_of (Name.pos_of b));
+                Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
         (var, ((Name.map_name (suffix "_raw") name, []), rhs));
@@ -223,7 +223,7 @@
             val y = Name.name_of b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
-                Position.str_of (Name.pos_of b));
+                Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val lthy' = lthy
       |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
@@ -348,7 +348,7 @@
         lthy
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
-          if Name.is_nothing name andalso null atts then
+          if Binding.is_nothing name andalso null atts then
             (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
           else
             let

--- a/src/Pure/Isar/theory_target.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -201,7 +201,7 @@
     val arg = (b', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val (prefix', _) = Name.dest_binding b';
+    val (prefix', _) = Binding.dest_binding b';
     val class_global = Name.name_of b = Name.name_of b'
       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class.class_prefix target;

--- a/src/Pure/facts.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/facts.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -192,7 +192,7 @@
 
 fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   let
-    val (name, facts') = if Name.is_nothing b then ("", facts)
+    val (name, facts') = if Binding.is_nothing b then ("", facts)
       else let
         val (space, tab) = facts;
         val (name, space') = NameSpace.declare_binding naming b space;

--- a/src/Pure/name.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/name.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -29,20 +29,16 @@
   val variant_list: string list -> string list -> string list
   val variant: string list -> string -> string
 
-  include NAME_BINDING
-  val add_prefix: bool -> string -> binding -> binding
-  val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
-  val name_of: binding -> string (*FIMXE legacy*)
-  val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
-  val qualified: string -> binding -> binding (*FIMXE legacy*)
-  val display: binding -> string
+  include BINDING
+  type binding = Binding.T
+  val name_of: Binding.T -> string (*FIMXE legacy*)
+  val map_name: (string -> string) -> Binding.T -> Binding.T (*FIMXE legacy*)
+  val qualified: string -> Binding.T -> Binding.T (*FIMXE legacy*)
 end;
 
 structure Name: NAME =
 struct
 
-open NameSpace;
-
 (** common defaults **)
 
 val uu = "uu";
@@ -152,27 +148,13 @@
 
 (** generic name bindings **)
 
-fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
-  else (map_binding o apfst) (cons (prfx, sticky)) b;
+open Binding;
+
+type binding = Binding.T;
 
 val prefix_of = fst o dest_binding;
 val name_of = snd o dest_binding;
 val map_name = map_binding o apsnd;
 val qualified = map_name o NameSpace.qualified;
 
-fun map_prefix f b =
-  let
-    val (prefix, name) = dest_binding b;
-    val pos = pos_of b;
-  in f prefix (binding_pos (name, pos)) end;
-
-fun display b =
-  let
-    val (prefix, name) = dest_binding b
-    fun mk_prefix (prfx, true) = prfx
-      | mk_prefix (prfx, false) = enclose "(" ")" prfx
-  in if not (! NameSpace.long_names) orelse null prefix orelse name = "" then name
-    else NameSpace.implode (map mk_prefix prefix) ^ ":" ^ name
-  end;
-
 end;

--- a/src/Pure/pure_thy.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/pure_thy.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -144,7 +144,7 @@
   (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
 
 fun enter_thms pre_name post_name app_att (b, thms) thy =
-  if Name.is_nothing b
+  if Binding.is_nothing b
   then swap (enter_proofs (app_att (thy, thms)))
   else let
     val naming = Sign.naming_of thy;
@@ -198,7 +198,7 @@
 
 fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   let
-    val pos = Name.pos_of b;
+    val pos = Binding.pos_of b;
     val name = Sign.full_binding thy b;
     val _ = Position.report (Markup.fact_decl name) pos;
 

--- a/src/Pure/sign.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/sign.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -535,7 +535,7 @@
 
 fun declare_const tags ((b, T), mx) thy =
   let
-    val pos = Name.pos_of b;
+    val pos = Binding.pos_of b;
     val tags' = Position.default_properties pos tags;
     val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
     val _ = Position.report (Markup.const_decl c) pos;