# HG changeset patch
# User wenzelm
# Date 1442245169 -7200
# Node ID 74eddfef841e6c906ae41decd467a341e156543c
# Parent  5f3f203a38ad901bcfdb3ce1b7113d8aa97adb76
replacement character for spaces;

diff -r 5f3f203a38ad -r 74eddfef841e NEWS
--- a/NEWS	Mon Sep 14 16:44:09 2015 +0200
+++ b/NEWS	Mon Sep 14 17:39:29 2015 +0200
@@ -347,6 +347,11 @@
 
 *** System ***
 
+* Property values in etc/symbols may contain spaces, if written with the
+replacement character "␣" (Unicode point 0x2324).  For example:
+
+  \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
+
 * Command-line tool "isabelle jedit_client" allows to connect to already
 running Isabelle/jEdit process. This achieves the effect of
 single-instance applications seen on common GUI desktops.
diff -r 5f3f203a38ad -r 74eddfef841e src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Sep 14 16:44:09 2015 +0200
+++ b/src/Pure/General/symbol.scala	Mon Sep 14 17:39:29 2015 +0200
@@ -289,7 +289,7 @@
         props match {
           case Nil => Nil
           case _ :: Nil => err()
-          case Key(x) :: y :: rest => (x -> y) :: read_props(rest)
+          case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest)
           case _ => err()
         }
       }