src/Pure/Syntax/lexicon.ML
changeset 5513 3896c7894a57
parent 5286 cfb74a99182c
child 5860 ed11c9890852
equal deleted inserted replaced
5512:4327eec06849 5513:3896c7894a57
    92 val scan_id = scan_letter_letdigs >> implode;
    92 val scan_id = scan_letter_letdigs >> implode;
    93 val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
    93 val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
    94 val scan_tid = $$ "'" ^^ scan_id;
    94 val scan_tid = $$ "'" ^^ scan_id;
    95 
    95 
    96 val scan_nat = scan_digits1 >> implode;
    96 val scan_nat = scan_digits1 >> implode;
    97 val scan_int = $$ "~" ^^ scan_nat || scan_nat;
    97 val scan_int = $$ "-" ^^ scan_nat || scan_nat;
    98 
    98 
    99 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
    99 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
   100 val scan_var = $$ "?" ^^ scan_id_nat;
   100 val scan_var = $$ "?" ^^ scan_id_nat;
   101 val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
   101 val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
   102 
   102