src/Pure/Isar/outer_parse.ML
changeset 27788 5def98c2646b
parent 27787 3bff97077d26
child 27815 2d36632bc5de
equal deleted inserted replaced
27787:3bff97077d26 27788:5def98c2646b
   139 
   139 
   140 val not_eof = Scan.one T.not_eof;
   140 val not_eof = Scan.one T.not_eof;
   141 
   141 
   142 fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
   142 fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
   143 
   143 
   144 (*fun inner_syntax token = Scan.ahead token |-- not_eof >> T.source_of; FIXME tmp *)
   144 fun inner_syntax token = Scan.ahead token |-- not_eof >> T.source_of;
   145 fun inner_syntax token = token;
       
   146 
   145 
   147 fun kind k =
   146 fun kind k =
   148   group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);
   147   group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);
   149 
   148 
   150 val command = kind T.Command;
   149 val command = kind T.Command;