--- a/src/Doc/System/Scala.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Scala.thy Sun Jan 15 18:30:18 2023 +0100
@@ -13,7 +13,7 @@
\<^item> Isabelle/ML is for \<^emph>\<open>mathematics\<close>, to develop tools within the context
of symbolic logic, e.g.\ for constructing proofs or defining
domain-specific formal languages. See the \<^emph>\<open>Isabelle/Isar implementation
- manual\<close> @{cite "isabelle-implementation"} for more details.
+ manual\<close> \<^cite>\<open>"isabelle-implementation"\<close> for more details.
\<^item> Isabelle/Scala is for \<^emph>\<open>physics\<close>, to connect with the world of systems
and services, including editors and IDE frameworks.
@@ -27,7 +27,7 @@
(\secref{sec:scala-functions}) via the PIDE protocol: execution happens
within the running Java process underlying Isabelle/Scala.
- \<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit @{cite "isabelle-jedit"}
+ \<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>
operates on the running Java application, using the Scala
read-eval-print-loop (REPL).