attrib: keyword_symid;
authorwenzelm
Sun Feb 13 20:52:58 2000 +0100 (2000-02-13)
changeset 823385169951d515
parent 8232 6b19ee96546c
child 8234 36a85a6c4852
attrib: keyword_symid;
goal_spec;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Thu Feb 10 20:54:40 2000 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Sun Feb 13 20:52:58 2000 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4    val local_term: Proof.context * T list -> term * (Proof.context * T list)
     1.5    val local_prop: Proof.context * T list -> term * (Proof.context * T list)
     1.6    val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
     1.7 +  val goal_spec: T list -> ((int -> tactic) -> tactic) * T list
     1.8    type src
     1.9    val src: (string * T list) * Position.T -> src
    1.10    val dest_src: src -> (string * T list) * Position.T
    1.11 @@ -102,6 +103,9 @@
    1.12  
    1.13  val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
    1.14  
    1.15 +val keyword_symid =
    1.16 +  Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
    1.17 +
    1.18  fun kind f = Scan.one (K true) :--
    1.19    (fn Arg (Ident, (x, _)) =>
    1.20      (case f x of Some y => Scan.succeed y | _ => Scan.fail)
    1.21 @@ -139,6 +143,12 @@
    1.22    ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
    1.23  
    1.24  
    1.25 +(* goal specifier *)
    1.26 +
    1.27 +val tactical = $$$$ "!" >> K ALLGOALS || $$$$ "?" >> K FINDGOAL || nat >> curry op |>;
    1.28 +val goal_spec = $$$$ "(" |-- tactical --| $$$$ ")";
    1.29 +
    1.30 +
    1.31  (* args *)
    1.32  
    1.33  val exclude = explode "(){}[],";
    1.34 @@ -185,7 +195,7 @@
    1.35  fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
    1.36  fun list scan = list1 scan || Scan.succeed [];
    1.37  
    1.38 -val attrib = position (name -- !!! (args false)) >> src;
    1.39 +val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
    1.40  val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
    1.41  val opt_attribs = Scan.optional attribs [];
    1.42