minor tuning;
authorwenzelm
Sat Mar 15 15:50:41 2014 +0100 (2014-03-15)
changeset 56164c7805a88f952
parent 56163 331f4aba14b3
child 56165 dd89ce51d2c8
minor tuning;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sat Mar 15 15:49:23 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Mar 15 15:50:41 2014 +0100
     1.3 @@ -107,13 +107,26 @@
     1.4  fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
     1.5  
     1.6  
     1.7 +(* internal names *)
     1.8 +
     1.9 +type internals = (string list * string list) Change_Table.T;  (*xname -> visible, hidden*)
    1.10 +
    1.11 +fun map_internals f xname : internals -> internals =
    1.12 +  Change_Table.map_default (xname, ([], [])) f;
    1.13 +
    1.14 +val del_name = map_internals o apfst o remove (op =);
    1.15 +fun del_name_extra name =
    1.16 +  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
    1.17 +val add_name = map_internals o apfst o update (op =);
    1.18 +val add_name' = map_internals o apsnd o update (op =);
    1.19 +
    1.20 +
    1.21  (* datatype T *)
    1.22  
    1.23  datatype T =
    1.24    Name_Space of
    1.25 -   {kind: string,
    1.26 -    internals: (string list * string list) Change_Table.T,  (*visible, hidden*)
    1.27 -    entries: (xstring list * entry) Change_Table.T};        (*externals, entry*)
    1.28 +   {kind: string, internals: internals,
    1.29 +    entries: (xstring list * entry) Change_Table.T};  (*name -> externals, entry*)
    1.30  
    1.31  fun make_name_space (kind, internals, entries) =
    1.32    Name_Space {kind = kind, internals = internals, entries = entries};
    1.33 @@ -127,9 +140,6 @@
    1.34  val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
    1.35    (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
    1.36  
    1.37 -fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
    1.38 -  (kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
    1.39 -
    1.40  
    1.41  fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
    1.42  
    1.43 @@ -248,15 +258,6 @@
    1.44    else Completion.none;
    1.45  
    1.46  
    1.47 -(* modify internals *)
    1.48 -
    1.49 -val del_name = map_internals o apfst o remove (op =);
    1.50 -fun del_name_extra name =
    1.51 -  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
    1.52 -val add_name = map_internals o apfst o update (op =);
    1.53 -val add_name' = map_internals o apsnd o update (op =);
    1.54 -
    1.55 -
    1.56  (* hide *)
    1.57  
    1.58  fun hide fully name space =
    1.59 @@ -265,13 +266,15 @@
    1.60    else if Long_Name.is_hidden name then
    1.61      error ("Attempt to hide hidden name " ^ quote name)
    1.62    else
    1.63 -    let val names = valid_accesses space name in
    1.64 -      space
    1.65 -      |> add_name' name name
    1.66 -      |> fold (del_name name)
    1.67 -        (if fully then names else inter (op =) [Long_Name.base_name name] names)
    1.68 -      |> fold (del_name_extra name) (get_accesses space name)
    1.69 -    end;
    1.70 +    space |> map_name_space (fn (kind, internals, entries) =>
    1.71 +      let
    1.72 +        val names = valid_accesses space name;
    1.73 +        val internals' = internals
    1.74 +          |> add_name' name name
    1.75 +          |> fold (del_name name)
    1.76 +            (if fully then names else inter (op =) [Long_Name.base_name name] names)
    1.77 +          |> fold (del_name_extra name) (get_accesses space name);
    1.78 +      in (kind, internals', entries) end);
    1.79  
    1.80  
    1.81  (* merge *)
    1.82 @@ -397,15 +400,15 @@
    1.83  fun alias naming binding name space =
    1.84    let
    1.85      val (accs, accs') = accesses naming binding;
    1.86 -    val space' = space
    1.87 -      |> fold (add_name name) accs
    1.88 -      |> map_name_space (fn (kind, internals, entries) =>
    1.89 +    val space' =
    1.90 +      space |> map_name_space (fn (kind, internals, entries) =>
    1.91          let
    1.92            val _ = Change_Table.defined entries name orelse error (undefined kind name);
    1.93 +          val internals' = internals |> fold (add_name name) accs;
    1.94            val entries' = entries
    1.95              |> Change_Table.map_entry name (fn (externals, entry) =>
    1.96                (Library.merge (op =) (externals, accs'), entry))
    1.97 -        in (kind, internals, entries') end);
    1.98 +        in (kind, internals', entries') end);
    1.99    in space' end;
   1.100  
   1.101  
   1.102 @@ -436,16 +439,6 @@
   1.103  
   1.104  (* declaration *)
   1.105  
   1.106 -fun new_entry strict (name, (externals, entry)) =
   1.107 -  map_name_space (fn (kind, internals, entries) =>
   1.108 -    let
   1.109 -      val entries' =
   1.110 -        (if strict then Change_Table.update_new else Change_Table.update)
   1.111 -          (name, (externals, entry)) entries
   1.112 -        handle Change_Table.DUP dup =>
   1.113 -          err_dup kind (dup, #2 (the (Change_Table.lookup entries dup))) (name, entry) (#pos entry);
   1.114 -    in (kind, internals, entries') end);
   1.115 -
   1.116  fun declare context strict binding space =
   1.117    let
   1.118      val naming = naming_of context;
   1.119 @@ -463,9 +456,17 @@
   1.120        theory_name = theory_name,
   1.121        pos = pos,
   1.122        id = serial ()};
   1.123 -    val space' = space
   1.124 -      |> fold (add_name name) accs
   1.125 -      |> new_entry strict (name, (accs', entry));
   1.126 +    val space' =
   1.127 +      space |> map_name_space (fn (kind, internals, entries) =>
   1.128 +        let
   1.129 +          val internals' = internals |> fold (add_name name) accs;
   1.130 +          val entries' =
   1.131 +            (if strict then Change_Table.update_new else Change_Table.update)
   1.132 +              (name, (accs', entry)) entries
   1.133 +            handle Change_Table.DUP dup =>
   1.134 +              err_dup kind (dup, #2 (the (Change_Table.lookup entries dup)))
   1.135 +                (name, entry) (#pos entry);
   1.136 +        in (kind, internals', entries') end);
   1.137      val _ =
   1.138        if proper_pos andalso Context_Position.is_reported_generic context pos then
   1.139          Position.report pos (entry_markup true (kind_of space) (name, entry))