src/Pure/Isar/args.ML
changeset 8803 189203bb4b34
parent 8687 24bff69370f0
child 8896 c80aba8c1d5e
equal deleted inserted replaced
8802:2c37263eb903 8803:189203bb4b34
     1 (*  Title:      Pure/Isar/args.ML
     1 (*  Title:      Pure/Isar/args.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
       
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4 
     5 
     5 Concrete argument syntax (of attributes and methods).
     6 Concrete argument syntax (of attributes and methods).
     6 *)
     7 *)
     7 
     8 
     8 signature ARGS =
     9 signature ARGS =
    17   val stopper: T * (T -> bool)
    18   val stopper: T * (T -> bool)
    18   val not_eof: T -> bool
    19   val not_eof: T -> bool
    19   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    20   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    20   val !!! : (T list -> 'a) -> T list -> 'a
    21   val !!! : (T list -> 'a) -> T list -> 'a
    21   val $$$ : string -> T list -> string * T list
    22   val $$$ : string -> T list -> string * T list
       
    23   val colon: T list -> string * T list
       
    24   val parens: (T list -> 'a * T list) -> T list -> 'a * T list
    22   val name: T list -> string * T list
    25   val name: T list -> string * T list
    23   val name_dummy: T list -> string option * T list
    26   val name_dummy: T list -> string option * T list
    24   val nat: T list -> int * T list
    27   val nat: T list -> int * T list
    25   val var: T list -> indexname * T list
    28   val var: T list -> indexname * T list
    26   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    29   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   101 (* basic *)
   104 (* basic *)
   102 
   105 
   103 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   106 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   104 fun $$$ x = $$$$ x >> val_of;
   107 fun $$$ x = $$$$ x >> val_of;
   105 
   108 
       
   109 val colon = $$$ ":";
       
   110 fun parens scan = $$$ "(" |-- scan --| $$$ ")";
       
   111 
   106 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
   112 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
   107 val name_dummy = $$$ "_" >> K None || name >> Some;
   113 val name_dummy = $$$ "_" >> K None || name >> Some;
   108 
   114 
   109 val keyword_symid =
   115 val keyword_symid =
   110   Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
   116   Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;