# HG changeset patch
# User wenzelm
# Date 950471578 -3600
# Node ID 85169951d515162caac1588c2e2260da5e84acb8
# Parent  6b19ee96546ce84dc35e954eb902a7799196ddf6
attrib: keyword_symid;
goal_spec;

diff -r 6b19ee96546c -r 85169951d515 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Feb 10 20:54:40 2000 +0100
+++ b/src/Pure/Isar/args.ML	Sun Feb 13 20:52:58 2000 +0100
@@ -33,6 +33,7 @@
   val local_term: Proof.context * T list -> term * (Proof.context * T list)
   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
   val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
+  val goal_spec: T list -> ((int -> tactic) -> tactic) * T list
   type src
   val src: (string * T list) * Position.T -> src
   val dest_src: src -> (string * T list) * Position.T
@@ -102,6 +103,9 @@
 
 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
 
+val keyword_symid =
+  Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
+
 fun kind f = Scan.one (K true) :--
   (fn Arg (Ident, (x, _)) =>
     (case f x of Some y => Scan.succeed y | _ => Scan.fail)
@@ -139,6 +143,12 @@
   ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
 
 
+(* goal specifier *)
+
+val tactical = $$$$ "!" >> K ALLGOALS || $$$$ "?" >> K FINDGOAL || nat >> curry op |>;
+val goal_spec = $$$$ "(" |-- tactical --| $$$$ ")";
+
+
 (* args *)
 
 val exclude = explode "(){}[],";
@@ -185,7 +195,7 @@
 fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
 fun list scan = list1 scan || Scan.succeed [];
 
-val attrib = position (name -- !!! (args false)) >> src;
+val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];