+ dropPosition();
+ return Arg(true, oss.str());
+}
+
+
+string const Parser::verbatimEnvironment(string const & name)
+{
+ //FIXME: do something if endstring is not found
+ string s = verbatimStuff("\\end{" + name + "}").second;
+ // ignore one newline at beginning or end of string
+ if (prefixIs(s, "\n"))
+ s.erase(0,1);
+ if (suffixIs(s, "\n"))
+ s.erase(s.length() - 1,1);
+ return s;
+}
+
+
+string Parser::verbatimOption()
+{
+ string res;
+ if (next_token().character() == '[') {
+ Token t = get_token();
+ for (t = get_token(); t.character() != ']' && good(); t = get_token()) {
+ if (t.cat() == catBegin) {
+ putback();
+ res += '{' + verbatim_item() + '}';
+ } else
+ res += t.asInput();
+ }
+ }
+ return res;
+}
+
+
+string Parser::verbatim_item()
+{