# HG changeset patch
# User wenzelm
# Date 1606577129 -3600
# Node ID bd5ee31481322f1dd73be696aa5dd992eb611f7f
# Parent  9d0951e24e615f23853e15cc4992d37662e33219
more antiquotations (reverting 4df341249348);

diff -r 9d0951e24e61 -r bd5ee3148132 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Sat Nov 28 15:59:24 2020 +0100
+++ b/src/Doc/System/Scala.thy	Sat Nov 28 16:25:29 2020 +0100
@@ -243,8 +243,7 @@
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Invoke a predefined Scala function that is the identity on type
-  \<^ML_type>\<open>string\<close>:
+  Invoke the predefined Scala function \<^scala_function>\<open>echo\<close>:
 \<close>
 
 ML \<open>
diff -r 9d0951e24e61 -r bd5ee3148132 src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Sat Nov 28 15:59:24 2020 +0100
+++ b/src/Pure/System/scala.ML	Sat Nov 28 16:25:29 2020 +0100
@@ -82,7 +82,9 @@
     (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg;
 
 val _ = Theory.setup
- (ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
+   (Scan.lift Parse.embedded_position) check_function #>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
     (Args.context -- Scan.lift Parse.embedded_position
       >> (uncurry check_function #> ML_Syntax.print_string)) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>