diff --git a/src/Doc/System/Scala.thy b/src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy
+++ b/src/Doc/System/Scala.thy
@@ -1,339 +1,337 @@
 (*:maxLineLen=78:*)
 
 theory Scala
 imports Base
 begin
 
 chapter \<open>Isabelle/Scala systems programming \label{sec:scala}\<close>
 
 text \<open>
   Isabelle/ML and Isabelle/Scala are the two main implementation languages of
   the Isabelle environment:
 
     \<^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.
 
     \<^item> Isabelle/Scala is for \<^emph>\<open>physics\<close>, to connect with the world of systems
     and services, including editors and IDE frameworks.
 
   There are various ways to access Isabelle/Scala modules and operations:
 
     \<^item> Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate
     Java process.
 
     \<^item> Isabelle/ML antiquotations access Isabelle/Scala functions
     (\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"}
     operates on the running Java application, using the Scala
     read-eval-print-loop (REPL).
 
   The main Isabelle/Scala functionality is provided by \<^verbatim>\<open>Pure.jar\<close>, but
   further add-ons are bundled with Isabelle, e.g.\ to access SQLite or
   PostgreSQL using JDBC (Java Database Connectivity).
 
   Other components may augment the system environment by providing a suitable
   \<^path>\<open>etc/settings\<close> shell script in the component directory. Some shell
   functions are available to help with that:
 
     \<^item> Function \<^bash_function>\<open>classpath\<close> adds \<^verbatim>\<open>jar\<close> files in Isabelle path
     notation (POSIX). On Windows, this is converted to native path names
     before invoking @{tool java} or @{tool scala} (\secref{sec:scala-tools}).
 
     \<^item> Function \<^bash_function>\<open>isabelle_scala_service\<close> registers global
     service providers as subclasses of
     \<^scala_type>\<open>isabelle.Isabelle_System.Service\<close>, using the raw Java name
     according to @{scala_method (in java.lang.Object) getClass} (it should be
     enclosed in single quotes to avoid special characters like \<^verbatim>\<open>$\<close> to be
     interpreted by the shell).
 
     Particular Isabelle/Scala services require particular subclasses:
     instances are filtered according to their dynamic type. For example, class
     \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> collects Scala command-line
     tools, and class \<^scala_type>\<open>isabelle.Scala.Functions\<close>
     collects Scala functions (\secref{sec:scala-functions}).
 \<close>
 
 
 section \<open>Command-line tools \label{sec:scala-tools}\<close>
 
 subsection \<open>Java Runtime Environment \label{sec:tool-java}\<close>
 
 text \<open>
   The @{tool_def java} tool is a direct wrapper for the Java Runtime
   Environment, within the regular Isabelle settings environment
   (\secref{sec:settings}) and Isabelle classpath. The command line arguments
   are that of the bundled Java distribution: see option \<^verbatim>\<open>-help\<close> in
   particular.
 
   The \<^verbatim>\<open>java\<close> executable is taken from @{setting ISABELLE_JDK_HOME}, according
   to the standard directory layout for regular distributions of OpenJDK.
 
   The shell function \<^bash_function>\<open>isabelle_jdk\<close> allows shell scripts to
   invoke other Java tools robustly (e.g.\ \<^verbatim>\<open>isabelle_jdk jar\<close>), without
   depending on accidental operating system installations.
 \<close>
 
 
 subsection \<open>Scala toplevel \label{sec:tool-scala}\<close>
 
 text \<open>
   The @{tool_def scala} tool is a direct wrapper for the Scala toplevel,
   similar to @{tool java} above. The command line arguments are that of the
   bundled Scala distribution: see option \<^verbatim>\<open>-help\<close> in particular. This allows
   to interact with Isabelle/Scala interactively.
 \<close>
 
 subsubsection \<open>Example\<close>
 
 text \<open>
   Explore the Isabelle system environment in Scala:
   @{verbatim [display, indent = 2] \<open>$ isabelle scala\<close>}
   @{scala [display, indent = 2]
 \<open>import isabelle._
 
 val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
 
 val options = Options.init()
 options.bool("browser_info")
 options.string("document")\<close>}
 \<close>
 
 
 subsection \<open>Scala compiler \label{sec:tool-scalac}\<close>
 
 text \<open>
   The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
   also @{tool scala} above. The command line arguments are that of the
   bundled Scala distribution.
 
   This allows to compile further Scala modules, depending on existing
   Isabelle/Scala functionality. The resulting \<^verbatim>\<open>class\<close> or \<^verbatim>\<open>jar\<close> files can be
   added to the Java classpath using the shell function
   \<^bash_function>\<open>classpath\<close>. Thus add-on components can register themselves
   in a modular manner, see also \secref{sec:components}.
 
   Note that Isabelle/jEdit @{cite "isabelle-jedit"} has its own mechanisms for
   adding plugin components. This needs special attention, since it overrides
   the standard Java class loader.
 \<close>
 
 
 subsection \<open>Scala script wrapper\<close>
 
 text \<open>
   The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
   allows to run Isabelle/Scala source files stand-alone programs, by using a
   suitable ``hash-bang'' line and executable file permissions. For example:
   @{verbatim [display, indent = 2] \<open>#!/usr/bin/env isabelle_scala_script\<close>}
   @{scala [display, indent = 2]
 \<open>val options = isabelle.Options.init()
 Console.println("browser_info = " + options.bool("browser_info"))
 Console.println("document = " + options.string("document"))\<close>}
 
   This assumes that the executable may be found via the @{setting PATH} from
   the process environment: this is the case when Isabelle settings are active,
   e.g.\ in the context of the main Isabelle tool wrapper
   \secref{sec:isabelle-tool}. Alternatively, the full
   \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
   form.
 \<close>
 
 
 subsection \<open>Project setup for common Scala IDEs\<close>
 
 text \<open>
   The @{tool_def scala_project} tool creates a project configuration for
   Isabelle/Scala/jEdit:
   @{verbatim [display]
 \<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
 
   Options are:
     -L           make symlinks to original scala files
 
   Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
   such as IntelliJ IDEA.\<close>}
 
   The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close>, but the
   main purpose is to import it into common Scala IDEs, such as IntelliJ
   IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the
   sources with static analysis and other hints in real-time.
 
   The specified project directory needs to be fresh. The generated files refer
   to physical file-system locations, using the path notation of the underlying
   OS platform. Thus the project needs to be recreated whenever the Isabelle
   installation is changed or moved.
 
   \<^medskip>
   By default, Scala sources are \<^emph>\<open>copied\<close> from the Isabelle distribution and
   editing them within the IDE has no permanent effect.
 
   Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
   develop Isabelle/Scala/jEdit within an external Scala IDE. Note that
   building the result always requires \<^verbatim>\<open>isabelle jedit -b\<close> on the
   command-line.
 \<close>
 
 
 section \<open>Registered Isabelle/Scala functions \label{sec:scala-functions}\<close>
 
 subsection \<open>Defining functions in Isabelle/Scala\<close>
 
 text \<open>
   A Scala functions of type \<^scala_type>\<open>String => String\<close> may be wrapped as
   \<^scala_type>\<open>isabelle.Scala.Fun\<close> and collected via an instance of the
   class \<^scala_type>\<open>isabelle.Scala.Functions\<close>. A system component
   can then register that class via \<^bash_function>\<open>isabelle_scala_service\<close>
   in \<^path>\<open>etc/settings\<close> (\secref{sec:components}). An example is the
   predefined collection of \<^scala_type>\<open>isabelle.Scala.Functions\<close> in
   Isabelle/\<^verbatim>\<open>Pure.jar\<close> with the following line in
   \<^file>\<open>$ISABELLE_HOME/etc/settings\<close>:
   @{verbatim [display, indent = 2] \<open>isabelle_scala_service 'isabelle.Functions'\<close>}
 
   The overall list of registered functions is accessible in Isabelle/Scala as
   \<^scala_object>\<open>isabelle.Scala.functions\<close>.
 \<close>
 
 
 subsection \<open>Invoking functions in Isabelle/ML\<close>
 
 text \<open>
   Isabelle/PIDE provides a protocol to invoke registered Scala functions in
   ML: this works both within the Prover IDE and in batch builds.
 
   The subsequent ML antiquotations refer to Scala functions in a
   formally-checked manner.
 
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "scala_function"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "scala"} & : & \<open>ML_antiquotation\<close> \\
-  @{ML_antiquotation_def "scala_thread"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   \<^rail>\<open>
     (@{ML_antiquotation scala_function} |
-     @{ML_antiquotation scala} |
-     @{ML_antiquotation scala_thread}) @{syntax embedded}
+     @{ML_antiquotation scala}) @{syntax embedded}
   \<close>
 
   \<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string
     literal.
 
   \<^descr> \<open>@{scala name}\<close> and \<open>@{scala_thread name}\<close> invoke the checked function via
   the PIDE protocol. In Isabelle/ML this appears as a function of type
   \<^ML_type>\<open>string -> string\<close>, which is subject to interrupts within the ML
   runtime environment as usual. A \<^scala>\<open>null\<close> result in Scala raises an
   exception \<^ML>\<open>Scala.Null\<close> in ML. The execution of \<open>@{scala}\<close> works via a
   Scala future on a bounded thread farm, while \<open>@{scala_thread}\<close> always forks
   a separate Java thread.
 
   The standard approach of representing datatypes via strings works via XML in
   YXML transfer syntax. See Isabelle/ML operations and modules @{ML
   YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode},
   @{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols
   may have to be recoded via Scala operations
   \<^scala_method>\<open>isabelle.Symbol.decode\<close> and
   \<^scala_method>\<open>isabelle.Symbol.encode\<close>.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Invoke the predefined Scala function \<^scala_function>\<open>echo\<close>:
 \<close>
 
 ML \<open>
   val s = "test";
   val s' = \<^scala>\<open>echo\<close> s;
   \<^assert> (s = s')
 \<close>
 
 text \<open>
   Let the Scala compiler process some toplevel declarations, producing a list
   of errors:
 \<close>
 
 ML \<open>
   val source = "class A(a: Int, b: Boolean)"
   val errors =
     \<^scala>\<open>scala_toplevel\<close> source
     |> YXML.parse_body
     |> let open XML.Decode in list string end;
 
   \<^assert> (null errors)\<close>
 
 text \<open>
   The above is merely for demonstration. See \<^ML>\<open>Scala_Compiler.toplevel\<close>
   for a more convenient version with builtin decoding and treatment of errors.
 \<close>
 
 
 section \<open>Documenting Isabelle/Scala entities\<close>
 
 text \<open>
   The subsequent document antiquotations help to document Isabelle/Scala
   entities, with formal checking of names against the Isabelle classpath.
 
   \begin{matharray}{rcl}
   @{antiquotation_def "scala"} & : & \<open>antiquotation\<close> \\
   @{antiquotation_def "scala_object"} & : & \<open>antiquotation\<close> \\
   @{antiquotation_def "scala_type"} & : & \<open>antiquotation\<close> \\
   @{antiquotation_def "scala_method"} & : & \<open>antiquotation\<close> \\
   \end{matharray}
 
   \<^rail>\<open>
     (@@{antiquotation scala} | @@{antiquotation scala_object})
       @{syntax embedded}
     ;
     @@{antiquotation scala_type} @{syntax embedded} types
     ;
     @@{antiquotation scala_method} class @{syntax embedded} types args
     ;
     class: ('(' @'in' @{syntax name} types ')')?
     ;
     types: ('[' (@{syntax name} ',' +) ']')?
     ;
     args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')?
   \<close>
 
   \<^descr> \<open>@{scala s}\<close> is similar to \<open>@{verbatim s}\<close>, but the given source text is
   checked by the Scala compiler as toplevel declaration (without evaluation).
   This allows to write Isabelle/Scala examples that are statically checked.
 
   \<^descr> \<open>@{scala_object x}\<close> checks the given Scala object name (simple value or
   ground module) and prints the result verbatim.
 
   \<^descr> \<open>@{scala_type T[A]}\<close> checks the given Scala type name (with optional type
   parameters) and prints the result verbatim.
 
   \<^descr> \<open>@{scala_method (in c[A]) m[B](n)}\<close> checks the given Scala method \<open>m\<close> in
   the context of class \<open>c\<close>. The method argument slots are either specified by
   a number \<open>n\<close> or by a list of (optional) argument types; this may refer to
   type variables specified for the class or method: \<open>A\<close> or \<open>B\<close> above.
 
   Everything except for the method name \<open>m\<close> is optional. The absence of the
   class context means that this is a static method. The absence of arguments
   with types means that the method can be determined uniquely as \<^verbatim>\<open>(\<close>\<open>m\<close>\<^verbatim>\<open> _)\<close>
   in Scala (no overloading).
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Miscellaneous Isabelle/Scala entities:
 
     \<^item> object: \<^scala_object>\<open>isabelle.Isabelle_Process\<close>
     \<^item> type without parameter: @{scala_type isabelle.Console_Progress}
     \<^item> type with parameter: @{scala_type List[A]}
     \<^item> static method: \<^scala_method>\<open>isabelle.Isabelle_System.bash\<close>
     \<^item> class and method with type parameters:
       @{scala_method (in List[A]) map[B]("A => B")}
     \<^item> overloaded method with argument type: @{scala_method (in Int) "+" (Int)}
 \<close>
 
 end
diff --git a/src/HOL/Tools/ATP/system_on_tptp.ML b/src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML
@@ -1,20 +1,20 @@
 (*  Title:      HOL/Tools/ATP/system_on_tptp.ML
     Author:     Makarius
 
 Support for remote ATPs via SystemOnTPTP.
 *)
 
 signature SYSTEM_ON_TPTP =
 sig
   val get_url: unit -> string
   val list_systems: unit -> string list
 end
 
 structure SystemOnTPTP: SYSTEM_ON_TPTP =
 struct
 
 fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close>
 
-fun list_systems () = get_url () |> \<^scala_thread>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
+fun list_systems () = get_url () |> \<^scala>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
 
 end
diff --git a/src/HOL/Tools/ATP/system_on_tptp.scala b/src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala
@@ -1,37 +1,37 @@
 /*  Title:      HOL/Tools/ATP/system_on_tptp.scala
     Author:     Makarius
 
 Support for remote ATPs via SystemOnTPTP.
 */
 
 package isabelle.atp
 
 import isabelle._
 
 import java.net.URL
 
 
 object SystemOnTPTP
 {
   def get_url(options: Options): URL = Url(options.string("SystemOnTPTP"))
 
   def proper_lines(text: String): List[String] =
     Library.trim_split_lines(text).filterNot(_.startsWith("%"))
 
   def list_systems(url: URL): List[String] =
   {
     val result =
       HTTP.Client.post(url, user_agent = "Sledgehammer", parameters =
         List("NoHTML" -> 1,
           "QuietFlag" -> "-q0",
           "SubmitButton" -> "ListSystems",
           "ListStatus" -> "READY"))
     proper_lines(result.text)
   }
 
-  object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems")
+  object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
   {
     val here = Scala_Project.here
     def apply(url: String): String = cat_lines(list_systems(Url(url)))
   }
 }
diff --git a/src/HOL/Tools/Nitpick/kodkod.ML b/src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML
+++ b/src/HOL/Tools/Nitpick/kodkod.ML
@@ -1,1095 +1,1095 @@
 (*  Title:      HOL/Tools/Nitpick/kodkod.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2008-2014
 
 ML interface for Kodkod.
 *)
 
 signature KODKOD =
 sig
   type n_ary_index = int * int
   type setting = string * string
 
   datatype tuple =
     Tuple of int list |
     TupleIndex of n_ary_index |
     TupleReg of n_ary_index
 
   datatype tuple_set =
     TupleUnion of tuple_set * tuple_set |
     TupleDifference of tuple_set * tuple_set |
     TupleIntersect of tuple_set * tuple_set |
     TupleProduct of tuple_set * tuple_set |
     TupleProject of tuple_set * int |
     TupleSet of tuple list |
     TupleRange of tuple * tuple |
     TupleArea of tuple * tuple |
     TupleAtomSeq of int * int |
     TupleSetReg of n_ary_index
 
   datatype tuple_assign =
     AssignTuple of n_ary_index * tuple |
     AssignTupleSet of n_ary_index * tuple_set
 
   type bound = (n_ary_index * string) list * tuple_set list
   type int_bound = int option * tuple_set list
 
   datatype formula =
     All of decl list * formula |
     Exist of decl list * formula |
     FormulaLet of expr_assign list * formula |
     FormulaIf of formula * formula * formula |
     Or of formula * formula |
     Iff of formula * formula |
     Implies of formula * formula |
     And of formula * formula |
     Not of formula |
     Acyclic of n_ary_index |
     Function of n_ary_index * rel_expr * rel_expr |
     Functional of n_ary_index * rel_expr * rel_expr |
     TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
     Subset of rel_expr * rel_expr |
     RelEq of rel_expr * rel_expr |
     IntEq of int_expr * int_expr |
     LT of int_expr * int_expr |
     LE of int_expr * int_expr |
     No of rel_expr |
     Lone of rel_expr |
     One of rel_expr |
     Some of rel_expr |
     False |
     True |
     FormulaReg of int
   and rel_expr =
     RelLet of expr_assign list * rel_expr |
     RelIf of formula * rel_expr * rel_expr |
     Union of rel_expr * rel_expr |
     Difference of rel_expr * rel_expr |
     Override of rel_expr * rel_expr |
     Intersect of rel_expr * rel_expr |
     Product of rel_expr * rel_expr |
     IfNo of rel_expr * rel_expr |
     Project of rel_expr * int_expr list |
     Join of rel_expr * rel_expr |
     Closure of rel_expr |
     ReflexiveClosure of rel_expr |
     Transpose of rel_expr |
     Comprehension of decl list * formula |
     Bits of int_expr |
     Int of int_expr |
     Iden |
     Ints |
     None |
     Univ |
     Atom of int |
     AtomSeq of int * int |
     Rel of n_ary_index |
     Var of n_ary_index |
     RelReg of n_ary_index
   and int_expr =
     Sum of decl list * int_expr |
     IntLet of expr_assign list * int_expr |
     IntIf of formula * int_expr * int_expr |
     SHL of int_expr * int_expr |
     SHA of int_expr * int_expr |
     SHR of int_expr * int_expr |
     Add of int_expr * int_expr |
     Sub of int_expr * int_expr |
     Mult of int_expr * int_expr |
     Div of int_expr * int_expr |
     Mod of int_expr * int_expr |
     Cardinality of rel_expr |
     SetSum of rel_expr |
     BitOr of int_expr * int_expr |
     BitXor of int_expr * int_expr |
     BitAnd of int_expr * int_expr |
     BitNot of int_expr |
     Neg of int_expr |
     Absolute of int_expr |
     Signum of int_expr |
     Num of int |
     IntReg of int
   and decl =
     DeclNo of n_ary_index * rel_expr |
     DeclLone of n_ary_index * rel_expr |
     DeclOne of n_ary_index * rel_expr |
     DeclSome of n_ary_index * rel_expr |
     DeclSet of n_ary_index * rel_expr
   and expr_assign =
     AssignFormulaReg of int * formula |
     AssignRelReg of n_ary_index * rel_expr |
     AssignIntReg of int * int_expr
 
   type 'a fold_expr_funcs =
     {formula_func: formula -> 'a -> 'a,
      rel_expr_func: rel_expr -> 'a -> 'a,
      int_expr_func: int_expr -> 'a -> 'a}
 
   val kodkodi_version : unit -> int list
 
   val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
   val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
   val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a
   val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
   val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
 
   type 'a fold_tuple_funcs =
     {tuple_func: tuple -> 'a -> 'a,
      tuple_set_func: tuple_set -> 'a -> 'a}
 
   val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
   val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
   val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a
   val fold_bound :
       'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
   val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
 
   type problem =
     {comment: string,
      settings: setting list,
      univ_card: int,
      tuple_assigns: tuple_assign list,
      bounds: bound list,
      int_bounds: int_bound list,
      expr_assigns: expr_assign list,
      formula: formula}
 
   type raw_bound = n_ary_index * int list list
 
   datatype outcome =
     Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
     Error of string * int list
 
   exception SYNTAX of string * string
 
   val max_arity : int -> int
   val arity_of_rel_expr : rel_expr -> int
   val is_problem_trivially_false : problem -> bool
   val problems_equivalent : problem * problem -> bool
   val solve_any_problem :
     bool -> bool -> Time.time -> int -> int -> problem list -> outcome
 end;
 
 structure Kodkod : KODKOD =
 struct
 
 type n_ary_index = int * int
 
 type setting = string * string
 
 datatype tuple =
   Tuple of int list |
   TupleIndex of n_ary_index |
   TupleReg of n_ary_index
 
 datatype tuple_set =
   TupleUnion of tuple_set * tuple_set |
   TupleDifference of tuple_set * tuple_set |
   TupleIntersect of tuple_set * tuple_set |
   TupleProduct of tuple_set * tuple_set |
   TupleProject of tuple_set * int |
   TupleSet of tuple list |
   TupleRange of tuple * tuple |
   TupleArea of tuple * tuple |
   TupleAtomSeq of int * int |
   TupleSetReg of n_ary_index
 
 datatype tuple_assign =
   AssignTuple of n_ary_index * tuple |
   AssignTupleSet of n_ary_index * tuple_set
 
 type bound = (n_ary_index * string) list * tuple_set list
 type int_bound = int option * tuple_set list
 
 datatype formula =
   All of decl list * formula |
   Exist of decl list * formula |
   FormulaLet of expr_assign list * formula |
   FormulaIf of formula * formula * formula |
   Or of formula * formula |
   Iff of formula * formula |
   Implies of formula * formula |
   And of formula * formula |
   Not of formula |
   Acyclic of n_ary_index |
   Function of n_ary_index * rel_expr * rel_expr |
   Functional of n_ary_index * rel_expr * rel_expr |
   TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
   Subset of rel_expr * rel_expr |
   RelEq of rel_expr * rel_expr |
   IntEq of int_expr * int_expr |
   LT of int_expr * int_expr |
   LE of int_expr * int_expr |
   No of rel_expr |
   Lone of rel_expr |
   One of rel_expr |
   Some of rel_expr |
   False |
   True |
   FormulaReg of int
 and rel_expr =
   RelLet of expr_assign list * rel_expr |
   RelIf of formula * rel_expr * rel_expr |
   Union of rel_expr * rel_expr |
   Difference of rel_expr * rel_expr |
   Override of rel_expr * rel_expr |
   Intersect of rel_expr * rel_expr |
   Product of rel_expr * rel_expr |
   IfNo of rel_expr * rel_expr |
   Project of rel_expr * int_expr list |
   Join of rel_expr * rel_expr |
   Closure of rel_expr |
   ReflexiveClosure of rel_expr |
   Transpose of rel_expr |
   Comprehension of decl list * formula |
   Bits of int_expr |
   Int of int_expr |
   Iden |
   Ints |
   None |
   Univ |
   Atom of int |
   AtomSeq of int * int |
   Rel of n_ary_index |
   Var of n_ary_index |
   RelReg of n_ary_index
 and int_expr =
   Sum of decl list * int_expr |
   IntLet of expr_assign list * int_expr |
   IntIf of formula * int_expr * int_expr |
   SHL of int_expr * int_expr |
   SHA of int_expr * int_expr |
   SHR of int_expr * int_expr |
   Add of int_expr * int_expr |
   Sub of int_expr * int_expr |
   Mult of int_expr * int_expr |
   Div of int_expr * int_expr |
   Mod of int_expr * int_expr |
   Cardinality of rel_expr |
   SetSum of rel_expr |
   BitOr of int_expr * int_expr |
   BitXor of int_expr * int_expr |
   BitAnd of int_expr * int_expr |
   BitNot of int_expr |
   Neg of int_expr |
   Absolute of int_expr |
   Signum of int_expr |
   Num of int |
   IntReg of int
 and decl =
   DeclNo of n_ary_index * rel_expr |
   DeclLone of n_ary_index * rel_expr |
   DeclOne of n_ary_index * rel_expr |
   DeclSome of n_ary_index * rel_expr |
   DeclSet of n_ary_index * rel_expr
 and expr_assign =
   AssignFormulaReg of int * formula |
   AssignRelReg of n_ary_index * rel_expr |
   AssignIntReg of int * int_expr
 
 type problem =
   {comment: string,
    settings: setting list,
    univ_card: int,
    tuple_assigns: tuple_assign list,
    bounds: bound list,
    int_bounds: int_bound list,
    expr_assigns: expr_assign list,
    formula: formula}
 
 type raw_bound = n_ary_index * int list list
 
 datatype outcome =
   Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
   Error of string * int list
 
 exception SYNTAX of string * string
 
 type 'a fold_expr_funcs =
   {formula_func: formula -> 'a -> 'a,
    rel_expr_func: rel_expr -> 'a -> 'a,
    int_expr_func: int_expr -> 'a -> 'a}
 
 fun kodkodi_version () =
   getenv "KODKODI_VERSION"
   |> space_explode "."
   |> map (the_default 0 o Int.fromString)
 
 
 (** Auxiliary functions on Kodkod problems **)
 
 fun fold_formula (F : 'a fold_expr_funcs) formula =
   case formula of
     All (ds, f) => fold (fold_decl F) ds #> fold_formula F f
   | Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f
   | FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f
   | FormulaIf (f, f1, f2) =>
     fold_formula F f #> fold_formula F f1 #> fold_formula F f2
   | Or (f1, f2) => fold_formula F f1 #> fold_formula F f2
   | Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2
   | Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2
   | And (f1, f2) => fold_formula F f1 #> fold_formula F f2
   | Not f => fold_formula F f
   | Acyclic x => fold_rel_expr F (Rel x)
   | Function (x, r1, r2) =>
     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
   | Functional (x, r1, r2) =>
     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
   | TotalOrdering (x, r1, r2, r3) =>
     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
     #> fold_rel_expr F r3
   | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | No r => fold_rel_expr F r
   | Lone r => fold_rel_expr F r
   | One r => fold_rel_expr F r
   | Some r => fold_rel_expr F r
   | False => #formula_func F formula
   | True => #formula_func F formula
   | FormulaReg _ => #formula_func F formula
 and fold_rel_expr F rel_expr =
   case rel_expr of
     RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r
   | RelIf (f, r1, r2) =>
     fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2
   | Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is
   | Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   | Closure r => fold_rel_expr F r
   | ReflexiveClosure r => fold_rel_expr F r
   | Transpose r => fold_rel_expr F r
   | Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f
   | Bits i => fold_int_expr F i
   | Int i => fold_int_expr F i
   | Iden => #rel_expr_func F rel_expr
   | Ints => #rel_expr_func F rel_expr
   | None => #rel_expr_func F rel_expr
   | Univ => #rel_expr_func F rel_expr
   | Atom _ => #rel_expr_func F rel_expr
   | AtomSeq _ => #rel_expr_func F rel_expr
   | Rel _ => #rel_expr_func F rel_expr
   | Var _ => #rel_expr_func F rel_expr
   | RelReg _ => #rel_expr_func F rel_expr
 and fold_int_expr F int_expr =
   case int_expr of
     Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i
   | IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i
   | IntIf (f, i1, i2) =>
     fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2
   | SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | Cardinality r => fold_rel_expr F r
   | SetSum r => fold_rel_expr F r
   | BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   | BitNot i => fold_int_expr F i
   | Neg i => fold_int_expr F i
   | Absolute i => fold_int_expr F i
   | Signum i => fold_int_expr F i
   | Num _ => #int_expr_func F int_expr
   | IntReg _ => #int_expr_func F int_expr
 and fold_decl F decl =
   case decl of
     DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   | DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   | DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   | DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   | DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
 and fold_expr_assign F assign =
   case assign of
     AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f
   | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
   | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
 
 type 'a fold_tuple_funcs =
   {tuple_func: tuple -> 'a -> 'a,
    tuple_set_func: tuple_set -> 'a -> 'a}
 
 fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
 
 fun fold_tuple_set F tuple_set =
   case tuple_set of
     TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   | TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   | TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   | TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   | TupleProject (ts, _) => fold_tuple_set F ts
   | TupleSet ts => fold (fold_tuple F) ts
   | TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
   | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
   | TupleAtomSeq _ => #tuple_set_func F tuple_set
   | TupleSetReg _ => #tuple_set_func F tuple_set
 
 fun fold_tuple_assign F assign =
   case assign of
     AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
   | AssignTupleSet (x, ts) =>
     fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts
 
 fun fold_bound expr_F tuple_F (zs, tss) =
   fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
   #> fold (fold_tuple_set tuple_F) tss
 
 fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss
 
 fun max_arity univ_card = floor (Math.ln 2147483647.0
                                  / Math.ln (Real.fromInt univ_card))
 
 fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
   | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
   | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Project (_, is)) = length is
   | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
   | arity_of_rel_expr (Closure _) = 2
   | arity_of_rel_expr (ReflexiveClosure _) = 2
   | arity_of_rel_expr (Transpose _) = 2
   | arity_of_rel_expr (Comprehension (ds, _)) =
     fold (curry op + o arity_of_decl) ds 0
   | arity_of_rel_expr (Bits _) = 1
   | arity_of_rel_expr (Int _) = 1
   | arity_of_rel_expr Iden = 2
   | arity_of_rel_expr Ints = 1
   | arity_of_rel_expr None = 1
   | arity_of_rel_expr Univ = 1
   | arity_of_rel_expr (Atom _) = 1
   | arity_of_rel_expr (AtomSeq _) = 1
   | arity_of_rel_expr (Rel (n, _)) = n
   | arity_of_rel_expr (Var (n, _)) = n
   | arity_of_rel_expr (RelReg (n, _)) = n
 and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2
 and arity_of_decl (DeclNo ((n, _), _)) = n
   | arity_of_decl (DeclLone ((n, _), _)) = n
   | arity_of_decl (DeclOne ((n, _), _)) = n
   | arity_of_decl (DeclSome ((n, _), _)) = n
   | arity_of_decl (DeclSet ((n, _), _)) = n
 
 fun is_problem_trivially_false ({formula = False, ...} : problem) = true
   | is_problem_trivially_false _ = false
 
 val chop_solver = take 2 o space_explode ","
 
 fun settings_equivalent ([], []) = true
   | settings_equivalent ((key1, value1) :: settings1,
                          (key2, value2) :: settings2) =
     key1 = key2 andalso
     (value1 = value2 orelse key1 = "delay" orelse
      (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso
     settings_equivalent (settings1, settings2)
   | settings_equivalent _ = false
 
 fun problems_equivalent (p1 : problem, p2 : problem) =
   #univ_card p1 = #univ_card p2 andalso
   #formula p1 = #formula p2 andalso
   #bounds p1 = #bounds p2 andalso
   #expr_assigns p1 = #expr_assigns p2 andalso
   #tuple_assigns p1 = #tuple_assigns p2 andalso
   #int_bounds p1 = #int_bounds p2 andalso
   settings_equivalent (#settings p1, #settings p2)
 
 (** Serialization of problem **)
 
 fun base_name j =
   if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
 
 fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
   | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
   | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j
 
 fun atom_name j = "A" ^ base_name j
 fun atom_seq_name (k, 0) = "u" ^ base_name k
   | atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0
 fun formula_reg_name j = "$f" ^ base_name j
 fun rel_reg_name j = "$e" ^ base_name j
 fun int_reg_name j = "$i" ^ base_name j
 
 fun tuple_name x = n_ary_name x "A" "P" "T"
 fun rel_name x = n_ary_name x "s" "r" "m"
 fun var_name x = n_ary_name x "S" "R" "M"
 fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
 fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
 
 fun inline_comment "" = ""
   | inline_comment comment =
     " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
     " */"
 
 fun block_comment "" = ""
   | block_comment comment = prefix_lines "// " comment ^ "\n"
 
 fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
 
 fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
   | string_for_tuple (TupleIndex x) = tuple_name x
   | string_for_tuple (TupleReg x) = tuple_reg_name x
 
 val no_prec = 100
 val prec_TupleUnion = 1
 val prec_TupleIntersect = 2
 val prec_TupleProduct = 3
 val prec_TupleProject = 4
 
 fun precedence_ts (TupleUnion _) = prec_TupleUnion
   | precedence_ts (TupleDifference _) = prec_TupleUnion
   | precedence_ts (TupleIntersect _) = prec_TupleIntersect
   | precedence_ts (TupleProduct _) = prec_TupleProduct
   | precedence_ts (TupleProject _) = prec_TupleProject
   | precedence_ts _ = no_prec
 
 fun string_for_tuple_set tuple_set =
   let
     fun sub tuple_set outer_prec =
       let
         val prec = precedence_ts tuple_set
         val need_parens = (prec < outer_prec)
       in
         (if need_parens then "(" else "") ^
         (case tuple_set of
            TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
          | TupleDifference (ts1, ts2) =>
            sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
          | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
          | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
          | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
          | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
          | TupleRange (t1, t2) =>
            "{" ^ string_for_tuple t1 ^
            (if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}"
          | TupleArea (t1, t2) =>
            "{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}"
          | TupleAtomSeq x => atom_seq_name x
          | TupleSetReg x => tuple_set_reg_name x) ^
         (if need_parens then ")" else "")
       end
   in sub tuple_set 0 end
 
 fun string_for_tuple_assign (AssignTuple (x, t)) =
     tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n"
   | string_for_tuple_assign (AssignTupleSet (x, ts)) =
     tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
 
 fun string_for_bound (zs, tss) =
   "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
   (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
   (if length tss = 1 then "" else "]") ^ "\n"
 
 fun int_string_for_bound (opt_n, tss) =
   (case opt_n of
      SOME n => signed_string_of_int n ^ ": "
    | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"
 
 val prec_All = 1
 val prec_Or = 2
 val prec_Iff = 3
 val prec_Implies = 4
 val prec_And = 5
 val prec_Not = 6
 val prec_Eq = 7
 val prec_Some = 8
 val prec_SHL = 9
 val prec_Add = 10
 val prec_Mult = 11
 val prec_Override = 12
 val prec_Intersect = 13
 val prec_Product = 14
 val prec_IfNo = 15
 val prec_Project = 17
 val prec_Join = 18
 val prec_BitNot = 19
 
 fun precedence_f (All _) = prec_All
   | precedence_f (Exist _) = prec_All
   | precedence_f (FormulaLet _) = prec_All
   | precedence_f (FormulaIf _) = prec_All
   | precedence_f (Or _) = prec_Or
   | precedence_f (Iff _) = prec_Iff
   | precedence_f (Implies _) = prec_Implies
   | precedence_f (And _) = prec_And
   | precedence_f (Not _) = prec_Not
   | precedence_f (Acyclic _) = no_prec
   | precedence_f (Function _) = no_prec
   | precedence_f (Functional _) = no_prec
   | precedence_f (TotalOrdering _) = no_prec
   | precedence_f (Subset _) = prec_Eq
   | precedence_f (RelEq _) = prec_Eq
   | precedence_f (IntEq _) = prec_Eq
   | precedence_f (LT _) = prec_Eq
   | precedence_f (LE _) = prec_Eq
   | precedence_f (No _) = prec_Some
   | precedence_f (Lone _) = prec_Some
   | precedence_f (One _) = prec_Some
   | precedence_f (Some _) = prec_Some
   | precedence_f False = no_prec
   | precedence_f True = no_prec
   | precedence_f (FormulaReg _) = no_prec
 and precedence_r (RelLet _) = prec_All
   | precedence_r (RelIf _) = prec_All
   | precedence_r (Union _) = prec_Add
   | precedence_r (Difference _) = prec_Add
   | precedence_r (Override _) = prec_Override
   | precedence_r (Intersect _) = prec_Intersect
   | precedence_r (Product _) = prec_Product
   | precedence_r (IfNo _) = prec_IfNo
   | precedence_r (Project _) = prec_Project
   | precedence_r (Join _) = prec_Join
   | precedence_r (Closure _) = prec_BitNot
   | precedence_r (ReflexiveClosure _) = prec_BitNot
   | precedence_r (Transpose _) = prec_BitNot
   | precedence_r (Comprehension _) = no_prec
   | precedence_r (Bits _) = no_prec
   | precedence_r (Int _) = no_prec
   | precedence_r Iden = no_prec
   | precedence_r Ints = no_prec
   | precedence_r None = no_prec
   | precedence_r Univ = no_prec
   | precedence_r (Atom _) = no_prec
   | precedence_r (AtomSeq _) = no_prec
   | precedence_r (Rel _) = no_prec
   | precedence_r (Var _) = no_prec
   | precedence_r (RelReg _) = no_prec
 and precedence_i (Sum _) = prec_All
   | precedence_i (IntLet _) = prec_All
   | precedence_i (IntIf _) = prec_All
   | precedence_i (SHL _) = prec_SHL
   | precedence_i (SHA _) = prec_SHL
   | precedence_i (SHR _) = prec_SHL
   | precedence_i (Add _) = prec_Add
   | precedence_i (Sub _) = prec_Add
   | precedence_i (Mult _) = prec_Mult
   | precedence_i (Div _) = prec_Mult
   | precedence_i (Mod _) = prec_Mult
   | precedence_i (Cardinality _) = no_prec
   | precedence_i (SetSum _) = no_prec
   | precedence_i (BitOr _) = prec_Intersect
   | precedence_i (BitXor _) = prec_Intersect
   | precedence_i (BitAnd _) = prec_Intersect
   | precedence_i (BitNot _) = prec_BitNot
   | precedence_i (Neg _) = prec_BitNot
   | precedence_i (Absolute _) = prec_BitNot
   | precedence_i (Signum _) = prec_BitNot
   | precedence_i (Num _) = no_prec
   | precedence_i (IntReg _) = no_prec
 
 fun write_problem out problems =
   let
     fun out_outmost_f (And (f1, f2)) =
         (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
       | out_outmost_f f = out_f f prec_And
     and out_f formula outer_prec =
       let
         val prec = precedence_f formula
         val need_parens = (prec < outer_prec)
       in
         (if need_parens then out "(" else ());
         (case formula of
            All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec)
          | Exist (ds, f) =>
            (out "some ["; out_decls ds; out "] | "; out_f f prec)
          | FormulaLet (bs, f) =>
            (out "let ["; out_assigns bs; out "] | "; out_f f prec)
          | FormulaIf (f, f1, f2) =>
            (out "if "; out_f f prec; out " then "; out_f f1 prec; out " else ";
             out_f f2 prec)
          | Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec)
          | Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec)
          | Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec)
          | And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec)
          | Not f => (out "! "; out_f f prec)
          | Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")")
          | Function (x, r1, r2) =>
            (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one ";
             out_r r2 0; out ")")
          | Functional (x, r1, r2) =>
            (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
             out_r r2 0; out ")")
          | TotalOrdering (x, r1, r2, r3) =>
            (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", ";
             out_r r2 0; out ", "; out_r r3 0; out ")")
          | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
          | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
          | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
          | LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec)
          | LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec)
          | No r => (out "no "; out_r r prec)
          | Lone r => (out "lone "; out_r r prec)
          | One r => (out "one "; out_r r prec)
          | Some r => (out "some "; out_r r prec)
          | False => out "false"
          | True => out "true"
          | FormulaReg j => out (formula_reg_name j));
         (if need_parens then out ")" else ())
       end
     and out_r rel_expr outer_prec =
       let
         val prec = precedence_r rel_expr
         val need_parens = (prec < outer_prec)
       in
         (if need_parens then out "(" else ());
         (case rel_expr of
            RelLet (bs, r) =>
            (out "let ["; out_assigns bs; out "] | "; out_r r prec)
          | RelIf (f, r1, r2) =>
            (out "if "; out_f f prec; out " then "; out_r r1 prec;
             out " else "; out_r r2 prec)
          | Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1))
          | Difference (r1, r2) =>
            (out_r r1 prec; out " - "; out_r r2 (prec + 1))
          | Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec)
          | Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec)
          | Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec)
          | IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec)
          | Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]")
          | Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1))
          | Closure r => (out "^"; out_r r prec)
          | ReflexiveClosure r => (out "*"; out_r r prec)
          | Transpose r => (out "~"; out_r r prec)
          | Comprehension (ds, f) =>
            (out "{["; out_decls ds; out "] | "; out_f f 0; out "}")
          | Bits i => (out "Bits["; out_i i 0; out "]")
          | Int i => (out "Int["; out_i i 0; out "]")
          | Iden => out "iden"
          | Ints => out "ints"
          | None => out "none"
          | Univ => out "univ"
          | Atom j => out (atom_name j)
          | AtomSeq x => out (atom_seq_name x)
          | Rel x => out (rel_name x)
          | Var x => out (var_name x)
          | RelReg (_, j) => out (rel_reg_name j));
         (if need_parens then out ")" else ())
       end
     and out_i int_expr outer_prec =
       let
         val prec = precedence_i int_expr
         val need_parens = (prec < outer_prec)
       in
         (if need_parens then out "(" else ());
         (case int_expr of
            Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec)
          | IntLet (bs, i) =>
            (out "let ["; out_assigns bs; out "] | "; out_i i prec)
          | IntIf (f, i1, i2) =>
            (out "if "; out_f f prec; out " then "; out_i i1 prec;
             out " else "; out_i i2 prec)
          | SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1))
          | SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1))
          | SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1))
          | Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1))
          | Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1))
          | Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1))
          | Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1))
          | Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1))
          | Cardinality r => (out "#("; out_r r 0; out ")")
          | SetSum r => (out "sum("; out_r r 0; out ")")
          | BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec)
          | BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec)
          | BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec)
          | BitNot i => (out "~"; out_i i prec)
          | Neg i => (out "-"; out_i i prec)
          | Absolute i => (out "abs "; out_i i prec)
          | Signum i => (out "sgn "; out_i i prec)
          | Num k => out (signed_string_of_int k)
          | IntReg j => out (int_reg_name j));
         (if need_parens then out ")" else ())
       end
     and out_decls [] = ()
       | out_decls [d] = out_decl d
       | out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds)
     and out_decl (DeclNo (x, r)) =
         (out (var_name x); out " : no "; out_r r 0)
       | out_decl (DeclLone (x, r)) =
         (out (var_name x); out " : lone "; out_r r 0)
       | out_decl (DeclOne (x, r)) =
         (out (var_name x); out " : one "; out_r r 0)
       | out_decl (DeclSome (x, r)) =
         (out (var_name x); out " : some "; out_r r 0)
       | out_decl (DeclSet (x, r)) =
         (out (var_name x); out " : set "; out_r r 0)
     and out_assigns [] = ()
       | out_assigns [b] = out_assign b
       | out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs)
     and out_assign (AssignFormulaReg (j, f)) =
         (out (formula_reg_name j); out " := "; out_f f 0)
       | out_assign (AssignRelReg ((_, j), r)) =
         (out (rel_reg_name j); out " := "; out_r r 0)
       | out_assign (AssignIntReg (j, i)) =
         (out (int_reg_name j); out " := "; out_i i 0)
     and out_columns [] = ()
       | out_columns [i] = out_i i 0
       | out_columns (i :: is) = (out_i i 0; out ", "; out_columns is)
     and out_problem {comment, settings, univ_card, tuple_assigns, bounds,
                      int_bounds, expr_assigns, formula} =
         (out ("\n" ^ block_comment comment ^
               implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n")
                             settings) ^
               "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
               implode (map string_for_tuple_assign tuple_assigns) ^
               implode (map string_for_bound bounds) ^
               (if int_bounds = [] then
                  ""
                else
                  "int_bounds: " ^
                  commas (map int_string_for_bound int_bounds) ^ "\n"));
          List.app (fn b => (out_assign b; out ";")) expr_assigns;
          out "solve "; out_outmost_f formula; out ";\n")
   in
     out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
          "// " ^ ATP_Util.timestamp () ^ "\n");
     List.app out_problem problems
   end
 
 (** Parsing of solution **)
 
 fun is_ident_char s =
   Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
   s = "_" orelse s = "'" orelse s = "$"
 
 fun strip_blanks [] = []
   | strip_blanks (" " :: ss) = strip_blanks ss
   | strip_blanks [s1, " "] = [s1]
   | strip_blanks (s1 :: " " :: s2 :: ss) =
     if is_ident_char s1 andalso is_ident_char s2 then
       s1 :: " " :: strip_blanks (s2 :: ss)
     else
       strip_blanks (s1 :: s2 :: ss)
   | strip_blanks (s :: ss) = s :: strip_blanks ss
 
 val scan_nat =
   Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
   >> (the o Int.fromString o implode)
 val scan_rel_name =
   ($$ "s" |-- scan_nat >> pair 1
    || $$ "r" |-- scan_nat >> pair 2
    || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
   >> (fn ((n, j), SOME _) => (n, ~j - 1)
        | ((n, j), NONE) => (n, j))
 val scan_atom = $$ "A" |-- scan_nat
 fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
 fun parse_list scan = parse_non_empty_list scan || Scan.succeed []
 val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]"
 val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]"
 val parse_assignment = (scan_rel_name --| $$ "=") -- parse_tuple_set
 val parse_instance =
   Scan.this_string "relations:"
   |-- $$ "{" |-- parse_list parse_assignment --| $$ "}"
 
 val extract_instance =
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ =>
                                 raise SYNTAX ("Kodkod.extract_instance",
                                               "ill-formed Kodkodi output"))
                             parse_instance))
   o strip_blanks o raw_explode
 
 val problem_marker = "*** PROBLEM "
 val outcome_marker = "---OUTCOME---\n"
 val instance_marker = "---INSTANCE---\n"
 
 fun read_section_body marker =
   Substring.string o fst o Substring.position "\n\n"
   o Substring.triml (size marker)
 
 fun read_next_instance s =
   let val s = Substring.position instance_marker s |> snd in
     if Substring.isEmpty s then
       raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
     else
       read_section_body instance_marker s |> extract_instance
   end
 
 fun read_next_outcomes j (s, ps, js) =
   let val (s1, s2) = Substring.position outcome_marker s in
     if Substring.isEmpty s2 orelse
        not (Substring.isEmpty (Substring.position problem_marker s1
                                |> snd)) then
       (s, ps, js)
     else
       let
         val outcome = read_section_body outcome_marker s2
         val s = Substring.triml (size outcome_marker) s2
       in
         if String.isSuffix "UNSATISFIABLE" outcome then
           read_next_outcomes j (s, ps, j :: js)
         else if String.isSuffix "SATISFIABLE" outcome then
           read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
         else
           raise SYNTAX ("Kodkod.read_next_outcomes",
                         "unknown outcome " ^ quote outcome)
       end
   end
 
 fun read_next_problems (s, ps, js) =
   let val s = Substring.position problem_marker s |> snd in
     if Substring.isEmpty s then
       (ps, js)
     else
       let
         val s = Substring.triml (size problem_marker) s
         val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
                          |> Int.fromString |> the
         val j = j_plus_1 - 1
       in read_next_problems (read_next_outcomes j (s, ps, js)) end
   end
   handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
                                         "expected number after \"PROBLEM\"")
 
 
 (** Main Kodkod entry point **)
 
 fun serial_string_and_temporary_dir overlord =
   if overlord then ("", getenv "ISABELLE_HOME_USER")
   else (serial_string (), getenv "ISABELLE_TMP")
 
 (* The fudge term below is to account for Kodkodi's slow start-up time, which
    is partly due to the JVM and partly due to the ML "bash" function. *)
 val fudge_ms = 250
 
 fun uncached_solve_any_problem overlord deadline max_threads0 max_solutions problems =
   let
     val j = find_index (curry (op =) True o #formula) problems
     val indexed_problems = if j >= 0 then
                              [(j, nth problems j)]
                            else
                              filter_out (is_problem_trivially_false o snd)
                                         (0 upto length problems - 1 ~~ problems)
     val triv_js = filter_out (AList.defined (op =) indexed_problems)
                              (0 upto length problems - 1)
     val reindex = fst o nth indexed_problems
 
     val max_threads =
       if max_threads0 = 0
       then Options.default_int \<^system_option>\<open>kodkod_max_threads\<close>
       else max_threads0
 
     val external_process =
       not (Options.default_bool \<^system_option>\<open>kodkod_scala\<close>) orelse overlord
     val timeout0 = Time.toMilliseconds (deadline - Time.now ())
     val timeout = if external_process then timeout0 - fudge_ms else timeout0
 
     val solve_all = max_solutions > 1
   in
     if null indexed_problems then
       Normal ([], triv_js, "")
     else if timeout <= 0 then TimedOut triv_js
     else
       let
         val kki =
           let
             val buf = Unsynchronized.ref Buffer.empty
             fun out s = Unsynchronized.change buf (Buffer.add s)
             val _ = write_problem out (map snd indexed_problems)
           in Buffer.content (! buf) end
         val (rc, out, err) =
           if external_process then
             let
               val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord
               fun path_for suf = Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
               val kki_path = path_for "kki"
               val out_path = path_for "out"
               val err_path = path_for "err"
 
               fun remove_temporary_files () =
                 if overlord then ()
                 else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
             in
               let
                 val _ = File.write kki_path kki
                 val rc =
                   Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
                     \\"$KODKODI/bin/kodkodi\"" ^
                     (" -max-msecs " ^ string_of_int timeout) ^
                     (if solve_all then " -solve-all" else "") ^
                     " -max-solutions " ^ string_of_int max_solutions ^
                     (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
                     " < " ^ File.bash_path kki_path ^
                     " > " ^ File.bash_path out_path ^
                     " 2> " ^ File.bash_path err_path)
                 val out = File.read out_path
                 val err = File.read err_path
                 val _ = remove_temporary_files ()
               in (rc, out, err) end
               handle exn => (remove_temporary_files (); Exn.reraise exn)
             end
           else
             (timeout, (solve_all, (max_solutions, (max_threads, kki))))
             |> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end
             |> YXML.string_of_body
-            |> \<^scala_thread>\<open>kodkod\<close>
+            |> \<^scala>\<open>kodkod\<close>
             |> YXML.parse_body
             |> let open XML.Decode in triple int string string end
 
         val (ps, nontriv_js) =
           read_next_problems (Substring.full out, [], [])
           |>> rev ||> rev
           |> apfst (map (apfst reindex)) |> apsnd (map reindex)
         val js = triv_js @ nontriv_js
 
         val first_error =
           trim_split_lines err
           |> map
            (perhaps (try (unsuffix ".")) #>
             perhaps (try (unprefix "Solve error: ")) #>
             perhaps (try (unprefix "Error: ")))
           |> find_first (fn line => line <> "" andalso line <> "EXIT")
           |> the_default ""
       in
         if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
         else if rc = 2 then TimedOut js
         else if rc = 130 then raise Exn.Interrupt
         else Error (if first_error = "" then "Unknown error" else first_error, js)
       end
   end
 
 val cached_outcome =
   Synchronized.var "Kodkod.cached_outcome"
                    (NONE : ((int * problem list) * outcome) option)
 
 fun solve_any_problem debug overlord deadline max_threads max_solutions
                       problems =
   let
     fun do_solve () =
       uncached_solve_any_problem overlord deadline max_threads max_solutions
                                  problems
   in
     if debug orelse overlord then
       do_solve ()
     else
       case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
                             max1 = max2 andalso length ps1 = length ps2 andalso
                             forall problems_equivalent (ps1 ~~ ps2))
                         (the_list (Synchronized.value cached_outcome))
                         (max_solutions, problems) of
         SOME outcome => outcome
       | NONE =>
         let val outcome = do_solve () in
           (case outcome of
              Normal (_, _, "") =>
              Synchronized.change cached_outcome
                                  (K (SOME ((max_solutions, problems), outcome)))
            | _ => ());
           outcome
         end
   end
 
 end;
diff --git a/src/HOL/Tools/Nitpick/kodkod.scala b/src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala
+++ b/src/HOL/Tools/Nitpick/kodkod.scala
@@ -1,178 +1,178 @@
 /*  Title:      HOL/Tools/Nitpick/kodkod.scala
     Author:     Makarius
 
 Scala interface for Kodkod.
 */
 
 package isabelle.nitpick
 
 import isabelle._
 
 import java.util.concurrent.{TimeUnit, LinkedBlockingQueue, ThreadPoolExecutor}
 
 import org.antlr.runtime.{ANTLRInputStream, RecognitionException}
 import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
 
 
 object Kodkod
 {
   /** result **/
 
   sealed case class Result(rc: Int, out: String, err: String)
   {
     def ok: Boolean = rc == 0
     def check: String =
       if (ok) out else error(if (err.isEmpty) "Error" else err)
 
     def encode: XML.Body =
     {
       import XML.Encode._
       triple(int, string, string)((rc, out, err))
     }
   }
 
 
 
   /** execute **/
 
   def execute(source: String,
     solve_all: Boolean = false,
     prove: Boolean = false,
     max_solutions: Int = Integer.MAX_VALUE,
     cleanup_inst: Boolean = false,
     timeout: Time = Time.zero,
     max_threads: Int = 0): Result =
   {
     /* executor */
 
     val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
     val executor: ThreadPoolExecutor =
       new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS,
         new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy)
 
     val executor_killed = Synchronized(false)
     def executor_kill(): Unit =
       executor_killed.change(b =>
         if (b) b else { Isabelle_Thread.fork() { executor.shutdownNow() }; true })
 
 
     /* system context */
 
     class Exit extends Exception("EXIT")
 
     class Exec_Context extends Context
     {
       private var rc = 0
       private val out = new StringBuilder
       private val err = new StringBuilder
 
       def return_code(i: Int): Unit = synchronized { rc = rc max i}
 
       override def output(s: String): Unit = synchronized {
         Exn.Interrupt.expose()
         out ++= s
         out += '\n'
       }
 
       override def error(s: String): Unit = synchronized {
         Exn.Interrupt.expose()
         err ++= s
         err += '\n'
       }
 
       override def exit(i: Int): Unit =
         synchronized {
           return_code(i)
           executor_kill()
           throw new Exit
         }
 
       def result(): Result = synchronized { Result(rc, out.toString, err.toString) }
     }
 
     val context = new Exec_Context
 
 
     /* main */
 
     try {
       val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream()))
       val parser =
         KodkodiParser.create(context, executor,
           false, solve_all, prove, max_solutions, cleanup_inst, lexer)
 
       val timeout_request =
         if (timeout.is_zero) None
         else {
           Some(Event_Timer.request(Time.now() + timeout) {
             context.error("Ran out of time")
             context.return_code(2)
             executor_kill()
           })
         }
 
       try { parser.problems() }
       catch { case exn: RecognitionException => parser.reportError(exn) }
 
       timeout_request.foreach(_.cancel())
 
       if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
         context.error("Error: trailing tokens")
         context.exit(1)
       }
       if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) {
         context.exit(1)
       }
     }
     catch {
       case _: Exit =>
       case exn: Throwable =>
         val message = exn.getMessage
         context.error(if (message.isEmpty) exn.toString else "Error: " + message)
         context.return_code(1)
     }
 
     executor.shutdownNow()
 
     context.result()
   }
 
 
   /** protocol handler **/
 
   def warmup(): String =
     execute(
       "solver: \"MiniSat\"\n" +
       File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
 
   class Handler extends Session.Protocol_Handler
   {
     override def init(session: Session): Unit = warmup()
   }
 
 
 
   /** scala function **/
 
-  object Fun extends Scala.Fun("kodkod")
+  object Fun extends Scala.Fun("kodkod", thread = true)
   {
     val here = Scala_Project.here
     def apply(args: String): String =
     {
       val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) =
       {
         import XML.Decode._
         pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args))
       }
       val result =
         execute(kki,
           solve_all = solve_all,
           max_solutions = max_solutions,
           timeout = Time.ms(timeout),
           max_threads = max_threads)
       YXML.string_of_body(result.encode)
     }
   }
 }
 
 class Scala_Functions extends Scala.Functions(Kodkod.Fun)
diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML
+++ b/src/Pure/PIDE/markup.ML
@@ -1,786 +1,785 @@
 (*  Title:      Pure/PIDE/markup.ML
     Author:     Makarius
 
 Quasi-abstract markup elements.
 *)
 
 signature MARKUP =
 sig
   type T = string * Properties.T
   val empty: T
   val is_empty: T -> bool
   val properties: Properties.T -> T -> T
   val nameN: string val name: string -> T -> T
   val xnameN: string val xname: string -> T -> T
   val kindN: string
   val serialN: string
   val serial_properties: int -> Properties.T
   val instanceN: string
   val meta_titleN: string val meta_title: T
   val meta_creatorN: string val meta_creator: T
   val meta_contributorN: string val meta_contributor: T
   val meta_dateN: string val meta_date: T
   val meta_licenseN: string val meta_license: T
   val meta_descriptionN: string val meta_description: T
   val languageN: string
   val symbolsN: string
   val delimitedN: string
   val is_delimited: Properties.T -> bool
   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
   val language_Isar: bool -> T
   val language_method: T
   val language_attribute: T
   val language_sort: bool -> T
   val language_type: bool -> T
   val language_term: bool -> T
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
   val language_document: bool -> T
   val language_document_marker: T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_verbatim: bool -> T
   val language_latex: bool -> T
   val language_rail: T
   val language_path: bool -> T
   val language_url: bool -> T
   val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val defN: string
   val refN: string
   val completionN: string val completion: T
   val no_completionN: string val no_completion: T
   val updateN: string val update: T
   val lineN: string
   val end_lineN: string
   val offsetN: string
   val end_offsetN: string
   val fileN: string
   val idN: string
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
   val toolN: string val tool: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
   val block_properties: string list
   val indentN: string
   val widthN: string
   val blockN: string val block: bool -> int -> T
   val breakN: string val break: int -> int -> T
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
   val bash_functionN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
   val classN: string
   val type_nameN: string
   val constantN: string
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val literal_factN: string val literal_fact: string -> T
   val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
   val skolemN: string val skolem: T
   val boundN: string val bound: T
   val varN: string val var: T
   val numeralN: string val numeral: T
   val literalN: string val literal: T
   val delimiterN: string val delimiter: T
   val inner_stringN: string val inner_string: T
   val inner_cartoucheN: string val inner_cartouche: T
   val token_rangeN: string val token_range: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
   val class_parameterN: string val class_parameter: T
   val ML_keyword1N: string val ML_keyword1: T
   val ML_keyword2N: string val ML_keyword2: T
   val ML_keyword3N: string val ML_keyword3: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
   val ML_charN: string val ML_char: T
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
   val ML_defN: string
   val ML_openN: string
   val ML_structureN: string
   val ML_typingN: string val ML_typing: T
   val ML_breakpointN: string val ML_breakpoint: int -> T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val file_typeN: string
   val antiquotationN: string
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
   val raw_textN: string val raw_text: T
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val document_markerN: string val document_marker: T
   val document_tagN: string val document_tag: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
   val markdown_listN: string val markdown_list: string -> T
   val itemizeN: string
   val enumerateN: string
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
   val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
   val quasi_keywordN: string val quasi_keyword: T
   val improperN: string val improper: T
   val operatorN: string val operator: T
   val comment1N: string val comment1: T
   val comment2N: string val comment2: T
   val comment3N: string val comment3: T
   val elapsedN: string
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val command_indentN: string val command_indent: int -> T
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
   val forkedN: string val forked: T
   val joinedN: string val joined: T
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val canceledN: string val canceled: T
   val initializedN: string val initialized: T
   val finalizedN: string val finalized: T
   val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
   val statusN: string val status: T
   val resultN: string val result: T
   val writelnN: string val writeln: T
   val stateN: string val state: T
   val informationN: string val information: T
   val tracingN: string val tracing: T
   val warningN: string val warning: T
   val legacyN: string val legacy: T
   val errorN: string val error: T
   val systemN: string val system: T
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
   val theory_exportsN: string
   val sendbackN: string
   val paddingN: string
   val padding_line: Properties.entry
   val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
   val ML_statistics: {pid: int, stats_dir: string} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
-  val invoke_scala: string -> string -> bool -> Properties.T
+  val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val build_session_finished: Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
   val exportN: string
   type export_args =
    {id: string option,
     serial: serial,
     theory_name: string,
     name: string,
     executable: bool,
     compress: bool,
     strict: bool}
   val export: export_args -> Properties.T
   val debugger_state: string -> Properties.T
   val debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
   val simp_trace_hintN: string
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
   type output = Output.output * Output.output
   val no_output: output
   val add_mode: string -> (T -> output) -> unit
   val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
   val markup_only: T -> string
   val markup_report: string -> string
 end;
 
 structure Markup: MARKUP =
 struct
 
 (** markup elements **)
 
 (* basic markup *)
 
 type T = string * Properties.T;
 
 val empty = ("", []);
 
 fun is_empty ("", _) = true
   | is_empty _ = false;
 
 
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev Properties.put more_props props);
 
 fun markup_elem name = (name, (name, []): T);
 fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
 fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T);
 
 
 (* misc properties *)
 
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
 val xnameN = "xname";
 fun xname a = properties [(xnameN, a)];
 
 val kindN = "kind";
 
 val serialN = "serial";
 fun serial_properties i = [(serialN, Value.print_int i)];
 
 val instanceN = "instance";
 
 
 (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *)
 
 val (meta_titleN, meta_title) = markup_elem "meta_title";
 val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
 val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
 val (meta_dateN, meta_date) = markup_elem "meta_date";
 val (meta_licenseN, meta_license) = markup_elem "meta_license";
 val (meta_descriptionN, meta_description) = markup_elem "meta_description";
 
 
 (* embedded languages *)
 
 val languageN = "language";
 val symbolsN = "symbols";
 val antiquotesN = "antiquotes";
 val delimitedN = "delimited"
 
 fun is_delimited props =
   Properties.get props delimitedN = SOME "true";
 
 fun language {name, symbols, antiquotes, delimited} =
   (languageN,
    [(nameN, name),
     (symbolsN, Value.print_bool symbols),
     (antiquotesN, Value.print_bool antiquotes),
     (delimitedN, Value.print_bool delimited)]);
 
 fun language' {name, symbols, antiquotes} delimited =
   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
 
 val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
 val language_method =
   language {name = "method", symbols = true, antiquotes = false, delimited = false};
 val language_attribute =
   language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
 val language_type = language' {name = "type", symbols = true, antiquotes = false};
 val language_term = language' {name = "term", symbols = true, antiquotes = false};
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_document_marker =
   language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
 val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
 val language_latex = language' {name = "latex", symbols = false, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language' {name = "path", symbols = false, antiquotes = false};
 val language_url = language' {name = "url", symbols = false, antiquotes = false};
 val language_mixfix =
   language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
 
 val (bindingN, binding) = markup_elem "binding";
 
 val entityN = "entity";
 fun entity kind name =
   (entityN,
     (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
 val defN = "def";
 val refN = "ref";
 
 
 (* completion *)
 
 val (completionN, completion) = markup_elem "completion";
 val (no_completionN, no_completion) = markup_elem "no_completion";
 
 val (updateN, update) = markup_elem "update";
 
 
 (* position *)
 
 val lineN = "line";
 val end_lineN = "end_line";
 
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 
 val fileN = "file";
 val idN = "id";
 
 val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 val (positionN, position) = markup_elem "position";
 
 
 (* expression *)
 
 val expressionN = "expression";
 fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
 
 
 (* citation *)
 
 val (citationN, citation) = markup_string "citation" nameN;
 
 
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
 val (toolN, tool) = markup_string "tool" nameN;
 
 
 (* pretty printing *)
 
 val markupN = "markup";
 val consistentN = "consistent";
 val unbreakableN = "unbreakable";
 val indentN = "indent";
 
 val block_properties = [markupN, consistentN, unbreakableN, indentN];
 
 val widthN = "width";
 
 val blockN = "block";
 fun block c i =
   (blockN,
     (if c then [(consistentN, Value.print_bool c)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val breakN = "break";
 fun break w i =
   (breakN,
     (if w <> 0 then [(widthN, Value.print_int w)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
 val (itemN, item) = markup_elem "item";
 
 
 (* text properties *)
 
 val (wordsN, words) = markup_elem "words";
 
 val (hiddenN, hidden) = markup_elem "hidden";
 
 val (deleteN, delete) = markup_elem "delete";
 
 
 (* misc entities *)
 
 val bash_functionN = "bash_function";
 val scala_functionN = "scala_function";
 val system_optionN = "system_option";
 
 val sessionN = "session";
 
 val theoryN = "theory";
 val classN = "class";
 val type_nameN = "type_name";
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
 
 val method_modifierN = "method_modifier";
 
 
 (* inner syntax *)
 
 val (tfreeN, tfree) = markup_elem "tfree";
 val (tvarN, tvar) = markup_elem "tvar";
 val (freeN, free) = markup_elem "free";
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
 val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
 val (delimiterN, delimiter) = markup_elem "delimiter";
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
 
 val (token_rangeN, token_range) = markup_elem "token_range";
 
 val (sortingN, sorting) = markup_elem "sorting";
 val (typingN, typing) = markup_elem "typing";
 val (class_parameterN, class_parameter) = markup_elem "class_parameter";
 
 
 (* ML *)
 
 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
 val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
 val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3";
 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
 val ML_structureN = "ML_structure";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN;
 
 
 (* antiquotations *)
 
 val (antiquotedN, antiquoted) = markup_elem "antiquoted";
 val (antiquoteN, antiquote) = markup_elem "antiquote";
 
 val file_typeN = "file_type";
 val antiquotationN = "antiquotation";
 val ML_antiquotationN = "ML_antiquotation";
 val document_antiquotationN = "document_antiquotation";
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
 (* document text *)
 
 val (raw_textN, raw_text) = markup_elem "raw_text";
 val (plain_textN, plain_text) = markup_elem "plain_text";
 
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 val (document_markerN, document_marker) = markup_elem "document_marker";
 val (document_tagN, document_tag) = markup_string "document_tag" nameN;
 
 
 (* Markdown document structure *)
 
 val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
 val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
 val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
 val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
 
 val itemizeN = "itemize";
 val enumerateN = "enumerate";
 val descriptionN = "description";
 
 
 (* formal input *)
 
 val inputN = "input";
 fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props);
 
 
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
 
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
 val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
 val (improperN, improper) = markup_elem "improper";
 val (operatorN, operator) = markup_elem "operator";
 val (stringN, string) = markup_elem "string";
 val (alt_stringN, alt_string) = markup_elem "alt_string";
 val (verbatimN, verbatim) = markup_elem "verbatim";
 val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 
 
 (* comments *)
 
 val (comment1N, comment1) = markup_elem "comment1";
 val (comment2N, comment2) = markup_elem "comment2";
 val (comment3N, comment3) = markup_elem "comment3";
 
 
 (* timing *)
 
 val elapsedN = "elapsed";
 val cpuN = "cpu";
 val gcN = "gc";
 
 fun timing_properties {elapsed, cpu, gc} =
  [(elapsedN, Value.print_time elapsed),
   (cpuN, Value.print_time cpu),
   (gcN, Value.print_time gc)];
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 
 
 (* command timing *)
 
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
       SOME ({file = file, offset = Value.parse_int offset, name = name},
         Properties.seconds props elapsedN)
   | _ => NONE);
 
 
 (* indentation *)
 
 val (command_indentN, command_indent) = markup_int "command_indent" indentN;
 
 
 (* goals *)
 
 val (goalN, goal) = markup_elem "goal";
 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 
 
 (* command status *)
 
 val taskN = "task";
 
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
 val (canceledN, canceled) = markup_elem "canceled";
 val (initializedN, initialized) = markup_elem "initialized";
 val (finalizedN, finalized) = markup_elem "finalized";
 val (consolidatingN, consolidating) = markup_elem "consolidating";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
 (* messages *)
 
 val exec_idN = "exec_id";
 
 val initN = "init";
 val (statusN, status) = markup_elem "status";
 val (resultN, result) = markup_elem "result";
 val (writelnN, writeln) = markup_elem "writeln";
 val (stateN, state) = markup_elem "state"
 val (informationN, information) = markup_elem "information";
 val (tracingN, tracing) = markup_elem "tracing";
 val (warningN, warning) = markup_elem "warning";
 val (legacyN, legacy) = markup_elem "legacy";
 val (errorN, error) = markup_elem "error";
 val (systemN, system) = markup_elem "system";
 val protocolN = "protocol";
 
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
 val badN = "bad";
 fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";
 
 
 (* active areas *)
 
 val browserN = "browser"
 val graphviewN = "graphview";
 val theory_exportsN = "theory_exports";
 
 val sendbackN = "sendback";
 val paddingN = "padding";
 val padding_line = (paddingN, "line");
 val padding_command = (paddingN, "command");
 
 val dialogN = "dialog";
 fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]);
 
 val jedit_actionN = "jedit_action";
 
 
 (* protocol message functions *)
 
 val functionN = "function"
 
 fun ML_statistics {pid, stats_dir} =
   [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
 
 val commands_accepted = [(functionN, "commands_accepted")];
 
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
-fun invoke_scala name id thread =
-  [(functionN, "invoke_scala"), (nameN, name), (idN, id), ("thread", Value.print_bool thread)];
+fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
 val task_statistics = (functionN, "task_statistics");
 
 val command_timing = (functionN, "command_timing");
 
 val theory_timing = (functionN, "theory_timing");
 
 val session_timing = (functionN, "session_timing");
 
 fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
 
 val build_session_finished = [("function", "build_session_finished")];
 
 val print_operationsN = "print_operations";
 val print_operations = [(functionN, print_operationsN)];
 
 
 (* export *)
 
 val exportN = "export";
 
 type export_args =
  {id: string option,
   serial: serial,
   theory_name: string,
   name: string,
   executable: bool,
   compress: bool,
   strict: bool};
 
 fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) =
  [(functionN, exportN),
   (idN, the_default "" id),
   (serialN, Value.print_int serial),
   ("theory_name", theory_name),
   (nameN, name),
   ("executable", Value.print_bool executable),
   ("compress", Value.print_bool compress),
   ("strict", Value.print_bool strict)];
 
 
 (* debugger *)
 
 fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
 fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
 
 
 (* simplifier trace *)
 
 val simp_trace_panelN = "simp_trace_panel";
 
 val simp_trace_logN = "simp_trace_log";
 val simp_trace_stepN = "simp_trace_step";
 val simp_trace_recurseN = "simp_trace_recurse";
 val simp_trace_hintN = "simp_trace_hint";
 val simp_trace_ignoreN = "simp_trace_ignore";
 
 fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)];
 
 
 
 (** print mode operations **)
 
 type output = Output.output * Output.output;
 
 val no_output = ("", "");
 
 local
   val default = {output = Output_Primitives.markup_fn};
   val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
 in
   fun add_mode name output =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
        else Output.warning ("Redefining markup mode " ^ quote name);
        Symtab.update (name, {output = output}) tab));
   fun get_mode () =
     the_default default
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
 fun markup m =
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
 val markups = fold_rev markup;
 
 fun markup_only m = markup m "";
 
 fun markup_report "" = ""
   | markup_report txt = markup report txt;
 
 end;
diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala
+++ b/src/Pure/PIDE/markup.scala
@@ -1,740 +1,739 @@
 /*  Title:      Pure/PIDE/markup.scala
     Author:     Makarius
 
 Quasi-abstract markup elements.
 */
 
 package isabelle
 
 
 object Markup
 {
   /* elements */
 
   object Elements
   {
     def apply(elems: Set[String]): Elements = new Elements(elems)
     def apply(elems: String*): Elements = apply(Set(elems: _*))
     val empty: Elements = apply()
     val full: Elements =
       new Elements(Set.empty)
       {
         override def apply(elem: String): Boolean = true
         override def toString: String = "Elements.full"
       }
   }
 
   sealed class Elements private[Markup](private val rep: Set[String])
   {
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     def - (elem: String): Elements = new Elements(rep - elem)
     def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     override def toString: String = rep.mkString("Elements(", ",", ")")
   }
 
 
   /* properties */
 
   val NAME = "name"
   val Name = new Properties.String(NAME)
 
   val XNAME = "xname"
   val XName = new Properties.String(XNAME)
 
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
   val CONTENT = "content"
   val Content = new Properties.String(CONTENT)
 
   val SERIAL = "serial"
   val Serial = new Properties.Long(SERIAL)
 
   val INSTANCE = "instance"
   val Instance = new Properties.String(INSTANCE)
 
 
   /* basic markup */
 
   val Empty: Markup = Markup("", Nil)
   val Broken: Markup = Markup("broken", Nil)
 
   class Markup_String(val name: String, prop: String)
   {
     private val Prop = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Int(val name: String, prop: String)
   {
     private val Prop = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Long(val name: String, prop: String)
   {
     private val Prop = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
 
   /* meta data */
 
   val META_TITLE = "meta_title"
   val META_CREATOR = "meta_creator"
   val META_CONTRIBUTOR = "meta_contributor"
   val META_DATE = "meta_date"
   val META_LICENSE = "meta_license"
   val META_DESCRIPTION = "meta_description"
 
 
   /* formal entities */
 
   val BINDING = "binding"
   val ENTITY = "entity"
 
   val Def = new Properties.Long("def")
   val Ref = new Properties.Long("ref")
 
   object Entity
   {
     object Def
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
     }
     object Ref
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
     }
     object Occ
     {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
     }
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
           val kind = Kind.unapply(props).getOrElse("")
           val name = Name.unapply(props).getOrElse("")
           Some((kind, name))
         case _ => None
       }
   }
 
 
   /* completion */
 
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
   val UPDATE = "update"
 
 
   /* position */
 
   val LINE = "line"
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
   val POSITION = "position"
 
 
   /* expression */
 
   val EXPRESSION = "expression"
   object Expression
   {
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(EXPRESSION, Kind(kind)) => Some(kind)
         case Markup(EXPRESSION, _) => Some("")
         case _ => None
       }
   }
 
 
   /* citation */
 
   val CITATION = "citation"
   val Citation = new Markup_String(CITATION, NAME)
 
 
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
   val Antiquotes = new Properties.Boolean("antiquotes")
   val Delimited = new Properties.Boolean("delimited")
 
   val LANGUAGE = "language"
   object Language
   {
     val DOCUMENT = "document"
     val ML = "ML"
     val SML = "SML"
     val PATH = "path"
     val UNKNOWN = "unknown"
 
     def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
               Some((name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
 
     object Path
     {
       def unapply(markup: Markup): Option[Boolean] =
         markup match {
           case Language(PATH, _, _, delimited) => Some(delimited)
           case _ => None
         }
     }
   }
 
 
   /* external resources */
 
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
   val EXPORT_PATH = "export_path"
   val Export_Path = new Markup_String(EXPORT_PATH, NAME)
 
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 
   val DOC = "doc"
   val Doc = new Markup_String(DOC, NAME)
 
 
   /* pretty printing */
 
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
   object Block
   {
     val name = "block"
     def apply(c: Boolean, i: Int): Markup =
       Markup(name,
         (if (c) Consistent(c) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
         val c = Consistent.unapply(markup.properties).getOrElse(false)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((c, i))
       }
       else None
   }
 
   object Break
   {
     val name = "break"
     def apply(w: Int, i: Int): Markup =
       Markup(name,
         (if (w != 0) Width(w) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Int, Int)] =
       if (markup.name == name) {
         val w = Width.unapply(markup.properties).getOrElse(0)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((w, i))
       }
       else None
   }
 
   val ITEM = "item"
   val BULLET = "bullet"
 
   val SEPARATOR = "separator"
 
 
   /* text properties */
 
   val WORDS = "words"
 
   val HIDDEN = "hidden"
 
   val DELETE = "delete"
 
 
   /* misc entities */
 
   val THEORY = "theory"
   val CLASS = "class"
   val TYPE_NAME = "type_name"
   val FIXED = "fixed"
   val CASE = "case"
   val CONSTANT = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
 
 
   /* inner syntax */
 
   val TFREE = "tfree"
   val TVAR = "tvar"
   val FREE = "free"
   val SKOLEM = "skolem"
   val BOUND = "bound"
   val VAR = "var"
   val NUMERAL = "numeral"
   val LITERAL = "literal"
   val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"
   val INNER_CARTOUCHE = "inner_cartouche"
 
   val TOKEN_RANGE = "token_range"
 
   val SORTING = "sorting"
   val TYPING = "typing"
   val CLASS_PARAMETER = "class_parameter"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
 
 
   /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"
 
   val ML_ANTIQUOTATION = "ML_antiquotation"
   val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
   /* document text */
 
   val RAW_TEXT = "raw_text"
   val PLAIN_TEXT = "plain_text"
 
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
   object Document_Tag
   {
     val ELEMENT = "document_tag"
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
 
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(ELEMENT, Name(name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* Markdown document structure */
 
   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
   val MARKDOWN_ITEM = "markdown_item"
   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   val Markdown_List = new Markup_String("markdown_list", "kind")
 
   val ITEMIZE = "itemize"
   val ENUMERATE = "enumerate"
   val DESCRIPTION = "description"
 
 
   /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"
   val ML_KEYWORD2 = "ML_keyword2"
   val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
   val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
   val ML_BREAKPOINT = "ML_breakpoint"
 
 
   /* outer syntax */
 
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
   val QUASI_KEYWORD = "quasi_keyword"
   val IMPROPER = "improper"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALT_STRING = "alt_string"
   val VERBATIM = "verbatim"
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
   val LOAD_COMMAND = "load_command"
 
 
   /* comments */
 
   val COMMENT1 = "comment1"
   val COMMENT2 = "comment2"
   val COMMENT3 = "comment3"
 
 
   /* timing */
 
   val Elapsed = new Properties.Double("elapsed")
   val CPU = new Properties.Double("cpu")
   val GC = new Properties.Double("gc")
 
   object Timing_Properties
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
           Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
 
     def parse(props: Properties.T): isabelle.Timing =
       unapply(props) getOrElse isabelle.Timing.zero
   }
 
   val TIMING = "timing"
 
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
 
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
         case _ => None
       }
   }
 
 
   /* process result */
 
   val Return_Code = new Properties.Int("return_code")
 
   object Process_Result
   {
     def apply(result: Process_Result): Properties.T =
       Return_Code(result.rc) :::
         (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
 
     def unapply(props: Properties.T): Option[Process_Result] =
       props match {
         case Return_Code(rc) =>
           val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
           Some(isabelle.Process_Result(rc, timing = timing))
         case _ => None
       }
   }
 
 
   /* command indentation */
 
   object Command_Indent
   {
     val name = "command_indent"
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Indent.unapply(markup.properties) else None
   }
 
 
   /* goals */
 
   val GOAL = "goal"
   val SUBGOAL = "subgoal"
 
 
   /* command status */
 
   val TASK = "task"
 
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
   val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val FINALIZED = "finalized"
   val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */
 
   val VERSION = "version"
   val ASSIGN = "assign"
 
 
   /* prover process */
 
   val PROVER_COMMAND = "prover_command"
   val PROVER_ARG = "prover_arg"
 
 
   /* messages */
 
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
   val RESULT = "result"
   val WRITELN = "writeln"
   val STATE = "state"
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
   val LEGACY = "legacy"
   val ERROR = "error"
   val NODES_STATUS = "nodes_status"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
   val EXIT = "exit"
 
   val WRITELN_MESSAGE = "writeln_message"
   val STATE_MESSAGE = "state_message"
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
   val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
     WRITELN -> WRITELN_MESSAGE,
     STATE -> STATE_MESSAGE,
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
     LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
 
   val INTENSIFY = "intensify"
 
 
   /* active areas */
 
   val BROWSER = "browser"
   val GRAPHVIEW = "graphview"
   val THEORY_EXPORTS = "theory_exports"
 
   val SENDBACK = "sendback"
   val PADDING = "padding"
   val PADDING_LINE = (PADDING, "line")
   val PADDING_COMMAND = (PADDING, "command")
 
   val DIALOG = "dialog"
   val Result = new Properties.String(RESULT)
 
   val JEDIT_ACTION = "jedit_action"
 
 
   /* protocol message functions */
 
   val FUNCTION = "function"
 
   class Function(val name: String)
   {
     val PROPERTY: Properties.Entry = (FUNCTION, name)
   }
 
   class Properties_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case PROPERTY :: args => Some(args)
         case _ => None
       }
   }
 
   class Name_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
   object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
         case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
     val Threads = new Properties.Int("threads")
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
 
   object Invoke_Scala extends Function("invoke_scala")
   {
-    def unapply(props: Properties.T): Option[(String, String, Boolean)] =
+    def unapply(props: Properties.T): Option[(String, String)] =
       props match {
-        case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) =>
-          Some((name, id, thread))
+        case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
   object Cancel_Scala extends Function("cancel_scala")
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (ID, id)) => Some(id)
         case _ => None
       }
   }
 
   val PRINT_OPERATIONS = "print_operations"
 
 
   /* export */
 
   val EXPORT = "export"
   val THEORY_NAME = "theory_name"
   val EXECUTABLE = "executable"
   val COMPRESS = "compress"
   val STRICT = "strict"
 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"
   object Debugger_State
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
   val SIMP_TRACE_RECURSE = "simp_trace_recurse"
   val SIMP_TRACE_HINT = "simp_trace_hint"
   val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
   val SIMP_TRACE_CANCEL = "simp_trace_cancel"
   object Simp_Trace_Cancel
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
         case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         case _ => None
       }
   }
 
 
   /* XML data representation */
 
   def encode: XML.Encode.T[Markup] = (markup: Markup) =>
   {
     import XML.Encode._
     pair(string, properties)((markup.name, markup.properties))
   }
 
   def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
   {
     import XML.Decode._
     val (name, props) = pair(string, properties)(body)
     Markup(name, props)
   }
 }
 
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
     else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))
 }
diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML
+++ b/src/Pure/PIDE/resources.ML
@@ -1,439 +1,435 @@
 (*  Title:      Pure/PIDE/resources.ML
     Author:     Makarius
 
 Resources for theories and auxiliary files.
 *)
 
 signature RESOURCES =
 sig
   val default_qualifier: string
   val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
      session_chapters: (string * string) list,
      bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
      scala_functions: (string * Position.T) list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val init_session_yxml: string -> unit
   val init_session_file: Path.T -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
   val session_chapter: string -> string
   val last_timing: Toplevel.transition -> Time.time
   val scala_functions: unit -> string list
   val check_scala_function: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
   val theory_bibtex_entries: string -> string list
   val find_theory_file: string -> Path.T option
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser
   val parse_file: (theory -> Token.file) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_file: Token.file -> theory -> theory
   val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser
   val provide_parse_file: (theory -> Token.file * theory) parser
   val loaded_files_current: theory -> bool
   val check_path: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_file: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T
 end;
 
 structure Resources: RESOURCES =
 struct
 
 (* command timings *)
 
 type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name, time*)
 
 val empty_timings: timings = Symtab.empty;
 
 fun update_timings props =
   (case Markup.parse_command_timing_properties props of
     SOME ({file, offset, name}, time) =>
       Symtab.map_default (file, Inttab.empty)
         (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
   | NONE => I);
 
 fun make_timings command_timings =
   fold update_timings command_timings empty_timings;
 
 fun approximative_id name pos =
   (case (Position.file_of pos, Position.offset_of pos) of
     (SOME file, SOME offset) =>
       if name = "" then NONE else SOME {file = file, offset = offset, name = name}
   | _ => NONE);
 
 fun get_timings timings tr =
   (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
     SOME {file, offset, name} =>
       (case Symtab.lookup timings file of
         SOME offsets =>
           (case Inttab.lookup offsets offset of
             SOME (name', time) => if name = name' then SOME time else NONE
           | NONE => NONE)
       | NONE => NONE)
   | NONE => NONE)
   |> the_default Time.zeroTime;
 
 
 (* session base *)
 
 val default_qualifier = "Draft";
 
 type entry = {pos: Position.T, serial: serial};
 
 fun make_entry props : entry =
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
   ({session_positions = []: (string * entry) list,
     session_directories = Symtab.empty: Path.T list Symtab.table,
     session_chapters = Symtab.empty: string Symtab.table,
     bibtex_entries = Symtab.empty: string list Symtab.table,
     timings = empty_timings,
     scala_functions = Symtab.empty: Position.T Symtab.table},
    {global_theories = Symtab.empty: string Symtab.table,
     loaded_theories = Symtab.empty: unit Symtab.table});
 
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
     {session_positions, session_directories, session_chapters, bibtex_entries,
       command_timings, scala_functions, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
       ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
         session_directories =
           fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
             session_directories Symtab.empty,
         session_chapters = Symtab.make session_chapters,
         bibtex_entries = Symtab.make bibtex_entries,
         timings = make_timings command_timings,
         scala_functions = Symtab.make scala_functions},
        {global_theories = Symtab.make global_theories,
         loaded_theories = Symtab.make_set loaded_theories}));
 
 fun init_session_yxml yxml =
   let
     val (session_positions, (session_directories, (session_chapters, (bibtex_entries,
         (command_timings, (scala_functions, (global_theories, loaded_theories))))))) =
       YXML.parse_body yxml |>
         let open XML.Decode in
           (pair (list (pair string properties))
             (pair (list (pair string string)) (pair (list (pair string string))
               (pair (list (pair string (list string))) (pair (list properties)
                 (pair (list (pair string properties))
                   (pair (list (pair string string)) (list string))))))))
         end;
   in
     init_session
       {session_positions = session_positions,
        session_directories = session_directories,
        session_chapters = session_chapters,
        bibtex_entries = bibtex_entries,
        command_timings = command_timings,
        scala_functions = map (apsnd Position.of_properties) scala_functions,
        global_theories = global_theories,
        loaded_theories = loaded_theories}
   end;
 
 fun init_session_file path =
   init_session_yxml (File.read path) before File.rm path;
 
 fun finish_session_base () =
   Synchronized.change global_session_base
     (apfst (K (#1 empty_session_base)));
 
 fun get_session_base f = f (Synchronized.value global_session_base);
 fun get_session_base1 f = get_session_base (f o #1);
 fun get_session_base2 f = get_session_base (f o #2);
 
 fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a;
 
 fun check_session ctxt arg =
   Completion.check_item "session"
     (fn (name, {pos, serial}) =>
       Markup.entity Markup.sessionN name
       |> Markup.properties (Position.entity_properties_of false serial pos))
     (get_session_base1 #session_positions) ctxt arg;
 
 fun session_chapter name =
   the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name);
 
 fun last_timing tr = get_timings (get_session_base1 #timings) tr;
 
 
 (* Scala functions *)
 
 (*raw bootstrap environment*)
 fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
 (*regular resources*)
 fun scala_function_pos name =
   (name, the_default Position.none (Symtab.lookup (get_session_base1 #scala_functions) name));
 
 fun check_scala_function ctxt arg =
   Completion.check_entity Markup.scala_functionN
     (scala_functions () |> sort_strings |> map scala_function_pos) ctxt arg;
 
 val _ = Theory.setup
  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
     (Scan.lift Parse.embedded_position) check_scala_function #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
     (Args.context -- Scan.lift Parse.embedded_position
       >> (uncurry check_scala_function #> ML_Syntax.print_string)) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
       let val name = check_scala_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
-  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
-      let val name = check_scala_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
+      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
 
 
 (* manage source files *)
 
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
   imports: (string * Position.T) list,  (*source specification of imports*)
   provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
 
 fun make_files (master_dir, imports, provided): files =
  {master_dir = master_dir, imports = imports, provided = provided};
 
 structure Files = Theory_Data
 (
   type T = files;
   val empty = make_files (Path.current, [], []);
   val extend = I;
   fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
     let val provided' = Library.merge (op =) (provided1, provided2)
     in make_files (master_dir, imports, provided') end
 );
 
 fun map_files f =
   Files.map (fn {master_dir, imports, provided} =>
     make_files (f (master_dir, imports, provided)));
 
 
 val master_directory = #master_dir o Files.get;
 val imports_of = #imports o Files.get;
 
 fun begin_theory master_dir {name, imports, keywords} parents =
   Theory.begin_theory name parents
   |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, []))
   |> Thy_Header.add_keywords keywords;
 
 
 (* theory files *)
 
 val thy_path = Path.ext "thy";
 
 fun theory_qualifier theory =
   (case global_theory theory of
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
 fun theory_name qualifier theory =
   if Long_Name.is_qualified theory orelse is_some (global_theory theory)
   then theory
   else Long_Name.qualify qualifier theory;
 
 fun theory_bibtex_entries theory =
   Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory);
 
 fun find_theory_file thy_name =
   let
     val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
     val session = theory_qualifier thy_name;
     val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session;
   in
     dirs |> get_first (fn dir =>
       let val path = dir + thy_file
       in if File.is_file path then SOME path else NONE end)
   end;
 
 fun make_theory_node node_name theory =
   {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory};
 
 fun loaded_theory_node theory =
   {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory};
 
 fun import_name qualifier dir s =
   let
     val theory = theory_name qualifier (Thy_Header.import_name s);
     fun theory_node () =
       make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory;
   in
     if not (Thy_Header.is_base_name s) then theory_node ()
     else if loaded_theory theory then loaded_theory_node theory
     else
       (case find_theory_file theory of
         SOME node_name => make_theory_node node_name theory
       | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ())
   end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
 fun check_thy dir thy_name =
   let
     val thy_base_name = Long_Name.base_name thy_name;
     val master_file =
       (case find_theory_file thy_name of
         SOME path => check_file Path.current path
       | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
     val text = File.read master_file;
 
     val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
     val _ =
       thy_base_name <> name andalso
         error ("Bad theory name " ^ quote name ^
           " for file " ^ Path.print (Path.base master_file) ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}
   end;
 
 
 (* load files *)
 
 fun parse_files make_paths =
   Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy =>
     (case Token.get_files tok of
       [] =>
         let
           val master_dir = master_directory thy;
           val name = Input.string_of source;
           val pos = Input.pos_of source;
           val delimited = Input.is_delimited source;
           val src_paths = make_paths (Path.explode name);
         in map (Command.read_file master_dir pos delimited) src_paths end
     | files => map Exn.release files));
 
 val parse_file = parse_files single >> (fn f => f #> the_single);
 
 
 fun provide (src_path, id) =
   map_files (fn (master_dir, imports, provided) =>
     if AList.defined (op =) provided src_path then
       error ("Duplicate use of source file: " ^ Path.print src_path)
     else (master_dir, imports, (src_path, id) :: provided));
 
 fun provide_file (file: Token.file) = provide (#src_path file, #digest file);
 
 fun provide_parse_files make_paths =
   parse_files make_paths >> (fn files => fn thy =>
     let
       val fs = files thy;
       val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
     in (fs, thy') end);
 
 val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single);
 
 
 fun load_file thy src_path =
   let
     val full_path = check_file (master_directory thy) src_path;
     val text = File.read full_path;
     val id = SHA1.digest text;
   in ((full_path, id), text) end;
 
 fun loaded_files_current thy =
   #provided (Files.get thy) |>
     forall (fn (src_path, id) =>
       (case try (load_file thy) src_path of
         NONE => false
       | SOME ((_, id'), _) => id = id'));
 
 
 (* formal check *)
 
 fun formal_check check_file ctxt opt_dir source =
   let
     val name = Input.string_of source;
     val pos = Input.pos_of source;
     val delimited = Input.is_delimited source;
 
     val _ = Context_Position.report ctxt pos (Markup.language_path delimited);
 
     fun err msg = error (msg ^ Position.here pos);
     val dir =
       (case opt_dir of
         SOME dir => dir
       | NONE => master_directory (Proof_Context.theory_of ctxt));
     val path = dir + Path.explode name handle ERROR msg => err msg;
     val _ = Path.expand path handle ERROR msg => err msg;
     val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
     val _ : Path.T = check_file path handle ERROR msg => err msg;
   in path end;
 
 val check_path = formal_check I;
 val check_file = formal_check File.check_file;
 val check_dir = formal_check File.check_dir;
 
 fun check_session_dir ctxt opt_dir s =
   let
     val dir = Path.expand (check_dir ctxt opt_dir s);
     val ok =
       File.is_file (dir + Path.explode("ROOT")) orelse
       File.is_file (dir + Path.explode("ROOTS"));
   in
     if ok then dir
     else
       error ("Bad session root directory (missing ROOT or ROOTS): " ^
         Path.print dir ^ Position.here (Input.pos_of s))
   end;
 
 
 (* antiquotations *)
 
 local
 
 fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) =
   Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
     let
       val _ = check ctxt NONE source;
       val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source));
     in Latex.enclose_block "\\isatt{" "}" [latex] end);
 
 fun ML_antiq check =
   Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
     check ctxt (SOME Path.current) source |> ML_Syntax.print_path);
 
 in
 
 val _ = Theory.setup
  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
     (Scan.lift Parse.embedded_position) check_session #>
   Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
   Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
   Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>path_binding\<close>
     (Scan.lift (Parse.position Parse.path) >>
       (ML_Syntax.print_path_binding o Path.explode_binding)) #>
   ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
     (Args.theory >> (ML_Syntax.print_path o master_directory)));
 
 end;
 
 end;
diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala
+++ b/src/Pure/System/bash.scala
@@ -1,235 +1,235 @@
 /*  Title:      Pure/System/bash.scala
     Author:     Makarius
 
 GNU bash processes, with propagation of interrupts.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, BufferedReader, InputStreamReader,
   BufferedWriter, OutputStreamWriter}
 
 import scala.annotation.tailrec
 
 
 object Bash
 {
   /* concrete syntax */
 
   private def bash_chr(c: Byte): String =
   {
     val ch = c.toChar
     ch match {
       case '\t' => "$'\\t'"
       case '\n' => "$'\\n'"
       case '\f' => "$'\\f'"
       case '\r' => "$'\\r'"
       case _ =>
         if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch))
           Symbol.ascii(ch)
         else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
         else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
         else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
         else  "\\" + ch
     }
   }
 
   def string(s: String): String =
     if (s == "") "\"\""
     else UTF8.bytes(s).iterator.map(bash_chr).mkString
 
   def strings(ss: List[String]): String =
     ss.iterator.map(Bash.string).mkString(" ")
 
 
   /* process and result */
 
   type Watchdog = (Time, Process => Boolean)
 
   def process(script: String,
       cwd: JFile = null,
       env: Map[String, String] = Isabelle_System.settings(),
       redirect: Boolean = false,
       cleanup: () => Unit = () => ()): Process =
     new Process(script, cwd, env, redirect, cleanup)
 
   class Process private[Bash](
       script: String,
       cwd: JFile,
       env: Map[String, String],
       redirect: Boolean,
       cleanup: () => Unit)
   {
     private val timing_file = Isabelle_System.tmp_file("bash_timing")
     private val timing = Synchronized[Option[Timing]](None)
     def get_timing: Timing = timing.value getOrElse Timing.zero
 
     private val script_file = Isabelle_System.tmp_file("bash_script")
     File.write(script_file, script)
 
     private val proc =
       Isabelle_System.process(
         List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
           File.standard_path(timing_file), "bash", File.standard_path(script_file)),
         cwd = cwd, env = env, redirect = redirect)
 
 
     // channels
 
     val stdin: BufferedWriter =
       new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
 
     val stdout: BufferedReader =
       new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
 
     val stderr: BufferedReader =
       new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
 
 
     // signals
 
     private val pid = stdout.readLine
 
     @tailrec private def kill(signal: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
         Isabelle_System.kill(signal, pid)
         val running = Isabelle_System.kill("0", pid)._2 == 0
         if (running) {
           Time.seconds(0.1).sleep
           kill(signal, count - 1)
         }
         else false
       }
     }
 
     def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
       kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
       proc.destroy()
       do_cleanup()
     }
 
     def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
     {
       Isabelle_System.kill("INT", pid)
     }
 
 
     // JVM shutdown hook
 
     private val shutdown_hook = Isabelle_Thread.create(() => terminate())
 
     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
     catch { case _: IllegalStateException => }
 
 
     // cleanup
 
     private def do_cleanup(): Unit =
     {
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
       script_file.delete
 
       timing.change {
         case None =>
           if (timing_file.isFile) {
             val t =
               Word.explode(File.read(timing_file)) match {
                 case List(Value.Long(elapsed), Value.Long(cpu)) =>
                   Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
                 case _ => Timing.zero
               }
             timing_file.delete
             Some(t)
           }
           else Some(Timing.zero)
         case some => some
       }
 
       cleanup()
     }
 
 
     // join
 
     def join: Int =
     {
       val rc = proc.waitFor
       do_cleanup()
       rc
     }
 
 
     // result
 
     def result(
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
       watchdog: Option[Watchdog] = None,
       strict: Boolean = true): Process_Result =
     {
       stdin.close()
 
       val out_lines =
         Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
       val err_lines =
         Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
 
       val watchdog_thread =
         for ((time, check) <- watchdog)
         yield {
           Future.thread("bash_watchdog") {
             while (proc.isAlive) {
               time.sleep
               if (check(this)) interrupt()
             }
           }
         }
 
       val rc =
         try { join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
       watchdog_thread.foreach(_.cancel())
 
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
   }
 
 
   /* Scala function */
 
-  object Process extends Scala.Fun("bash_process")
+  object Process extends Scala.Fun("bash_process", thread = true)
   {
     val here = Scala_Project.here
     def apply(script: String): String =
     {
       val result = Exn.capture { Isabelle_System.bash(script) }
 
       val is_interrupt =
         result match {
           case Exn.Res(res) => res.rc == Exn.Interrupt.return_code
           case Exn.Exn(exn) => Exn.is_interrupt(exn)
         }
 
       result match {
         case _ if is_interrupt => ""
         case Exn.Exn(exn) => Exn.message(exn)
         case Exn.Res(res) =>
           Library.cat_strings0(
             res.rc.toString ::
             res.timing.elapsed.ms.toString ::
             res.timing.cpu.ms.toString ::
             res.out_lines.length.toString ::
             res.out_lines ::: res.err_lines)
       }
     }
   }
 }
diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML
+++ b/src/Pure/System/isabelle_system.ML
@@ -1,117 +1,117 @@
 (*  Title:      Pure/System/isabelle_system.ML
     Author:     Makarius
 
 Isabelle system support.
 *)
 
 signature ISABELLE_SYSTEM =
 sig
   val bash_process: string -> Process_Result.T
   val bash_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
   val check_bash_function: Proof.context -> string * Position.T -> string
   val make_directory: Path.T -> Path.T
   val copy_dir: Path.T -> Path.T -> unit
   val copy_file: Path.T -> Path.T -> unit
   val copy_file_base: Path.T * Path.T -> Path.T -> unit
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val rm_tree: Path.T -> unit
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val download: string -> Path.T -> unit
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
 struct
 
 (* bash *)
 
 fun bash_process script =
-  Scala.function_thread "bash_process"
+  Scala.function "bash_process"
     ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
   |> split_strings0
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
       | a :: b :: c :: d :: lines =>
           let
             val rc = Value.parse_int a;
             val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
             val (out_lines, err_lines) = chop (Value.parse_int d) lines;
           in
             Process_Result.make
              {rc = rc,
               out_lines = out_lines,
               err_lines = err_lines,
               timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
 val bash = bash_process #> Process_Result.print #> Process_Result.rc;
 
 fun bash_output s =
   let
     val res = bash_process s;
     val _ = warning (Process_Result.err res);
   in (Process_Result.out res, Process_Result.rc res) end;
 
 
 (* bash functions *)
 
 fun bash_functions () =
   bash_process "declare -Fx"
   |> Process_Result.check
   |> Process_Result.out_lines
   |> map_filter (space_explode " " #> try List.last);
 
 fun check_bash_function ctxt arg =
   Completion.check_entity Markup.bash_functionN
     (bash_functions () |> map (rpair Position.none)) ctxt arg;
 
 
 (* directory and file operations *)
 
 val absolute_path = Path.implode o File.absolute_path;
 fun scala_function0 name = ignore o Scala.function name o cat_strings0;
 fun scala_function name = scala_function0 name o map absolute_path;
 
 fun make_directory path = (scala_function "make_directory" [path]; path);
 
 fun copy_dir src dst = scala_function "copy_dir" [src, dst];
 
 fun copy_file src dst = scala_function "copy_file" [src, dst];
 
 fun copy_file_base (base_dir, src) target_dir =
   scala_function0 "copy_file_base"
     [absolute_path base_dir, Path.implode src, absolute_path target_dir];
 
 
 (* tmp files *)
 
 fun create_tmp_path name ext =
   let
     val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext);
     val _ = File.exists path andalso
       raise Fail ("Temporary file already exists: " ^ Path.print path);
   in path end;
 
 fun with_tmp_file name ext f =
   let val path = create_tmp_path name ext
   in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
 
 
 (* tmp dirs *)
 
 fun rm_tree path = scala_function "rm_tree" [path];
 
 fun with_tmp_dir name f =
   let val path = create_tmp_path name ""
   in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
 
 
 (* download file *)
 
 fun download url file =
-  ignore (Scala.function_thread "download" (cat_strings0 [url, absolute_path file]));
+  ignore (Scala.function "download" (cat_strings0 [url, absolute_path file]));
 
 end;
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,568 +1,568 @@
 /*  Title:      Pure/System/isabelle_system.scala
     Author:     Makarius
 
 Fundamental Isabelle system environment: quasi-static module with
 optional init operation.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, IOException}
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
   StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 
 
 
 object Isabelle_System
 {
   /** bootstrap information **/
 
   def jdk_home(): String =
   {
     val java_home = System.getProperty("java.home", "")
     val home = new JFile(java_home)
     val parent = home.getParent
     if (home.getName == "jre" && parent != null &&
         (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
     else java_home
   }
 
   def bootstrap_directory(
     preference: String, envar: String, property: String, description: String): String =
   {
     val value =
       proper_string(preference) orElse  // explicit argument
       proper_string(System.getenv(envar)) orElse  // e.g. inherited from running isabelle tool
       proper_string(System.getProperty(property)) getOrElse  // e.g. via JVM application boot process
       error("Unknown " + description + " directory")
 
     if ((new JFile(value)).isDirectory) value
     else error("Bad " + description + " directory " + quote(value))
   }
 
 
 
   /** implicit settings environment **/
 
   abstract class Service
 
   @volatile private var _settings: Option[Map[String, String]] = None
   @volatile private var _services: Option[List[Class[Service]]] = None
 
   def settings(): Map[String, String] =
   {
     if (_settings.isEmpty) init()  // unsynchronized check
     _settings.get
   }
 
   def services(): List[Class[Service]] =
   {
     if (_services.isEmpty) init()  // unsynchronized check
     _services.get
   }
 
   def make_services[C](c: Class[C]): List[C] =
     for { c1 <- services() if Library.is_subclass(c1, c) }
       yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
   {
     if (_settings.isEmpty || _services.isEmpty) {
       val isabelle_root1 =
         bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
 
       val cygwin_root1 =
         if (Platform.is_windows)
           bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
         else ""
 
       if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
 
       def set_cygwin_root(): Unit =
       {
         if (Platform.is_windows)
           _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
       }
 
       set_cygwin_root()
 
       def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
         if (env.isDefinedAt(entry._1) || entry._2 == "") env
         else env + entry
 
       val env =
       {
         val temp_windows =
         {
           val temp = if (Platform.is_windows) System.getenv("TEMP") else null
           if (temp != null && temp.contains('\\')) temp else ""
         }
         val user_home = System.getProperty("user.home", "")
         val isabelle_app = System.getProperty("isabelle.app", "")
 
         default(
           default(
             default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
               "TEMP_WINDOWS" -> temp_windows),
             "HOME" -> user_home),
           "ISABELLE_APP" -> "true")
       }
 
       val settings =
       {
         val dump = JFile.createTempFile("settings", null)
         dump.deleteOnExit
         try {
           val cmd1 =
             if (Platform.is_windows)
               List(cygwin_root1 + "\\bin\\bash", "-l",
                 File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
             else
               List(isabelle_root1 + "/bin/isabelle")
           val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
 
           val (output, rc) = process_output(process(cmd, env = env, redirect = true))
           if (rc != 0) error(output)
 
           val entries =
             (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield {
               val i = entry.indexOf('=')
               if (i <= 0) entry -> ""
               else entry.substring(0, i) -> entry.substring(i + 1)
             }).toMap
           entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
         }
         finally { dump.delete }
       }
       _settings = Some(settings)
       set_cygwin_root()
 
       val variable = "ISABELLE_SCALA_SERVICES"
       val services =
         for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
         yield {
           def err(msg: String): Nothing =
             error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
           try { Class.forName(name).asInstanceOf[Class[Service]] }
           catch {
             case _: ClassNotFoundException => err("Class not found")
             case exn: Throwable => err(Exn.message(exn))
           }
         }
       _services = Some(services)
     }
   }
 
 
   /* getenv */
 
   private def getenv_error(name: String): Nothing =
     error("Undefined Isabelle environment variable: " + quote(name))
 
   def getenv(name: String, env: Map[String, String] = settings()): String =
     env.getOrElse(name, "")
 
   def getenv_strict(name: String, env: Map[String, String] = settings()): String =
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))
 
   def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
 
   def isabelle_id(): String =
     proper_string(getenv("ISABELLE_ID")) getOrElse
       Mercurial.repository(Path.explode("~~")).parent()
 
 
 
   /** file-system operations **/
 
   /* scala functions */
 
   private def apply_paths(arg: String, fun: List[Path] => Unit): String =
     { fun(Library.split_strings0(arg).map(Path.explode)); "" }
 
   private def apply_paths1(arg: String, fun: Path => Unit): String =
     apply_paths(arg, { case List(path) => fun(path) })
 
   private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String =
     apply_paths(arg, { case List(path1, path2) => fun(path1, path2) })
 
   private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String =
     apply_paths(arg, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
 
   def chmod(arg: String, path: Path): Unit =
     bash("chmod " + arg + " " + File.bash_path(path)).check
 
   def chown(arg: String, path: Path): Unit =
     bash("chown " + arg + " " + File.bash_path(path)).check
 
 
   /* directories */
 
   def make_directory(path: Path): Path =
   {
     if (!path.is_dir) {
       try { Files.createDirectories(path.file.toPath) }
       catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
     }
     path
   }
 
   def new_directory(path: Path): Path =
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)
 
   def copy_dir(dir1: Path, dir2: Path): Unit =
   {
     val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
     if (!res.ok) {
       cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
     }
   }
 
 
   object Make_Directory extends Scala.Fun("make_directory")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = apply_paths1(arg, make_directory)
   }
 
   object Copy_Dir extends Scala.Fun("copy_dir")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = apply_paths2(arg, copy_dir)
   }
 
 
   /* copy files */
 
   def copy_file(src: JFile, dst: JFile): Unit =
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target)) {
       try {
         Files.copy(src.toPath, target.toPath,
           StandardCopyOption.COPY_ATTRIBUTES,
           StandardCopyOption.REPLACE_EXISTING)
       }
       catch {
         case ERROR(msg) =>
           cat_error("Failed top copy file " +
             File.path(src).absolute + " to " + File.path(dst).absolute, msg)
       }
     }
   }
 
   def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
 
   def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit =
   {
     val src1 = src.expand
     val src1_dir = src1.dir
     if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
     copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
   }
 
 
   object Copy_File extends Scala.Fun("copy_file")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = apply_paths2(arg, copy_file)
   }
 
   object Copy_File_Base extends Scala.Fun("copy_file_base")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = apply_paths3(arg, copy_file_base)
   }
 
 
   /* move files */
 
   def move_file(src: JFile, dst: JFile): Unit =
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target))
       Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
   }
 
   def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
 
 
   /* symbolic link */
 
   def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
   {
     val src_file = src.file
     val dst_file = dst.file
     val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
 
     if (force) target.delete
 
     try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
     catch {
       case _: UnsupportedOperationException if Platform.is_windows =>
         Cygwin.link(File.standard_path(src), target)
       case _: FileSystemException if Platform.is_windows =>
         Cygwin.link(File.standard_path(src), target)
     }
   }
 
 
   /* tmp files */
 
   def isabelle_tmp_prefix(): JFile =
   {
     val path = Path.explode("$ISABELLE_TMP_PREFIX")
     path.file.mkdirs  // low-level mkdirs to avoid recursion via Isabelle environment
     File.platform_file(path)
   }
 
   def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
   {
     val suffix = if (ext == "") "" else "." + ext
     val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
     file.deleteOnExit
     file
   }
 
   def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
   {
     val file = tmp_file(name, ext)
     try { body(File.path(file)) } finally { file.delete }
   }
 
 
   /* tmp dirs */
 
   def rm_tree(root: JFile): Unit =
   {
     root.delete
     if (root.isDirectory) {
       Files.walkFileTree(root.toPath,
         new SimpleFileVisitor[JPath] {
           override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
             try { Files.deleteIfExists(file) }
             catch { case _: IOException => }
             FileVisitResult.CONTINUE
           }
 
           override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
           {
             if (e == null) {
               try { Files.deleteIfExists(dir) }
               catch { case _: IOException => }
               FileVisitResult.CONTINUE
             }
             else throw e
           }
         }
       )
     }
   }
 
   def rm_tree(root: Path): Unit = rm_tree(root.file)
 
   object Rm_Tree extends Scala.Fun("rm_tree")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = apply_paths1(arg, rm_tree)
   }
 
   def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
   {
     val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
     dir.deleteOnExit
     dir
   }
 
   def with_tmp_dir[A](name: String)(body: Path => A): A =
   {
     val dir = tmp_dir(name)
     try { body(File.path(dir)) } finally { rm_tree(dir) }
   }
 
 
   /* quasi-atomic update of directory */
 
   def update_directory(dir: Path, f: Path => Unit): Unit =
   {
     val new_dir = dir.ext("new")
     val old_dir = dir.ext("old")
 
     rm_tree(new_dir)
     rm_tree(old_dir)
 
     f(new_dir)
 
     if (dir.is_dir) move_file(dir, old_dir)
     move_file(new_dir, dir)
     rm_tree(old_dir)
   }
 
 
 
   /** external processes **/
 
   /* raw process */
 
   def process(command_line: List[String],
     cwd: JFile = null,
     env: Map[String, String] = settings(),
     redirect: Boolean = false): Process =
   {
     val proc = new ProcessBuilder
     proc.command(command_line:_*)  // fragile on Windows
     if (cwd != null) proc.directory(cwd)
     if (env != null) {
       proc.environment.clear()
       for ((x, y) <- env) proc.environment.put(x, y)
     }
     proc.redirectErrorStream(redirect)
     proc.start
   }
 
   def process_output(proc: Process): (String, Int) =
   {
     proc.getOutputStream.close()
 
     val output = File.read_stream(proc.getInputStream)
     val rc =
       try { proc.waitFor }
       finally {
         proc.getInputStream.close()
         proc.getErrorStream.close()
         proc.destroy()
         Exn.Interrupt.dispose()
       }
     (output, rc)
   }
 
   def kill(signal: String, group_pid: String): (String, Int) =
   {
     val bash =
       if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
       else List("/usr/bin/env", "bash")
     process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
   }
 
 
   /* GNU bash */
 
   def bash(script: String,
     cwd: JFile = null,
     env: Map[String, String] = settings(),
     redirect: Boolean = false,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
     watchdog: Option[Bash.Watchdog] = None,
     strict: Boolean = true,
     cleanup: () => Unit = () => ()): Process_Result =
   {
     Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
       result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
         watchdog = watchdog, strict = strict)
   }
 
   private lazy val gnutar_check: Boolean =
     try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
     catch { case ERROR(_) => false }
 
   def gnutar(
     args: String,
     dir: Path = Path.current,
     original_owner: Boolean = false,
     redirect: Boolean = false): Process_Result =
   {
     val options =
       (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
       (if (original_owner) "" else "--owner=root --group=staff ")
 
     if (gnutar_check) bash("tar " + options + args, redirect = redirect)
     else error("Expected to find GNU tar executable")
   }
 
   def require_command(cmds: String*): Unit =
   {
     for (cmd <- cmds) {
       if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd))
     }
   }
 
   def hostname(): String = bash("hostname -s").check.out
 
   def open(arg: String): Unit =
     bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
 
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
   def open_external_file(name: String): Boolean =
   {
     val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
     val external =
       ext.nonEmpty &&
       Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
     if (external) {
       if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
       else open(name)
     }
     external
   }
 
   def export_isabelle_identifier(isabelle_identifier: String): String =
     if (isabelle_identifier == "") ""
     else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
 
 
   /** Isabelle resources **/
 
   /* repository clone with Admin */
 
   def admin(): Boolean = Path.explode("~~/Admin").is_dir
 
 
   /* components */
 
   def components(): List[Path] =
     Path.split(getenv_strict("ISABELLE_COMPONENTS"))
 
 
   /* default logic */
 
   def default_logic(args: String*): String =
   {
     args.find(_ != "") match {
       case Some(logic) => logic
       case None => getenv_strict("ISABELLE_LOGIC")
     }
   }
 
 
   /* download file */
 
   def download(url_name: String, file: Path, progress: Progress = new Progress): Unit =
   {
     val url = Url(url_name)
     progress.echo("Getting " + quote(url_name))
     val content =
       try { HTTP.Client.get(url) }
       catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
     Bytes.write(file, content.bytes)
   }
 
-  object Download extends Scala.Fun("download")
+  object Download extends Scala.Fun("download", thread = true)
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
       Library.split_strings0(arg) match {
         case List(url, file) => download(url, Path.explode(file)); ""
       }
   }
 }
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,66 @@
 (*  Title:      Pure/System/scala.ML
     Author:     Makarius
 
 Invoke Scala functions from the ML runtime.
 *)
 
 signature SCALA =
 sig
   exception Null
   val function: string -> string -> string
-  val function_thread: string -> string -> string
 end;
 
 structure Scala: SCALA =
 struct
 
 exception Null;
 
 local
 
 val new_id = string_of_int o Counter.make ();
 
 val results =
   Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table);
 
 val _ =
   Protocol_Command.define "Scala.result"
     (fn [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: " ^ tag));
       in Synchronized.change results (Symtab.map_entry id (K result)) end);
 
-fun gen_function thread name arg =
+in
+
+fun function name arg =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val id = new_id ();
       fun invoke () =
        (Synchronized.change results (Symtab.update (id, Exn.Exn Match));
-        Output.protocol_message (Markup.invoke_scala name id thread) [XML.Text arg]);
+        Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]);
       fun cancel () =
        (Synchronized.change results (Symtab.delete_safe id);
         Output.protocol_message (Markup.cancel_scala id) []);
       fun await_result () =
         Synchronized.guarded_access results
           (fn tab =>
             (case Symtab.lookup tab id of
               SOME (Exn.Exn Match) => NONE
             | SOME result => SOME (result, Symtab.delete id tab)
             | NONE => SOME (Exn.Exn Exn.Interrupt, tab)));
     in
       invoke ();
       Exn.release (restore_attributes await_result ())
         handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
     end) ();
 
-in
-
-val function = gen_function false;
-val function_thread = gen_function true;
-
 end;
 
 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,256 +1,263 @@
 /*  Title:      Pure/System/scala.scala
     Author:     Makarius
 
 Support for Scala at runtime.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
 import scala.tools.nsc.interpreter.{IMain, Results}
 import scala.tools.nsc.interpreter.shell.ReplReporterImpl
 
 object Scala
 {
   /** registered functions **/
 
-  abstract class Fun(val name: String) extends Function[String, String]
+  abstract class Fun(val name: String, val thread: Boolean = false)
+    extends Function[String, String]
   {
     override def toString: String = name
     def position: Properties.T = here.position
     def here: Scala_Project.Here
     def apply(arg: String): String
   }
 
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 
   lazy val functions: List[Fun] =
     Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
 
 
 
   /** demo functions **/
 
   object Echo extends Fun("echo")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = arg
   }
 
   object Sleep extends Fun("sleep")
   {
     val here = Scala_Project.here
     def apply(seconds: String): String =
     {
       val t =
         seconds match {
           case Value.Double(s) => Time.seconds(s)
           case _ => error("Malformed argument: " + quote(seconds))
         }
       val t0 = Time.now()
       t.sleep
       val t1 = Time.now()
       (t1 - t0).toString
     }
   }
 
 
 
   /** compiler **/
 
   object Compiler
   {
     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("isabelle.scala.classpath", "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, new ReplReporterImpl(settings, print_writer))
         {
           override def parentClassLoader: ClassLoader =
             if (class_loader == null) super.parentClassLoader
             else class_loader
         }
       }
 
       def toplevel(interpret: Boolean, source: String): List[String] =
       {
         val out = new StringWriter
         val interp = interpreter(new PrintWriter(out))
         val marker = '\u000b'
         val ok =
           interp.withLabel(marker.toString) {
             if (interpret) interp.interpret(source) == Results.Success
             else (new interp.ReadEvalPrint).compile(source)
           }
         out.close()
 
         val Error = """(?s)^\S* error: (.*)$""".r
         val errors =
           space_explode(marker, Library.strip_ansi_color(out.toString)).
             collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
         if (!ok && errors.isEmpty) List("Error") else errors
       }
     }
   }
 
   object Toplevel extends Fun("scala_toplevel")
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
     {
       val (interpret, source) =
         YXML.parse_body(arg) match {
           case Nil => (false, "")
           case List(XML.Text(source)) => (false, source)
           case body => import XML.Decode._; pair(bool, string)(body)
         }
       val errors =
         try { Compiler.context().toplevel(interpret, source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
   }
 
 
 
   /** invoke Scala functions from ML **/
 
   /* invoke function */
 
   object Tag extends Enumeration
   {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
-  def function(name: String, arg: String): (Tag.Value, String) =
+  def function_thread(name: String): Boolean =
+    functions.find(fun => fun.name == name) match {
+      case Some(fun) => fun.thread
+      case None => false
+    }
+
+  def function_body(name: String, arg: String): (Tag.Value, String) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
         Exn.capture { fun(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 None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
     }
 
 
   /* protocol handler */
 
   class Handler extends Session.Protocol_Handler
   {
     private var session: Session = null
     private var futures = Map.empty[String, Future[Unit]]
 
     override def init(session: Session): Unit =
       synchronized { this.session = session }
 
     override def exit(): Unit = synchronized
     {
       for ((id, future) <- futures) cancel(id, future)
       futures = Map.empty
     }
 
     private def result(id: String, tag: Scala.Tag.Value, res: String): Unit =
       synchronized
       {
         if (futures.isDefinedAt(id)) {
           session.protocol_command("Scala.result", id, tag.id.toString, res)
           futures -= id
         }
       }
 
     private def cancel(id: String, future: Future[Unit]): Unit =
     {
       future.cancel()
       result(id, Scala.Tag.INTERRUPT, "")
     }
 
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
-        case Markup.Invoke_Scala(name, id, thread) =>
+        case Markup.Invoke_Scala(name, id) =>
           def body: Unit =
           {
-            val (tag, res) = Scala.function(name, msg.text)
+            val (tag, res) = Scala.function_body(name, msg.text)
             result(id, tag, res)
           }
           val future =
-            if (thread) {
+            if (Scala.function_thread(name)) {
               Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
             }
             else Future.fork(body)
           futures += (id -> future)
           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
       }
     }
 
     override val functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
   }
 }
 
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
   Doc.Doc_Names,
   Bash.Process,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,
   Isabelle_System.Copy_Dir,
   Isabelle_System.Copy_File,
   Isabelle_System.Copy_File_Base,
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
   Isabelle_Tool.Isabelle_Tools,
   isabelle.atp.SystemOnTPTP.List_Systems)