/[eiffelstudio]/branches/eth/eve/Src/library/base/base2/container/v_container.e
ViewVC logotype

Diff of /branches/eth/eve/Src/library/base/base2/container/v_container.e

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 94770 by polikarn, Mon Feb 24 08:56:09 2014 UTC revision 94771 by polikarn, Thu Apr 3 12:37:44 2014 UTC
# Line 121  feature -- Specification Line 121  feature -- Specification
121                  attribute                  attribute
122                  end                  end
123    
124            add_iterator (it: V_ITERATOR [G])
125                            -- Add `it' to `observers'.
126                    note
127                            status: ghost
128                            explicit: contracts
129                    require
130                            wrapped: is_wrapped
131                            it_not_current: it /= Current
132                            modify_field (["observers", "closed"], Current)
133                    do
134                            set_observers (observers & it)
135                    ensure
136                            is_wrapped
137                            observers = old observers & it
138                    end
139    
140          forget_iterator (it: V_ITERATOR [G])          forget_iterator (it: V_ITERATOR [G])
141                          -- Remove `it' from `observers'.                          -- Remove `it' from `observers'.
142                  note                  note
# Line 130  feature -- Specification Line 146  feature -- Specification
146                          wrapped: is_wrapped                          wrapped: is_wrapped
147                          it_wrapped: it.is_wrapped                          it_wrapped: it.is_wrapped
148                          valid_target: it.target = Current                          valid_target: it.target = Current
149                          modify_model (["observers"], Current)                          modify_field (["observers", "closed"], Current)
150                          modify_model (["closed"], it)                          modify_field (["closed"], it)
151                  do                  do
152                          it.unwrap                          it.unwrap
153                          set_observers (observers / it)                          set_observers (observers / it)
# Line 149  feature -- Specification Line 165  feature -- Specification
165                  require                  require
166                          wrapped: is_wrapped                          wrapped: is_wrapped
167                          observers_wrapped: across observers as o all o.item.is_wrapped  end                          observers_wrapped: across observers as o all o.item.is_wrapped  end
168                          modify_model (["observers"], Current)                          modify_field (["observers", "closed"], Current)
169                          modify_model (["closed"], observers)                          modify_field (["closed"], observers)
170                  do                  do
171                          unwrap_all (observers)                          unwrap_all (observers)
172                          set_observers ([])                          set_observers ([])

Legend:
Removed from v.94770  
changed lines
  Added in v.94771

  ViewVC Help
Powered by ViewVC 1.1.23