On Tue, 25 Aug 2015, Rafal Kolanski wrote:
3. Trying to specify a font with a space in the name (e.g. Arial
Unicode MS, Cambria Math) doesn't work, because the config lines
in etc/symbols are split on \s+
See the following changeset:
changeset: 61174:74eddfef841e
tag: tip
user: wenzelm
date: Mon Sep 14 17:39:29 2015 +0200
files: NEWS src/Pure/General/symbol.scala
description:
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()
}
}
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
