more antiquotations (reverting 4df341249348);

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

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