src/Pure/General/symbol_pos.ML
changeset 62782 057e8dbe4326
parent 62781 7ba8b944d093
child 62797 e08c44eed27f
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Mar 31 15:42:01 2016 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Mar 31 16:23:25 2016 +0200
     1.3 @@ -46,6 +46,8 @@
     1.4    val explode0: string -> T list
     1.5    val scan_ident: T list -> T list * T list
     1.6    val is_identifier: string -> bool
     1.7 +  val scan_nat: T list -> T list * T list
     1.8 +  val scan_float: T list -> T list * T list
     1.9  end;
    1.10  
    1.11  structure Symbol_Pos: SYMBOL_POS =
    1.12 @@ -300,6 +302,12 @@
    1.13        SOME (_, []) => true
    1.14      | _ => false);
    1.15  
    1.16 +
    1.17 +(* numerals *)
    1.18 +
    1.19 +val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
    1.20 +val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
    1.21 +
    1.22  end;
    1.23  
    1.24  structure Basic_Symbol_Pos =   (*not open by default*)