--- 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.
--- 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()
}
}