src/Pure/Isar/parse.ML
changeset 59918 d01e6d159c33
parent 59917 9830c944670f
child 59924 801b979ec0c2
equal deleted inserted replaced
59917:9830c944670f 59918:d01e6d159c33
    42   val reserved: string -> string parser
    42   val reserved: string -> string parser
    43   val underscore: string parser
    43   val underscore: string parser
    44   val maybe: 'a parser -> 'a option parser
    44   val maybe: 'a parser -> 'a option parser
    45   val tag_name: string parser
    45   val tag_name: string parser
    46   val tags: string list parser
    46   val tags: string list parser
    47   val opt_unit: unit parser
       
    48   val opt_keyword: string -> bool parser
    47   val opt_keyword: string -> bool parser
    49   val opt_bang: bool parser
    48   val opt_bang: bool parser
    50   val begin: string parser
    49   val begin: string parser
    51   val opt_begin: bool parser
    50   val opt_begin: bool parser
    52   val nat: int parser
    51   val nat: int parser
   228 val real = float_number >> Markup.parse_real || int >> Real.fromInt;
   227 val real = float_number >> Markup.parse_real || int >> Real.fromInt;
   229 
   228 
   230 val tag_name = group (fn () => "tag name") (short_ident || string);
   229 val tag_name = group (fn () => "tag name") (short_ident || string);
   231 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
   230 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
   232 
   231 
   233 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
       
   234 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
   232 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
   235 val opt_bang = Scan.optional ($$$ "!" >> K true) false;
   233 val opt_bang = Scan.optional ($$$ "!" >> K true) false;
   236 
   234 
   237 val begin = $$$ "begin";
   235 val begin = $$$ "begin";
   238 val opt_begin = Scan.optional (begin >> K true) false;
   236 val opt_begin = Scan.optional (begin >> K true) false;