src/Pure/Isar/outer_parse.ML

  (position (xname >> rpair []) >> (Method.Source o Args.src) ||
   $$$ "(" |-- !!! (meth0 --| $$$ ")")) x
 and meth3 x =
  (meth4 --| $$$ "?" >> Method.Try ||
   meth4 --| $$$ "+" >> Method.Repeat1 ||
+  meth4 -- ($$$ "[" |-- nat --| $$$ "]") >> (Method.SelectGoals o swap) ||
   meth4) x
 and meth2 x =
  (position (xname -- args1 is_symid_meth false) >> (Method.Source o Args.src) ||
   meth3) x
 and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Method.Then ms)) x