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
----------------------------------------------------------------------------_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
