src/Pure/Isar/args.ML
changeset 9126 ca8c6793dca5
parent 8896 c80aba8c1d5e
child 9504 8168600e88a5
equal deleted inserted replaced
9125:f85564116be1 9126:ca8c6793dca5
   166 fun goal_spec def = Scan.lift (Scan.optional goal def);
   166 fun goal_spec def = Scan.lift (Scan.optional goal def);
   167 
   167 
   168 
   168 
   169 (* args *)
   169 (* args *)
   170 
   170 
   171 val exclude = explode "(){}[],";
   171 val exclude = explode "()[],";
   172 
   172 
   173 fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
   173 fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
   174   k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
   174   k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
   175 
   175 
   176 fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
   176 fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)