public String where(int p)
    {
      int ln = 1;   // Line number
      int ls = -1;  // Line start (position of preceding newline)
      int nextnl;   // Position of next newline or end

      while (true)
      {
        nextnl = text.indexOf('\n',ls+1);
        if (nextnl<0) nextnl = text.length();
        if (ls<p && p<=nextnl)
          return ("line " + ln + " col. " + (p-ls));
        ls = nextnl;
        ln++;
      }
    }