diff --git a/src/HOL/Sledgehammer.thy b/src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy
+++ b/src/HOL/Sledgehammer.thy
@@ -1,36 +1,37 @@
 (*  Title:      HOL/Sledgehammer.thy
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     Author:     Jasmin Blanchette, TU Muenchen
 *)
 
 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
 
 theory Sledgehammer
 imports Presburger SMT
 keywords
   "sledgehammer" :: diag and
   "sledgehammer_params" :: thy_decl
 begin
 
+ML_file \<open>Tools/ATP/system_on_tptp.ML\<close>
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_atp_systems.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 
 end
diff --git a/src/HOL/Tools/ATP/system_on_tptp.ML b/src/HOL/Tools/ATP/system_on_tptp.ML
new file mode 100644
--- /dev/null
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML
@@ -0,0 +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
+
+end
diff --git a/src/HOL/Tools/ATP/system_on_tptp.scala b/src/HOL/Tools/ATP/system_on_tptp.scala
new file mode 100644
--- /dev/null
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala
@@ -0,0 +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")
+  {
+    val here = Scala_Project.here
+    def apply(url: String): String = cat_lines(list_systems(Url(url)))
+  }
+}
diff --git a/src/HOL/Tools/etc/options b/src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options
+++ b/src/HOL/Tools/etc/options
@@ -1,45 +1,48 @@
 (* :mode=isabelle-options: *)
 
 section "Automatically tried tools"
 
 public option auto_time_start : real = 1.0
   -- "initial delay for automatically tried tools (seconds)"
 
 public option auto_time_limit : real = 2.0
   -- "time limit for automatically tried tools (seconds > 0)"
 
 public option auto_nitpick : bool = false
   -- "run Nitpick automatically"
 
 public option auto_sledgehammer : bool = false
   -- "run Sledgehammer automatically"
 
 public option auto_methods : bool = false
   -- "try standard proof methods automatically"
 
 public option auto_quickcheck : bool = true
   -- "run Quickcheck automatically"
 
 public option auto_solve_direct : bool = true
   -- "run solve_direct automatically"
 
 
 section "Miscellaneous Tools"
 
 public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire"
   -- "provers for Sledgehammer (separated by blanks)"
 
 public option sledgehammer_timeout : int = 30
   -- "provers will be interrupted after this time (in seconds)"
 
 public option vampire_noncommercial : string = "unknown"
   -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
 
+public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
+  -- "URL for SystemOnTPTP service"
+
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
 
 public option kodkod_scala : bool = true
   -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
 
 public option kodkod_max_threads : int = 0
   -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)"
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,255 +1,256 @@
 /*  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]
   {
     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) =
     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) =>
           def body: Unit =
           {
             val (tag, res) = Scala.function(name, msg.text)
             result(id, tag, res)
           }
           val future =
             if (thread) {
               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_Tool.Isabelle_Tools,
+  isabelle.atp.SystemOnTPTP.List_Systems)
diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala
+++ b/src/Pure/Tools/scala_project.scala
@@ -1,192 +1,193 @@
 /*  Title:      Pure/Tools/scala_project.scala
     Author:     Makarius
 
 Setup Gradle project for Isabelle/Scala/jEdit.
 */
 
 package isabelle
 
 
 object Scala_Project
 {
   /* groovy syntax */
 
   def groovy_string(s: String): String =
   {
     s.map(c =>
       c match {
         case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c
         case _ => c.toString
       }).mkString("'", "", "'")
   }
 
 
   /* file and directories */
 
   lazy val isabelle_files: List[String] =
   {
     val files1 =
     {
       val isabelle_home = Path.explode("~~").canonical
       Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")).
         map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode)
     }
 
     val files2 =
       (for {
         path <-
           List(
             Path.explode("~~/lib/classes/Pure.shasum"),
             Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum"))
         if path.is_file
         line <- Library.trim_split_lines(File.read(path))
         name =
           if (line.length > 42 && line(41) == '*') line.substring(42)
           else error("Bad shasum entry: " + quote(line))
         if name != "lib/classes/Pure.jar" &&
           name != "src/Tools/jEdit/dist/jedit.jar" &&
           name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit-base.jar" &&
           name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar"
       } yield name)
 
     files1 ::: files2
   }
 
   lazy val isabelle_scala_files: Map[String, Path] =
     isabelle_files.foldLeft(Map.empty[String, Path]) {
       case (map, name) =>
         if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) {
           val path = Path.explode("~~/" + name)
           val base = path.base.implode
           map.get(base) match {
             case None => map + (base -> path)
             case Some(path1) => error("Conflicting base names: " + path + " vs. " + path1)
           }
         }
         else map
     }
 
   val isabelle_dirs: List[(String, Path)] =
     List(
       "src/Pure/" -> Path.explode("isabelle"),
       "src/Tools/Graphview/" -> Path.explode("isabelle.graphview"),
       "src/Tools/VSCode/" -> Path.explode("isabelle.vscode"),
       "src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
       "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
       "src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
+      "src/HOL/Tools/ATP" -> Path.explode("isabelle.atp"),
       "src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
 
 
   /* compile-time position */
 
   def here: Here =
   {
     val exn = new Exception
     exn.getStackTrace.toList match {
       case _ :: caller :: _ =>
         val name = proper_string(caller.getFileName).getOrElse("")
         val line = caller.getLineNumber
         new Here(name, line)
       case _ => new Here("", 0)
     }
   }
 
   class Here private[Scala_Project](name: String, line: Int)
   {
     override def toString: String = name + ":" + line
     def position: Position.T =
       isabelle_scala_files.get(name) match {
         case Some(path) => Position.Line_File(line, path.implode)
         case None => Position.none
       }
   }
 
 
   /* scala project */
 
   def scala_project(project_dir: Path, symlinks: Boolean = false): Unit =
   {
     if (symlinks && Platform.is_windows)
       error("Cannot create symlinks on Windows")
 
     if (project_dir.is_file || project_dir.is_dir)
       error("Project directory already exists: " + project_dir)
 
     val src_dir = project_dir + Path.explode("src/main/scala")
     val java_src_dir = project_dir + Path.explode("src/main/java")
     val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
 
     Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
 
     val files = isabelle_files
     isabelle_scala_files
 
     for (file <- files if file.endsWith(".scala")) {
       val (path, target) =
         isabelle_dirs.collectFirst({
           case (prfx, p) if file.startsWith(prfx) =>
             (Path.explode("~~") + Path.explode(file), scala_src_dir + p)
         }).getOrElse(error("Unknown directory prefix for " + quote(file)))
 
       Isabelle_System.make_directory(target)
       if (symlinks) Isabelle_System.symlink(path, target)
       else Isabelle_System.copy_file(path, target)
     }
 
     val jars =
       for (file <- files if file.endsWith(".jar"))
       yield {
         if (file.startsWith("/")) file
         else Isabelle_System.getenv("ISABELLE_HOME") + "/" + file
       }
 
     File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n")
     File.write(project_dir + Path.explode("build.gradle"),
 """plugins {
   id 'scala'
 }
 
 repositories {
   mavenCentral()
 }
 
 dependencies {
   implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """'
   compile files(
     """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
 """
 }
 """)
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit",
       Scala_Project.here, args =>
     {
       var symlinks = false
 
       val getopts = Getopts("""
 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.
 """,
         "L" -> (_ => symlinks = true))
 
       val more_args = getopts(args)
 
       val project_dir =
         more_args match {
           case List(dir) => Path.explode(dir)
           case _ => getopts.usage()
         }
 
       scala_project(project_dir, symlinks = symlinks)
     })
 }
diff --git a/src/Pure/build-jars b/src/Pure/build-jars
--- a/src/Pure/build-jars
+++ b/src/Pure/build-jars
@@ -1,324 +1,325 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # build-jars - build Isabelle/Scala
 #
 # Requires proper Isabelle settings environment.
 
 ## sources
 
 declare -a SOURCES=(
   src/HOL/SPARK/Tools/spark.scala
+  src/HOL/Tools/ATP/system_on_tptp.scala
   src/HOL/Tools/Nitpick/kodkod.scala
   src/Pure/Admin/afp.scala
   src/Pure/Admin/build_csdp.scala
   src/Pure/Admin/build_cygwin.scala
   src/Pure/Admin/build_doc.scala
   src/Pure/Admin/build_e.scala
   src/Pure/Admin/build_fonts.scala
   src/Pure/Admin/build_history.scala
   src/Pure/Admin/build_jdk.scala
   src/Pure/Admin/build_log.scala
   src/Pure/Admin/build_polyml.scala
   src/Pure/Admin/build_release.scala
   src/Pure/Admin/build_spass.scala
   src/Pure/Admin/build_sqlite.scala
   src/Pure/Admin/build_status.scala
   src/Pure/Admin/build_vampire.scala
   src/Pure/Admin/build_verit.scala
   src/Pure/Admin/build_zipperposition.scala
   src/Pure/Admin/check_sources.scala
   src/Pure/Admin/ci_profile.scala
   src/Pure/Admin/components.scala
   src/Pure/Admin/isabelle_cronjob.scala
   src/Pure/Admin/isabelle_devel.scala
   src/Pure/Admin/jenkins.scala
   src/Pure/Admin/other_isabelle.scala
   src/Pure/Concurrent/consumer_thread.scala
   src/Pure/Concurrent/counter.scala
   src/Pure/Concurrent/delay.scala
   src/Pure/Concurrent/event_timer.scala
   src/Pure/Concurrent/future.scala
   src/Pure/Concurrent/isabelle_thread.scala
   src/Pure/Concurrent/mailbox.scala
   src/Pure/Concurrent/par_list.scala
   src/Pure/Concurrent/synchronized.scala
   src/Pure/GUI/color_value.scala
   src/Pure/GUI/desktop_app.scala
   src/Pure/GUI/gui.scala
   src/Pure/GUI/gui_thread.scala
   src/Pure/GUI/popup.scala
   src/Pure/GUI/wrap_panel.scala
   src/Pure/General/antiquote.scala
   src/Pure/General/bytes.scala
   src/Pure/General/cache.scala
   src/Pure/General/codepoint.scala
   src/Pure/General/comment.scala
   src/Pure/General/completion.scala
   src/Pure/General/csv.scala
   src/Pure/General/date.scala
   src/Pure/General/exn.scala
   src/Pure/General/file.scala
   src/Pure/General/file_watcher.scala
   src/Pure/General/graph.scala
   src/Pure/General/graph_display.scala
   src/Pure/General/graphics_file.scala
   src/Pure/General/http.scala
   src/Pure/General/json.scala
   src/Pure/General/linear_set.scala
   src/Pure/General/logger.scala
   src/Pure/General/long_name.scala
   src/Pure/General/mailman.scala
   src/Pure/General/mercurial.scala
   src/Pure/General/multi_map.scala
   src/Pure/General/output.scala
   src/Pure/General/path.scala
   src/Pure/General/position.scala
   src/Pure/General/pretty.scala
   src/Pure/General/properties.scala
   src/Pure/General/rdf.scala
   src/Pure/General/scan.scala
   src/Pure/General/sha1.scala
   src/Pure/General/sql.scala
   src/Pure/General/ssh.scala
   src/Pure/General/symbol.scala
   src/Pure/General/time.scala
   src/Pure/General/timing.scala
   src/Pure/General/untyped.scala
   src/Pure/General/url.scala
   src/Pure/General/utf8.scala
   src/Pure/General/uuid.scala
   src/Pure/General/value.scala
   src/Pure/General/word.scala
   src/Pure/General/xz.scala
   src/Pure/Isar/document_structure.scala
   src/Pure/Isar/keyword.scala
   src/Pure/Isar/line_structure.scala
   src/Pure/Isar/outer_syntax.scala
   src/Pure/Isar/parse.scala
   src/Pure/Isar/token.scala
   src/Pure/ML/ml_console.scala
   src/Pure/ML/ml_lex.scala
   src/Pure/ML/ml_process.scala
   src/Pure/ML/ml_statistics.scala
   src/Pure/ML/ml_syntax.scala
   src/Pure/PIDE/byte_message.scala
   src/Pure/PIDE/command.scala
   src/Pure/PIDE/command_span.scala
   src/Pure/PIDE/document.scala
   src/Pure/PIDE/document_id.scala
   src/Pure/PIDE/document_status.scala
   src/Pure/PIDE/editor.scala
   src/Pure/PIDE/headless.scala
   src/Pure/PIDE/line.scala
   src/Pure/PIDE/markup.scala
   src/Pure/PIDE/markup_tree.scala
   src/Pure/PIDE/protocol.scala
   src/Pure/PIDE/protocol_handlers.scala
   src/Pure/PIDE/protocol_message.scala
   src/Pure/PIDE/prover.scala
   src/Pure/PIDE/query_operation.scala
   src/Pure/PIDE/rendering.scala
   src/Pure/PIDE/resources.scala
   src/Pure/PIDE/session.scala
   src/Pure/PIDE/text.scala
   src/Pure/PIDE/xml.scala
   src/Pure/PIDE/yxml.scala
   src/Pure/ROOT.scala
   src/Pure/System/bash.scala
   src/Pure/System/command_line.scala
   src/Pure/System/cygwin.scala
   src/Pure/System/distribution.scala
   src/Pure/System/executable.scala
   src/Pure/System/getopts.scala
   src/Pure/System/isabelle_charset.scala
   src/Pure/System/isabelle_fonts.scala
   src/Pure/System/isabelle_platform.scala
   src/Pure/System/isabelle_process.scala
   src/Pure/System/isabelle_system.scala
   src/Pure/System/isabelle_tool.scala
   src/Pure/System/java_statistics.scala
   src/Pure/System/linux.scala
   src/Pure/System/mingw.scala
   src/Pure/System/numa.scala
   src/Pure/System/options.scala
   src/Pure/System/platform.scala
   src/Pure/System/posix_interrupt.scala
   src/Pure/System/process_result.scala
   src/Pure/System/progress.scala
   src/Pure/System/scala.scala
   src/Pure/System/system_channel.scala
   src/Pure/System/tty_loop.scala
   src/Pure/Thy/bibtex.scala
   src/Pure/Thy/export.scala
   src/Pure/Thy/export_theory.scala
   src/Pure/Thy/file_format.scala
   src/Pure/Thy/html.scala
   src/Pure/Thy/latex.scala
   src/Pure/Thy/presentation.scala
   src/Pure/Thy/sessions.scala
   src/Pure/Thy/thy_element.scala
   src/Pure/Thy/thy_header.scala
   src/Pure/Thy/thy_syntax.scala
   src/Pure/Tools/build.scala
   src/Pure/Tools/build_docker.scala
   src/Pure/Tools/build_job.scala
   src/Pure/Tools/check_keywords.scala
   src/Pure/Tools/debugger.scala
   src/Pure/Tools/doc.scala
   src/Pure/Tools/dump.scala
   src/Pure/Tools/fontforge.scala
   src/Pure/Tools/java_monitor.scala
   src/Pure/Tools/logo.scala
   src/Pure/Tools/main.scala
   src/Pure/Tools/mkroot.scala
   src/Pure/Tools/phabricator.scala
   src/Pure/Tools/print_operation.scala
   src/Pure/Tools/profiling_report.scala
   src/Pure/Tools/scala_project.scala
   src/Pure/Tools/server.scala
   src/Pure/Tools/server_commands.scala
   src/Pure/Tools/simplifier_trace.scala
   src/Pure/Tools/spell_checker.scala
   src/Pure/Tools/task_statistics.scala
   src/Pure/Tools/update.scala
   src/Pure/Tools/update_cartouches.scala
   src/Pure/Tools/update_comments.scala
   src/Pure/Tools/update_header.scala
   src/Pure/Tools/update_then.scala
   src/Pure/Tools/update_theorems.scala
   src/Pure/library.scala
   src/Pure/pure_thy.scala
   src/Pure/term.scala
   src/Pure/term_xml.scala
   src/Pure/thm_name.scala
   src/Tools/Graphview/graph_file.scala
   src/Tools/Graphview/graph_panel.scala
   src/Tools/Graphview/graphview.scala
   src/Tools/Graphview/layout.scala
   src/Tools/Graphview/main_panel.scala
   src/Tools/Graphview/metrics.scala
   src/Tools/Graphview/model.scala
   src/Tools/Graphview/mutator.scala
   src/Tools/Graphview/mutator_dialog.scala
   src/Tools/Graphview/mutator_event.scala
   src/Tools/Graphview/popups.scala
   src/Tools/Graphview/shapes.scala
   src/Tools/Graphview/tree_panel.scala
   src/Tools/VSCode/src/build_vscode.scala
   src/Tools/VSCode/src/channel.scala
   src/Tools/VSCode/src/dynamic_output.scala
   src/Tools/VSCode/src/language_server.scala
   src/Tools/VSCode/src/lsp.scala
   src/Tools/VSCode/src/preview_panel.scala
   src/Tools/VSCode/src/state_panel.scala
   src/Tools/VSCode/src/textmate_grammar.scala
   src/Tools/VSCode/src/vscode_model.scala
   src/Tools/VSCode/src/vscode_rendering.scala
   src/Tools/VSCode/src/vscode_resources.scala
   src/Tools/VSCode/src/vscode_spell_checker.scala
 )
 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS]"
   echo
   echo "  Options are:"
   echo "    -f           fresh build"
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
 
 
 ## process command line
 
 # options
 
 FRESH=""
 
 while getopts "f" OPT
 do
   case "$OPT" in
     f)
       FRESH=true
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 [ "$#" -ne 0 ] && usage
 
 
 ## target
 
 TARGET_DIR="lib/classes"
 TARGET_JAR="$TARGET_DIR/Pure.jar"
 TARGET_SHASUM="$TARGET_DIR/Pure.shasum"
 
 function target_shasum()
 {
   shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null
 }
 
 function target_clean()
 {
   rm -rf "$TARGET_DIR"
 }
 
 [ -n "$FRESH" ] && target_clean
 
 
 ## build
 
 target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
 if [ "$?" -ne 0 ]; then
   echo "### Building Isabelle/Scala ..."
 
   target_clean
 
   BUILD_DIR="$TARGET_DIR/build"
   mkdir -p "$BUILD_DIR"
 
   (
     export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
     isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \
       -d "$BUILD_DIR" "${SOURCES[@]}"
   ) || fail "Failed to compile sources"
 
   CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
   mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")"
   echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE"
 
   cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/."
   cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/."
 
   isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \
     -C "$BUILD_DIR" META-INF \
     -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR"
 
   rm -rf "$BUILD_DIR"
 
   target_shasum > "$TARGET_SHASUM"
 fi