38 class Workspace {
41   virtual ~Workspace() {}  in ~Workspace()
44   // Create an empty workspace.
45   Workspace() {}  in Workspace()  function
48   SAFTM_DISALLOW_COPY_AND_ASSIGN(Workspace);
69   // Returns the index of a named workspace, adding it to the registry first
84   // Returns the maximum workspace id that has been registered.
98   // Workspace type names, indexed as workspace_types_[typeid].
101   // Workspace names, indexed as workspace_names_[typeid][workspace].
104   // The maximum workspace id that has been registered.
117   // Returns true if a workspace has been set.
129   // Returns an indexed workspace; the workspace must have been set.
134     const Workspace *w = workspaces_[id][index];  in Get()
138   // Sets an indexed workspace; this takes ownership of the workspace, which
139   // must have been new-allocated.  It is an error to set a workspace twice.
141   void Set(int index, W *workspace) {  in Set()  argument
148     SAFTM_DCHECK(workspace != nullptr);  in Set()
149     workspaces_[id][index] = workspace;  in Set()
160     workspaces_.resize(registry.MaxId() + 1, std::vector<Workspace *>());  in Reset()
168   std::vector<std::vector<Workspace *> > workspaces_;
171 // A workspace that wraps around a vector of int.
172 class VectorIntWorkspace : public Workspace {
184   // Returns the name of this type of workspace.