diff --git a/etc/settings b/etc/settings
--- a/etc/settings
+++ b/etc/settings
@@ -1,170 +1,172 @@
 # -*- shell-script -*- :mode=shellscript:
 #
 # Isabelle system settings.
 #
 # Important notes:
 #   * See the "system" manual for explanations on Isabelle settings
 #   * User settings go into $ISABELLE_HOME_USER/etc/settings
 #   * DO NOT EDIT the repository copy of this file!
 #   * DO NOT COPY this file into the $ISABELLE_HOME_USER directory!
 
 ###
 ### Isabelle/Scala
 ###
 
 ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2"
 
 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
 
 ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
 isabelle_scala_service 'isabelle.Tools'
 [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
 
+isabelle_scala_service 'isabelle.Functions'
+
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
 unset "JAVA_TOOL_OPTIONS"
 
 #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
 unset XMODIFIERS
 
 
 ###
 ### Interactive sessions (cf. isabelle console)
 ###
 
 ISABELLE_LINE_EDITOR="rlwrap"
 
 
 ###
 ### Batch sessions (cf. isabelle build)
 ###
 
 ISABELLE_BUILD_OPTIONS=""
 
 
 ###
 ### Document preparation (cf. isabelle latex/document)
 ###
 
 ISABELLE_LATEX="latex -file-line-error"
 ISABELLE_PDFLATEX="pdflatex -file-line-error"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
 ISABELLE_EPSTOPDF="epstopdf"
 
 if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
   ISABELLE_LATEX="latex -c-style-errors"
   ISABELLE_PDFLATEX="pdflatex -c-style-errors"
 fi
 
 
 ###
 ### Misc path settings
 ###
 
 ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"
 ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
 
 # The place for user configuration, heap files, etc.
 if [ -z "$ISABELLE_IDENTIFIER" ]; then
   ISABELLE_HOME_USER="$USER_HOME/.isabelle"
 else
   ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
 fi
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
 
 # Location for temporary files (should be on a local file system).
 ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
 
 # Heap locations.
 ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps"
 ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps"
 
 # HTML browser info.
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info"
 
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
   { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
 ISABELLE_SITE_SETTINGS_PRESENT=true
 
 
 ###
 ### Default logic
 ###
 
 ISABELLE_LOGIC=HOL
 
 
 ###
 ### Docs
 ###
 
 # Where to look for docs (multiple dirs separated by ':').
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
 ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY"
 ISABELLE_DOCS_EXAMPLES="~~/src/HOL/ex/Seq.thy:~~/src/HOL/ex/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/HOL/Isar_Examples/Drinker.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML"
 
 # "open" within desktop environment (potentially asynchronous)
 case "$ISABELLE_PLATFORM_FAMILY" in
   linux)
     ISABELLE_OPEN="xdg-open"
     ;;
   macos)
     ISABELLE_OPEN="open"
     ;;
   windows)
     ISABELLE_OPEN="cygstart"
     ;;
 esac
 
 PDF_VIEWER="$ISABELLE_OPEN"
 DVI_VIEWER="$ISABELLE_OPEN"
 
 
 ###
 ### Symbol rendering
 ###
 
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
 
 
 ###
 ### OCaml
 ###
 
 ISABELLE_OPAM_ROOT="$USER_HOME/.opam"
 
 ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.05.0"
 
 
 ###
 ### Haskell
 ###
 
 ISABELLE_STACK_ROOT="$USER_HOME/.stack"
 
 ISABELLE_STACK_RESOLVER="lts-13.19"
 
 ISABELLE_GHC_VERSION="ghc-8.6.4"
 
 
 ###
 ### Misc settings
 ###
 
 ISABELLE_GNUPLOT="gnuplot"
 ISABELLE_FONTFORGE="fontforge"
 
 #ISABELLE_MLTON="/usr/bin/mlton"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML
+++ b/src/Pure/System/scala.ML
@@ -1,70 +1,73 @@
 (*  Title:      Pure/System/scala.ML
     Author:     Makarius
 
 Support for Scala at runtime.
 *)
 
 signature SCALA =
 sig
-  val method: string -> string -> string
-  val promise_method: string -> string -> string future
+  val promise_function: string -> string -> string future
+  val function: string -> string -> string
+  val function_yxml: string -> XML.body -> XML.body
   exception Null
 end;
 
 structure Scala: SCALA =
 struct
 
-(** invoke JVM method via Isabelle/Scala **)
+(** invoke Scala functions from ML **)
 
 val _ = Session.protocol_handler "isabelle.Scala";
 
 
 (* pending promises *)
 
 val new_id = string_of_int o Counter.make ();
 
 val promises =
   Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
 
 
-(* method invocation *)
+(* invoke function *)
 
-fun promise_method name arg =
+fun promise_function name arg =
   let
     val id = new_id ();
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
     val promise = Future.promise_name "invoke_scala" abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   in promise end;
 
-fun method name arg = Future.join (promise_method name arg);
+fun function name arg = Future.join (promise_function name arg);
+
+fun function_yxml name = YXML.string_of_body #> function name #> YXML.parse_body;
 
 
 (* fulfill *)
 
 exception Null;
 
 fun fulfill id tag res =
   let
     val result =
       (case tag of
         "0" => Exn.Exn Null
       | "1" => Exn.Res res
       | "2" => Exn.Exn (ERROR res)
       | "3" => Exn.Exn (Fail res)
       | "4" => Exn.Exn Exn.Interrupt
       | _ => raise Fail "Bad tag");
     val promise =
       Synchronized.change_result promises
         (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
     val _ = Future.fulfill_result promise result;
   in () end;
 
 val _ =
   Isabelle_Process.protocol_command "Scala.fulfill"
     (fn [id, tag, res] =>
       fulfill id tag res
         handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
 
 end;
diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala
+++ b/src/Pure/System/scala.scala
@@ -1,200 +1,201 @@
 /*  Title:      Pure/System/scala.scala
     Author:     Makarius
 
 Support for Scala at runtime.
 */
 
 package isabelle
 
 
 import java.lang.reflect.{Modifier, InvocationTargetException}
 import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.util.matching.Regex
 import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
 import scala.tools.nsc.interpreter.IMain
 
 
 object Scala
 {
   /** compiler **/
 
   object Compiler
   {
     lazy val default_context: Context = context()
 
     def context(
       error: String => Unit = Exn.error,
       jar_dirs: List[JFile] = Nil): Context =
     {
       def find_jars(dir: JFile): List[String] =
         File.find_files(dir, file => file.getName.endsWith(".jar")).
           map(File.absolute_name)
 
       val class_path =
         for {
           prop <- List("scala.boot.class.path", "java.class.path")
           path = System.getProperty(prop, "") if path != "\"\""
           elem <- space_explode(JFile.pathSeparatorChar, path)
         } yield elem
 
       val settings = new GenericRunnerSettings(error)
       settings.classpath.value =
         (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
 
       new Context(settings)
     }
 
     def default_print_writer: PrintWriter =
       new NewLinePrintWriter(new ConsoleWriter, true)
 
     class Context private [Compiler](val settings: GenericRunnerSettings)
     {
       override def toString: String = settings.toString
 
       def interpreter(
         print_writer: PrintWriter = default_print_writer,
         class_loader: ClassLoader = null): IMain =
       {
         new IMain(settings, print_writer)
         {
           override def parentClassLoader: ClassLoader =
             if (class_loader == null) super.parentClassLoader
             else class_loader
         }
       }
 
       def toplevel(source: String): List[String] =
       {
         val out = new StringWriter
         val interp = interpreter(new PrintWriter(out))
         val rep = new interp.ReadEvalPrint
         val ok = interp.withLabel("\u0001") { rep.compile(source) }
         out.close
 
         val Error = """(?s)^\S* error: (.*)$""".r
         val errors =
           space_explode('\u0001', Library.strip_ansi_color(out.toString)).
             collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
         if (!ok && errors.isEmpty) List("Error") else errors
       }
     }
   }
 
 
 
-  /** invoke JVM method via Isabelle/Scala **/
-
-  /* method reflection */
-
-  private val Ext = new Regex("(.*)\\.([^.]*)")
-  private val STRING = Class.forName("java.lang.String")
+  /** invoke Scala functions from ML **/
 
-  private def get_method(name: String): String => String =
-    name match {
-      case Ext(class_name, method_name) =>
-        val m =
-          try { Class.forName(class_name).getMethod(method_name, STRING) }
-          catch {
-            case _: ClassNotFoundException | _: NoSuchMethodException =>
-              error("No such method: " + quote(name))
-          }
-        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
-        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
+  /* registered functions */
 
-        (arg: String) => {
-          try { m.invoke(null, arg).asInstanceOf[String] }
-          catch {
-            case e: InvocationTargetException if e.getCause != null =>
-              throw e.getCause
-          }
-        }
-      case _ => error("Malformed method name: " + quote(name))
-    }
+  object Fun
+  {
+    def apply(name: String, fn: String => String): Fun =
+      new Fun(name, fn, false)
+
+    def yxml(name: String, fn: XML.Body => XML.Body): Fun =
+      new Fun(name, s => YXML.string_of_body(fn(YXML.parse_body(s))), true)
+  }
+  class Fun private(val name: String, val fn: String => String, val yxml: Boolean)
+  {
+    def decl: (String, Boolean) = (name, yxml)
+  }
+
+  lazy val functions: List[Fun] =
+    Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
 
 
-  /* method invocation */
+  /* invoke function */
 
   object Tag extends Enumeration
   {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
-  def method(name: String, arg: String): (Tag.Value, String) =
-    Exn.capture { get_method(name) } match {
-      case Exn.Res(f) =>
-        Exn.capture { f(arg) } match {
+  def function(name: String, arg: String): (Tag.Value, String) =
+    functions.collectFirst({ case fun if fun.name == name => fun.fn }) match {
+      case Some(fn) =>
+        Exn.capture { fn(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
-      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
+      case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
     }
 }
 
 
 /* protocol handler */
 
 class Scala extends Session.Protocol_Handler
 {
   private var session: Session = null
   private var futures = Map.empty[String, Future[Unit]]
 
   override def init(init_session: Session): Unit =
     synchronized { session = init_session }
 
   override def exit(): Unit = synchronized
   {
     for ((id, future) <- futures) cancel(id, future)
     futures = Map.empty
   }
 
   private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit =
     synchronized
     {
       if (futures.isDefinedAt(id)) {
         session.protocol_command("Scala.fulfill", id, tag.id.toString, res)
         futures -= id
       }
     }
 
   private def cancel(id: String, future: Future[Unit])
   {
     future.cancel
     fulfill(id, Scala.Tag.INTERRUPT, "")
   }
 
   private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
           Future.fork {
-            val (tag, result) = Scala.method(name, msg.text)
+            val (tag, result) = Scala.function(name, msg.text)
             fulfill(id, tag, result)
           })
         true
       case _ => false
     }
   }
 
   private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Cancel_Scala(id) =>
         futures.get(id) match {
           case Some(future) => cancel(id, future)
           case None =>
         }
         true
       case _ => false
     }
   }
 
   val functions =
     List(
       Markup.Invoke_Scala.name -> invoke_scala,
       Markup.Cancel_Scala.name -> cancel_scala)
 }
+
+
+/* registered functions */
+
+class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service
+
+class Functions extends Isabelle_Scala_Functions(
+  Scala.Fun("echo", identity),
+  Scala.Fun.yxml("echo_yxml", identity),
+  Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))
diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML
+++ b/src/Pure/Thy/bibtex.ML
@@ -1,64 +1,64 @@
 (*  Title:      Pure/Thy/bibtex.ML
     Author:     Makarius
 
 BibTeX support.
 *)
 
 signature BIBTEX =
 sig
   val check_database:
     Position.T -> string -> (string * Position.T) list * (string * Position.T) list
   val check_database_output: Position.T -> string -> unit
   val cite_macro: string Config.T
 end;
 
 structure Bibtex: BIBTEX =
 struct
 
 (* check database *)
 
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  Scala.method "isabelle.Bibtex.check_database_yxml" database
+  Scala.function "check_bibtex_database" database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
   |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
 
 fun check_database_output pos0 database =
   let val (errors, warnings) = check_database pos0 database in
     errors |> List.app (fn (msg, pos) =>
       Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
     warnings |> List.app (fn (msg, pos) =>
       warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
   end;
 
 
 (* document antiquotations *)
 
 val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
 
 val _ =
   Theory.setup
    (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
     Thy_Output.antiquotation_raw \<^binding>\<open>cite\<close>
       (Scan.lift
         (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position))
       (fn ctxt => fn (opt, citations) =>
         let
           val thy = Proof_Context.theory_of ctxt;
           val bibtex_entries = Present.get_bibtex_entries thy;
           val _ =
             if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then ()
             else
               citations |> List.app (fn (name, pos) =>
                 if member (op =) bibtex_entries name then ()
                 else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
           val _ =
             Context_Position.reports ctxt
               (map (fn (name, pos) => (pos, Markup.citation name)) citations);
           val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
           val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
         in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
 
 end;