src/Pure/Isar/args.ML
changeset 8687 24bff69370f0
parent 8549 851d39c10d9f
child 8803 189203bb4b34
equal deleted inserted replaced
8686:5893f2952e4f 8687:24bff69370f0
    18   val not_eof: T -> bool
    18   val not_eof: T -> bool
    19   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    19   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    20   val !!! : (T list -> 'a) -> T list -> 'a
    20   val !!! : (T list -> 'a) -> T list -> 'a
    21   val $$$ : string -> T list -> string * T list
    21   val $$$ : string -> T list -> string * T list
    22   val name: T list -> string * T list
    22   val name: T list -> string * T list
       
    23   val name_dummy: T list -> string option * T list
    23   val nat: T list -> int * T list
    24   val nat: T list -> int * T list
    24   val var: T list -> indexname * T list
    25   val var: T list -> indexname * T list
    25   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    26   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    26   val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    27   val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    27   val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    28   val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   101 
   102 
   102 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   103 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   103 fun $$$ x = $$$$ x >> val_of;
   104 fun $$$ x = $$$$ x >> val_of;
   104 
   105 
   105 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
   106 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
       
   107 val name_dummy = $$$ "_" >> K None || name >> Some;
   106 
   108 
   107 val keyword_symid =
   109 val keyword_symid =
   108   Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
   110   Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
   109 
   111 
   110 fun kind f = Scan.one (K true) :--
   112 fun kind f = Scan.one (K true) :--