class SHARED

feature

	Saved_text:STRING is
			-- Text being edited in a temporarily interrupted editing session
		once
			create Result.make(0)
		end

end -- class SHARED