diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML
+++ b/src/Pure/ROOT.ML
@@ -1,356 +1,356 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
 
 Main entry point for the Isabelle/Pure bootstrap process.
 
 Note: When this file is open in the Prover IDE, the ML files of
 Isabelle/Pure can be explored interactively. This is a separate copy of
 Pure within Pure: it does not affect the running logic session.
 *)
 
 chapter "Isabelle/Pure bootstrap";
 
 ML_file "ML/ml_name_space.ML";
 
 
 section "Bootstrap phase 0: Poly/ML setup";
 
 ML_file "ML/ml_init.ML";
 ML_file "ML/ml_system.ML";
 ML_file "System/distribution.ML";
 
 ML_file "General/basics.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_profiling.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
 
 
 section "Bootstrap phase 1: towards ML within position context";
 
 subsection "Library of general tools";
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 
 ML_file "General/random.ML";
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";
 ML_file "General/symbol.ML";
 ML_file "General/position.ML";
 ML_file "General/symbol_pos.ML";
 ML_file "General/input.ML";
 ML_file "General/comment.ML";
 ML_file "General/antiquote.ML";
 ML_file "ML/ml_lex.ML";
 ML_file "ML/ml_compiler1.ML";
 
 
 section "Bootstrap phase 2: towards ML within Isar context";
 
 subsection "Library of general tools";
 
 ML_file "General/integer.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
 ML_file "General/same.ML";
 ML_file "General/ord_list.ML";
 ML_file "General/balanced_tree.ML";
 ML_file "General/linear_set.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
 ML_file "General/rat.ML";
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash_syntax.ML";
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/socket_io.ML";
 ML_file "General/seq.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/yxml.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 
 ML_file "General/change_table.ML";
 ML_file "General/graph.ML";
 
 ML_file "System/options.ML";
 
 
 subsection "Fundamental structures";
 
 ML_file "name.ML";
 ML_file "term.ML";
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
 ML_file "soft_type_system.ML";
 
 
 subsection "Concurrency within the ML runtime";
 
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "ML/ml_statistics.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
 ML_file "Concurrent/future.ML";
 ML_file "Concurrent/event_timer.ML";
 ML_file "Concurrent/timeout.ML";
 ML_file "Concurrent/lazy.ML";
 ML_file "Concurrent/par_list.ML";
 
 ML_file "Concurrent/mailbox.ML";
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
 ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
 
 ML_file "Syntax/type_annotation.ML";
 ML_file "Syntax/term_position.ML";
 ML_file "Syntax/lexicon.ML";
 ML_file "Syntax/ast.ML";
 ML_file "Syntax/syntax_ext.ML";
 ML_file "Syntax/parser.ML";
 ML_file "Syntax/syntax_trans.ML";
 ML_file "Syntax/mixfix.ML";
 ML_file "Syntax/printer.ML";
 ML_file "Syntax/syntax.ML";
 
 
 subsection "Core of tactical proof system";
 
 ML_file "term_ord.ML";
 ML_file "term_subst.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";
 ML_file "Syntax/simple_syntax.ML";
 ML_file "net.ML";
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
 ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
 ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
 ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
 ML_file "morphism.ML";
 ML_file "variable.ML";
 ML_file "conv.ML";
 ML_file "goal_display.ML";
 ML_file "tactical.ML";
 ML_file "search.ML";
 ML_file "tactic.ML";
 ML_file "raw_simplifier.ML";
 ML_file "conjunction.ML";
 ML_file "assumption.ML";
 
 
 subsection "Isar -- Intelligible Semi-Automated Reasoning";
 
 (*ML support and global execution*)
 ML_file "ML/ml_syntax.ML";
 ML_file "ML/ml_env.ML";
 ML_file "ML/ml_options.ML";
 ML_file "ML/ml_print_depth.ML";
 ML_file_no_debug "Isar/runtime.ML";
 ML_file "PIDE/execution.ML";
 ML_file "ML/ml_compiler.ML";
 
 ML_file "skip_proof.ML";
 ML_file "goal.ML";
 
 (*outer syntax*)
 ML_file "Isar/keyword.ML";
 ML_file "Isar/token.ML";
 ML_file "Isar/parse.ML";
 ML_file "Thy/document_source.ML";
 ML_file "Thy/thy_header.ML";
 ML_file "Thy/document_marker.ML";
 
 (*proof context*)
 ML_file "Isar/object_logic.ML";
 ML_file "Isar/rule_cases.ML";
 ML_file "Isar/auto_bind.ML";
 ML_file "type_infer.ML";
 ML_file "Syntax/local_syntax.ML";
 ML_file "Isar/proof_context.ML";
 ML_file "type_infer_context.ML";
 ML_file "Syntax/syntax_phases.ML";
 ML_file "Isar/args.ML";
 
 (*theory specifications*)
 ML_file "Isar/local_defs.ML";
 ML_file "Isar/local_theory.ML";
 ML_file "Isar/entity.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_element.ML";
 ML_file "Thy/markdown.ML";
 ML_file "Thy/html.ML";
 ML_file "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
 
 (*basic proof engine*)
 ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
 ML_file "Isar/proof_display.ML";
 ML_file "Isar/attrib.ML";
 ML_file "Isar/context_rules.ML";
 ML_file "Isar/method.ML";
 ML_file "Isar/proof.ML";
 ML_file "Isar/element.ML";
 ML_file "Isar/obtain.ML";
 ML_file "Isar/subgoal.ML";
 ML_file "Isar/calculation.ML";
 
 (*local theories and targets*)
 ML_file "Isar/locale.ML";
 ML_file "Isar/generic_target.ML";
 ML_file "Isar/overloading.ML";
 ML_file "axclass.ML";
 ML_file "Isar/class.ML";
 ML_file "Isar/named_target.ML";
 ML_file "Isar/expression.ML";
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
 ML_file "Isar/bundle.ML";
 ML_file "Isar/experiment.ML";
 
 ML_file "simplifier.ML";
 ML_file "Tools/plugin.ML";
 
 (*executable theory content*)
 ML_file "Isar/code.ML";
 
 (*specifications*)
 ML_file "Isar/spec_rules.ML";
 ML_file "Isar/specification.ML";
 ML_file "Isar/parse_spec.ML";
 ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
 ML_file "Isar/proof_node.ML";
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
 ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_syntax.ML";
 ML_file "Proof/proof_checker.ML";
 ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
 ML_file "System/bash.ML";
 ML_file "System/isabelle_system.ML";
 
 
 (*theory documents*)
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "ML/ml_antiquotations.ML";
 ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/thy_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
 ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "thm_deps.ML";
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/document.ML";
 
 (*theory and proof operations*)
 ML_file "Isar/isar_cmd.ML";
 
 
 subsection "Isabelle/Isar system";
 
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
-ML_file "System/invoke_scala.ML";
+ML_file "System/scala.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 
 
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
 ML_file "ML/ml_pp.ML";
 ML_file "ML/ml_thms.ML";
 ML_file "ML/ml_file.ML";
 
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";
 ML_file "Tools/rail.ML";
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thy_deps.ML";
 ML_file "Tools/class_deps.ML";
 ML_file "Tools/find_theorems.ML";
 ML_file "Tools/find_consts.ML";
 ML_file "Tools/simplifier_trace.ML";
 ML_file_no_debug "Tools/debugger.ML";
 ML_file "Tools/named_theorems.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
diff --git a/src/Pure/System/invoke_scala.ML b/src/Pure/System/scala.ML
rename from src/Pure/System/invoke_scala.ML
rename to src/Pure/System/scala.ML
--- a/src/Pure/System/invoke_scala.ML
+++ b/src/Pure/System/scala.ML
@@ -1,69 +1,70 @@
-(*  Title:      Pure/System/invoke_scala.ML
+(*  Title:      Pure/System/scala.ML
     Author:     Makarius
 
-JVM method invocation service via Isabelle/Scala.
+Support for Scala at runtime.
 *)
 
-signature INVOKE_SCALA =
+signature SCALA =
 sig
   val method: string -> string -> string
   val promise_method: string -> string -> string future
   exception Null
 end;
 
-structure Invoke_Scala: INVOKE_SCALA =
+structure Scala: SCALA =
 struct
 
-val _ = Session.protocol_handler "isabelle.Invoke_Scala";
+(** invoke JVM method via Isabelle/Scala **)
+
+val _ = Session.protocol_handler "isabelle.Scala";
 
 
 (* pending promises *)
 
 val new_id = string_of_int o Counter.make ();
 
 val promises =
-  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
+  Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
 
 
 (* method invocation *)
 
 fun promise_method name arg =
   let
     val id = new_id ();
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
     val promise = Future.promise_name "invoke_scala" abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   in promise end;
 
 fun method name arg = Future.join (promise_method name arg);
 
 
 (* fulfill *)
 
 exception Null;
 
 fun fulfill id tag res =
   let
     val result =
       (case tag of
         "0" => Exn.Exn Null
       | "1" => Exn.Res res
       | "2" => Exn.Exn (ERROR res)
       | "3" => Exn.Exn (Fail res)
       | "4" => Exn.Exn Exn.Interrupt
       | _ => raise Fail "Bad tag");
     val promise =
       Synchronized.change_result promises
         (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
     val _ = Future.fulfill_result promise result;
   in () end;
 
 val _ =
-  Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
+  Isabelle_Process.protocol_command "Scala.fulfill"
     (fn [id, tag, res] =>
       fulfill id tag res
         handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
 
 end;
-
diff --git a/src/Pure/System/invoke_scala.scala b/src/Pure/System/scala.scala
rename from src/Pure/System/invoke_scala.scala
rename to src/Pure/System/scala.scala
--- a/src/Pure/System/invoke_scala.scala
+++ b/src/Pure/System/scala.scala
@@ -1,128 +1,130 @@
-/*  Title:      Pure/System/invoke_scala.scala
+/*  Title:      Pure/System/scala.scala
     Author:     Makarius
 
-JVM method invocation service via Isabelle/Scala.
+Support for Scala at runtime.
 */
 
 package isabelle
 
 
 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
 
 import scala.util.matching.Regex
 
 
-object Invoke_Scala
+object Scala
 {
+  /** invoke JVM method via Isabelle/Scala **/
+
   /* method reflection */
 
   private val Ext = new Regex("(.*)\\.([^.]*)")
   private val STRING = Class.forName("java.lang.String")
 
   private def get_method(name: String): String => String =
     name match {
       case Ext(class_name, method_name) =>
         val m =
           try { Class.forName(class_name).getMethod(method_name, STRING) }
           catch {
             case _: ClassNotFoundException | _: NoSuchMethodException =>
               error("No such method: " + quote(name))
           }
         if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
         if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
 
         (arg: String) => {
           try { m.invoke(null, arg).asInstanceOf[String] }
           catch {
             case e: InvocationTargetException if e.getCause != null =>
               throw e.getCause
           }
         }
       case _ => error("Malformed method name: " + quote(name))
     }
 
 
   /* method invocation */
 
   object Tag extends Enumeration
   {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
   def method(name: String, arg: String): (Tag.Value, String) =
     Exn.capture { get_method(name) } match {
       case Exn.Res(f) =>
         Exn.capture { f(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
     }
 }
 
 
 /* protocol handler */
 
-class Invoke_Scala extends Session.Protocol_Handler
+class Scala extends Session.Protocol_Handler
 {
   private var session: Session = null
   private var futures = Map.empty[String, Future[Unit]]
 
   override def init(init_session: Session): Unit =
     synchronized { session = init_session }
 
   override def exit(): Unit = synchronized
   {
     for ((id, future) <- futures) cancel(id, future)
     futures = Map.empty
   }
 
-  private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
+  private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit =
     synchronized
     {
       if (futures.isDefinedAt(id)) {
-        session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
+        session.protocol_command("Scala.fulfill", id, tag.id.toString, res)
         futures -= id
       }
     }
 
   private def cancel(id: String, future: Future[Unit])
   {
     future.cancel
-    fulfill(id, Invoke_Scala.Tag.INTERRUPT, "")
+    fulfill(id, Scala.Tag.INTERRUPT, "")
   }
 
   private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
           Future.fork {
-            val (tag, result) = Invoke_Scala.method(name, msg.text)
+            val (tag, result) = Scala.method(name, msg.text)
             fulfill(id, tag, result)
           })
         true
       case _ => false
     }
   }
 
   private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Cancel_Scala(id) =>
         futures.get(id) match {
           case Some(future) => cancel(id, future)
           case None =>
         }
         true
       case _ => false
     }
   }
 
   val functions =
     List(
       Markup.Invoke_Scala.name -> invoke_scala,
       Markup.Cancel_Scala.name -> cancel_scala)
 }
diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML
+++ b/src/Pure/Thy/bibtex.ML
@@ -1,64 +1,64 @@
 (*  Title:      Pure/Thy/bibtex.ML
     Author:     Makarius
 
 BibTeX support.
 *)
 
 signature BIBTEX =
 sig
   val check_database:
     Position.T -> string -> (string * Position.T) list * (string * Position.T) list
   val check_database_output: Position.T -> string -> unit
   val cite_macro: string Config.T
 end;
 
 structure Bibtex: BIBTEX =
 struct
 
 (* check database *)
 
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  Invoke_Scala.method "isabelle.Bibtex.check_database_yxml" database
+  Scala.method "isabelle.Bibtex.check_database_yxml" database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
   |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
 
 fun check_database_output pos0 database =
   let val (errors, warnings) = check_database pos0 database in
     errors |> List.app (fn (msg, pos) =>
       Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
     warnings |> List.app (fn (msg, pos) =>
       warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
   end;
 
 
 (* document antiquotations *)
 
 val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
 
 val _ =
   Theory.setup
    (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
     Thy_Output.antiquotation_raw \<^binding>\<open>cite\<close>
       (Scan.lift
         (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position))
       (fn ctxt => fn (opt, citations) =>
         let
           val thy = Proof_Context.theory_of ctxt;
           val bibtex_entries = Present.get_bibtex_entries thy;
           val _ =
             if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then ()
             else
               citations |> List.app (fn (name, pos) =>
                 if member (op =) bibtex_entries name then ()
                 else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
           val _ =
             Context_Position.reports ctxt
               (map (fn (name, pos) => (pos, Markup.citation name)) citations);
           val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
           val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
         in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
 
 end;
diff --git a/src/Pure/build-jars b/src/Pure/build-jars
--- a/src/Pure/build-jars
+++ b/src/Pure/build-jars
@@ -1,306 +1,306 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # build-jars - build Isabelle/Scala
 #
 # Requires proper Isabelle settings environment.
 
 ## sources
 
 declare -a SOURCES=(
   src/Pure/Admin/afp.scala
   src/Pure/Admin/build_cygwin.scala
   src/Pure/Admin/build_doc.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_status.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/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/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/getopts.scala
-  src/Pure/System/invoke_scala.scala
   src/Pure/System/isabelle_charset.scala
   src/Pure/System/isabelle_fonts.scala
   src/Pure/System/isabelle_process.scala
   src/Pure/System/isabelle_system.scala
   src/Pure/System/isabelle_tool.scala
   src/Pure/System/linux.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/present.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/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/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/document_model.scala
   src/Tools/VSCode/src/dynamic_output.scala
   src/Tools/VSCode/src/grammar.scala
   src/Tools/VSCode/src/preview_panel.scala
   src/Tools/VSCode/src/protocol.scala
   src/Tools/VSCode/src/server.scala
   src/Tools/VSCode/src/state_panel.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