# [isabelle-dev] Isabelle/PIDE as ML IDE: syntax highlighting of string literals

Makarius makarius at sketis.net
Mon Dec 8 17:06:56 CET 2014

On Mon, 1 Dec 2014, Christian Sternagel wrote:

> A tiny thing I noticed recently is that in the presence of control
> symbols, string literals are highlighted somewhat strange. To see what I
> mean, consult the attached screenshot, where after a "\<^sub>" in a
> string literal function names are no longer highlighted black.

Thanks for keeping an eye on such details.  I have refined that in
Isabelle/50ccc027e8a7.

Some hints on your application, which was spelled out like this:

fun sub s = String.explode s |> map (fn c => "⇩" ^ String.str c) |> String.conca

Here you are looking at the physical representation of Isabelle strings,
as list of characters, but the char type of SML is not used in Isabelle/ML
(main exceptions: system implementation and external tool connectivity).

This version is more canonical:

fun sub str = Symbol.explode str |> map (fn s => "⇩" ^ s) |> implode

\item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
from the packed form.  This function supersedes @{ML
"String.explode"} for virtually all purposes of manipulating text in
Isabelle!

As well as section "Characters":

\item Type @{ML_type char} is \emph{not} used.  The smallest textual
unit in Isabelle is represented as a symbol'' (see
\secref{sec:symbols}).

Maybe the Isabelle/ML IDE should somehow highlight accidental emergence of
type char, which is usually a mistake.  Although in this particular
example, it should have been semantically clear that it is about
mathematical symbols in general, not ASCII text.

Moreover, the task to subscript a piece of text is more difficult than it
seems at first sight --- depending on the application and its ambition.
In Isabelle/jEdit there is Token_Markup.edit_control_style to apply
\<^sub> or \<^sup> or \<^bold> to some text selection, taking into account
that controls work only once, so existing ones need to be cleared first.
Adjacent controls also need special care.

Makarius

----------------------------------------------------------------------------
https://stop-ttip.org/signatures-member-states
----------------------------------------------------------------------------