Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] x-symbol in Carbon Emacs


view this post on Zulip Email Gateway (Aug 18 2022 at 12:03):

From: Chris Osborn <cosborn3@uiuc.edu>
Hello all,

I am on a brand new MacBook Pro (OS 10.5.3) using Isabelle 2007 and
the current release of Carbon Emacs.

x-symbol fails to load (from the ProofGeneral menu) under Carbon Emacs.
In the bottom window, I get the error:

Warning (emacs): X-Symbol characters with registry "xsymb-xsymb1" are not used

On the line at the very bottom, I get:

Symbol's value as variable is void: ccl-encode-fake-xsymb1-font

Does anyone know what might cause this?

Thanks in advance,
Chris

view this post on Zulip Email Gateway (Aug 18 2022 at 12:05):

From: Makarius <makarius@sketis.net>
I would say this is because Carbon Emacs is a native Mac OS application,
without support for the X Window system.

More recent versions of Proof General support mathematical symbols in
Carbon Emacs via Unicode, but there are still some rough edges. Problem
reports can be dumped to http://proofgeneral.inf.ed.ac.uk/trac/

Makarius


Last updated: May 03 2024 at 12:27 UTC