[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts

[Makarius]

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