src/Pure/Isar/parse.ML
changeset 59924 801b979ec0c2
parent 59918 d01e6d159c33
child 59939 7d46aa03696e
--- a/src/Pure/Isar/parse.ML	Sat Apr 04 14:04:11 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Sat Apr 04 21:21:40 2015 +0200
@@ -103,6 +103,8 @@
   val literal_fact: string parser
   val propp: (string * string list) parser
   val termp: (string * string list) parser
+  val private: Position.T parser
+  val opt_private: Position.T option parser
   val target: (xstring * Position.T) parser
   val opt_target: (xstring * Position.T) option parser
   val args: Token.T list parser
@@ -396,7 +398,10 @@
 val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
 
 
-(* targets *)
+(* target information *)
+
+val private = position ($$$ "private") >> #2;
+val opt_private = Scan.option private;
 
 val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
 val opt_target = Scan.option target;