src/Pure/ML/ml_parse.ML
changeset 27817 78cae5cca09e
parent 24594 6689effe75d1
child 29606 fedb8be05f24
equal deleted inserted replaced
27816:0dfed2f2822a 27817:78cae5cca09e
    32     (fn msg => Scan.fail_with (K msg))) x;
    32     (fn msg => Scan.fail_with (K msg))) x;
    33 
    33 
    34 
    34 
    35 (** basic parsers **)
    35 (** basic parsers **)
    36 
    36 
    37 fun $$$ x = Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.val_of tok = x) >> T.val_of;
    37 fun $$$ x =
    38 val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.val_of;
    38   Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.content_of tok = x) >> T.content_of;
       
    39 val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.content_of;
    39 
    40 
    40 val regular = Scan.one T.is_regular >> T.val_of;
    41 val regular = Scan.one T.is_regular >> T.content_of;
    41 val improper = Scan.one T.is_improper >> T.val_of;
    42 val improper = Scan.one T.is_improper >> T.content_of;
    42 
    43 
    43 val blanks = Scan.repeat improper >> implode;
    44 val blanks = Scan.repeat improper >> implode;
    44 
    45 
    45 
    46 
    46 (* fix_ints *)
    47 (* fix_ints *)