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

[Makarius]

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


See also the "implementation" manual, section "Strings of symbols":

   \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
----------------------------------------------------------------------------