src/Pure/General/symbol.ML
changeset 14221 9276f30eaed6
parent 14173 a3690aeb79d4
child 14232 ef550525c591
equal deleted inserted replaced
14220:4dc132902672 14221:9276f30eaed6
   135   | is_quasi _ = false;
   135   | is_quasi _ = false;
   136 
   136 
   137 fun is_quasi_letter s = is_quasi s orelse is_letter s;
   137 fun is_quasi_letter s = is_quasi s orelse is_letter s;
   138 
   138 
   139 val is_blank =
   139 val is_blank =
   140   fn " " => true | "\t" => true | "\n" => true | "\^L" => true
   140   fn " " => true | "\t" => true | "\r" => true | "\n" => true | "\^L" => true
   141     | "\160" => true | "\\<spacespace>" => true
   141     | "\160" => true | "\\<spacespace>" => true
   142     | _ => false;
   142     | _ => false;
   143 
   143 
   144 fun is_letdig s = is_quasi_letter s orelse is_digit s;
   144 fun is_letdig s = is_quasi_letter s orelse is_digit s;
   145 
   145