# HG changeset patch
# User wenzelm
# Date 1214485588 -7200
# Node ID f89aa7bd46020f84378225874f3b1e3fb8cec7bc
# Parent  8e8f96dfaf639b8a5c3c2e6a574cdd8aed998d13
added context/theory scanner;

diff -r 8e8f96dfaf63 -r f89aa7bd4602 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Jun 26 15:06:25 2008 +0200
+++ b/src/Pure/Isar/args.ML	Thu Jun 26 15:06:28 2008 +0200
@@ -35,6 +35,8 @@
   val assignable: src -> src
   val assign: value option -> T -> unit
   val closure: src -> src
+  val context: Context.generic * T list -> Context.proof * (Context.generic * T list)
+  val theory: Context.generic * T list -> Context.theory * (Context.generic * T list)
   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
   val !!! : (T list -> 'a) -> T list -> 'a
   val $$$ : string -> T list -> string * T list
@@ -224,6 +226,12 @@
 
 (** scanners **)
 
+(* context *)
+
+fun context x = (Scan.state >> Context.proof_of) x;
+fun theory x = (Scan.state >> Context.theory_of) x;
+
+
 (* position *)
 
 fun position scan =