src/Pure/Isar/outer_syntax.ML
changeset 51271 e8d2ecf6aaac
parent 51268 fcc4b89a600d
child 51627 589daaf48dba
equal deleted inserted replaced
51270:17d30843fc3b 51271:e8d2ecf6aaac
   291 val span_cmts = filter Token.is_proper #> cmts;
   291 val span_cmts = filter Token.is_proper #> cmts;
   292 
   292 
   293 end;
   293 end;
   294 
   294 
   295 
   295 
   296 (* read toplevel commands -- fail-safe *)
   296 (* read command span -- fail-safe *)
   297 
   297 
   298 fun read_span outer_syntax toks =
   298 fun read_span outer_syntax toks =
   299   let
   299   let
   300     val commands = lookup_commands outer_syntax;
   300     val commands = lookup_commands outer_syntax;
   301 
   301