# HG changeset patch
# User wenzelm
# Date 1398513025 -7200
# Node ID f87e3be0de9ace519366b39615331bfa5096d519
# Parent  d37a5d09a27752d1974b635c524afa60b4107399
clarified;

diff -r d37a5d09a277 -r f87e3be0de9a src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Sat Apr 26 13:34:10 2014 +0200
+++ b/src/Pure/General/word.scala	Sat Apr 26 13:50:25 2014 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/word.scala
     Author:     Makarius
 
-Support for plain text words.
+Support for words within Unicode text.
 */
 
 package isabelle
@@ -84,6 +84,6 @@
     explode(_ == sep, text)
 
   def explode(text: String): List[String] =
-    explode(Symbol.is_ascii_blank(_), text)
+    explode(Character.isWhitespace(_), text)
 }