src/Pure/Syntax/lexicon.ML
changeset 4587 6bce9ef27d7e
parent 4247 9bba9251bb4d
child 4703 a50ab39756db
equal deleted inserted replaced
4586:6d0c1b2dc717 4587:6bce9ef27d7e
    50   val scan_varname: string list -> indexname * string list
    50   val scan_varname: string list -> indexname * string list
    51   val scan_var: string -> term
    51   val scan_var: string -> term
    52   val const: string -> term
    52   val const: string -> term
    53   val free: string -> term
    53   val free: string -> term
    54   val var: indexname -> term
    54   val var: indexname -> term
       
    55   val read_var: string -> string * int
    55 end;
    56 end;
    56 
    57 
    57 signature LEXICON =
    58 signature LEXICON =
    58 sig
    59 sig
    59   include SCANNER
    60   include SCANNER
   491   in
   492   in
   492     #1 (scan (explode str))
   493     #1 (scan (explode str))
   493   end;
   494   end;
   494 
   495 
   495 
   496 
       
   497 (* read_var *)
       
   498 
       
   499 fun read_var str =
       
   500   let val scan = $$ "?" -- scan_vname -- scan_end >> (#2 o #1) in
       
   501     #1 (scan (explode str)) handle LEXICAL_ERROR
       
   502       => error ("Bad variable " ^ quote str)
       
   503   end;
       
   504 
       
   505 
   496 end;
   506 end;