# HG changeset patch
# User wenzelm
# Date 1459530094 -7200
# Node ID 42934bdf90bacb51117507a6da967574f0897bc7
# Parent  7b9c5416f30edef859076002bbc586bd5e6efb6c
require actual space;

diff -r 7b9c5416f30e -r 42934bdf90ba src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 18:56:31 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 19:01:34 2016 +0200
@@ -247,13 +247,13 @@
     scan_many Symbol.is_digit >> read_block_indent) ||
   $$ ")" >> K En ||
   $$ "/" -- $$ "/" >> K (Brk ~1) ||
-  $$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) ||
-  scan_many1 Symbol.is_blank >> (Space o Symbol_Pos.content) ||
+  $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) ||
+  scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) ||
   Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
 
 val scan_symb =
   Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||
-  $$ "'" -- scan_one Symbol.is_blank >> K NONE;
+  $$ "'" -- scan_one Symbol.is_space >> K NONE;
 
 val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");