tuned text;
authorwenzelm
Mon, 09 May 2022 13:41:10 +0200
changeset 75945 5acc4de7db89
parent 75944 f16d83de3e4a
child 75946 7095df141819
tuned text;
src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri May 06 17:03:35 2022 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Mon May 09 13:41:10 2022 +0200
@@ -27,9 +27,11 @@
     \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
     extends the pure logical environment of Isabelle/ML towards the outer
     world of graphical user interfaces, text editors, IDE frameworks, web
-    services, SSH servers, SQL databases etc. Special infrastructure allows to
-    transfer algebraic datatypes and formatted text easily between ML and
-    Scala, using asynchronous protocol commands.
+    services, SSH servers, SQL databases etc. Both Scala and ML provide
+    library modules to support formatted text with formal markup, and to
+    encode/decode algebraic datatypes. Scala communicates with ML via
+    asynchronous protocol commands; from the ML perspective this is wrapped up
+    as synchronous function call (RPC).
 
     \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
     is built around a concept of parallel and asynchronous document