diff --git a/etc/options b/etc/options
--- a/etc/options
+++ b/etc/options
@@ -1,349 +1,364 @@
 (* :mode=isabelle-options: *)
 
 section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
 
 option document : string = ""
   -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
   -- "control line breaks in non-display material"
 option thy_output_cartouche : bool = false
   -- "indicate if the output should be delimited as cartouche"
 option thy_output_quotes : bool = false
   -- "indicate if the output should be delimited via double quotes"
 option thy_output_margin : int = 76
   -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
 option thy_output_source_cartouche : bool = false
   -- "print original source text rather than internal representation, preserve cartouches"
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
 
 section "Prover Output"
 
 option show_types : bool = false
   -- "show type constraints when printing terms"
 option show_sorts : bool = false
   -- "show sort constraints when printing types"
 option show_brackets : bool = false
   -- "show extra brackets when printing terms/types"
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"
 option goals_limit : int = 10
   -- "maximum number of subgoals to be printed"
 
 option names_long : bool = false
   -- "show fully qualified names"
 option names_short : bool = false
   -- "show base names only"
 option names_unique : bool = true
   -- "show partially qualified names, as required for unique name resolution"
 
 option eta_contract : bool = true
   -- "print terms in eta-contracted form"
 
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"
 
 
 section "Parallel Processing"
 
 public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
 option threads_stack_limit : real = 0.25
   -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 
 public option parallel_limit : int = 0
   -- "approximative limit for parallel tasks (0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 1
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
 option command_timing_threshold : real = 0.1
   -- "default threshold for persistent command timing (seconds)"
 
 
 section "Detail of Proof Checking"
 
 option record_proofs : int = -1
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
 option strict_facts : bool = false
   -- "force lazy facts when defined in context"
 
 
 section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
 
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
 option timeout_scale : real = 1.0
   -- "scale factor for session timeout"
 
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"
 
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
 
 section "ML System"
 
 option ML_print_depth : int = 20
   -- "ML print depth for toplevel pretty-printing"
 
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
 public option ML_exception_debugger : bool = false
   -- "ML debugger exception trace for toplevel command execution"
 
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"
 
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
 
 
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
 public option editor_input_delay : real = 0.3
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0
   -- "delay for machine-generated input that may outperform user edits"
 
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
 public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
 option editor_prune_size : int = 0
   -- "retained size of pruned history (delete old versions)"
 
 public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
 public option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
 public option editor_continuous_checking : bool = true
   -- "continuous checking of proof document (visible and required parts)"
 
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
 public option editor_presentation : bool = false
   -- "dynamic presentation while editing"
 
 
 section "Headless Session"
 
 option headless_consolidate_delay : real = 15
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 option headless_prune_delay : real = 60
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5
   -- "delay for theory status check during PIDE processing (seconds)"
 
 option headless_check_limit : int = 0
   -- "maximum number of theory status checks (0 = unlimited)"
 
 option headless_nodes_status_delay : real = -1
   -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
 
 option headless_watchdog_timeout : real = 600
   -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
 
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
 option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
 section "Miscellaneous Tools"
 
 public option find_theorems_limit : int = 40
   -- "limit of displayed results"
 
 public option find_theorems_tactic_limit : int = 5
   -- "limit of tactic search for 'solves' criterion"
 
 
 section "Completion"
 
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
 public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
   -- "glob patterns to ignore in file-system path completion (separated by colons)"
 
 
 section "Spell Checker"
 
 public option spell_checker : bool = true
   -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_dictionary : string = "en"
   -- "spell-checker dictionary name"
 
 public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
 public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
 section "Secure Shell"
 
 option ssh_config_dir : string = "$HOME/.ssh"
   -- "SSH configuration directory"
 
 option ssh_config_file : string = "$HOME/.ssh/config"
   -- "main SSH configuration file"
 
 option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
   -- "possible SSH identity files (separated by colons)"
 
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
 option ssh_connect_timeout : real = 60
   -- "SSH connection timeout (seconds)"
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
 option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive"
 
 
 section "Theory Export"
 
 option export_document : bool = false
   -- "export document sources to Isabelle/Scala"
 
 option export_theory : bool = false
   -- "export theory content to Isabelle/Scala"
 
 option export_standard_proofs : bool = false
   -- "export standardized proof terms to Isabelle/Scala (not scalable)"
 
 option export_proofs : bool = false
   -- "export proof terms to Isabelle/Scala"
 
 option prune_proofs : bool = false
   -- "prune proof terms after export (do not store in Isabelle/ML)"
 
 
 section "Theory update"
 
 option update_inner_syntax_cartouches : bool = false
   -- "update inner syntax (types, terms, etc.) to use cartouches"
 
 option update_mixfix_cartouches : bool = false
   -- "update mixfix templates to use cartouches instead of double quotes"
 
 option update_control_cartouches : bool = false
   -- "update antiquotations to use control symbol with cartouche argument"
 
 option update_path_cartouches : bool = false
   -- "update file-system paths to use cartouches"
 
 
 section "Build Database"
 
 option build_database_server : bool = false
 option build_database_user : string = ""
 option build_database_password : string = ""
 option build_database_name : string = ""
 option build_database_host : string = ""
 option build_database_port : int = 0
 option build_database_ssh_host : string = ""
 option build_database_ssh_user : string = ""
 option build_database_ssh_port : int = 0
 
 
 section "Build Log Database"
 
 option build_log_database_user : string = ""
 option build_log_database_password : string = ""
 option build_log_database_name : string = ""
 option build_log_database_host : string = ""
 option build_log_database_port : int = 0
 option build_log_ssh_host : string = ""
 option build_log_ssh_user : string = ""
 option build_log_ssh_port : int = 0
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
 
 
+section "Phabricator server"
+
+option phabricator_user : string = "phabricator"
+
+option phabricator_www_user : string = "www-data"
+option phabricator_www_root : string = "/var/www"
+
+option phabricator_smtp_host : string = ""
+option phabricator_smtp_port : int = 465
+option phabricator_smtp_user : string = ""
+option phabricator_smtp_passwd : string = ""
+option phabricator_smtp_protocol : string = "ssl"
+option phabricator_smtp_message_id : bool = true
+
+
 section "Isabelle/Scala/ML system channel"
 
 option system_channel_address : string = ""
 option system_channel_password : string = ""
diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala
+++ b/src/Pure/System/isabelle_tool.scala
@@ -1,176 +1,178 @@
 /*  Title:      Pure/System/isabelle_tool.scala
     Author:     Makarius
     Author:     Lars Hupel
 
 Isabelle system tools: external executables or internal Scala functions.
 */
 
 package isabelle
 
 import java.net.URLClassLoader
 import scala.reflect.runtime.universe
 import scala.tools.reflect.{ToolBox,ToolBoxError}
 
 
 object Isabelle_Tool
 {
   /* Scala source tools */
 
   abstract class Body extends Function[List[String], Unit]
 
   private def compile(path: Path): Body =
   {
     def err(msg: String): Nothing =
       cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
 
     val source = File.read(path)
 
     val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
     val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
 
     try {
       val symbol = tool_box.parse(source) match {
         case tree: universe.ModuleDef => tool_box.define(tree)
         case _ => err("Source does not describe a module (Scala object)")
       }
       tool_box.compile(universe.Ident(symbol))() match {
         case body: Body => body
         case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
       }
     }
     catch {
       case e: ToolBoxError =>
         if (tool_box.frontEnd.hasErrors) {
           val infos = tool_box.frontEnd.infos.toList
           val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
           err(msgs.mkString("\n"))
         }
         else
           err(e.toString)
     }
   }
 
 
   /* external tools */
 
   private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
 
   private def is_external(dir: Path, file_name: String): Boolean =
   {
     val file = (dir + Path.explode(file_name)).file
     try {
       file.isFile && file.canRead &&
         (file_name.endsWith(".scala") || file.canExecute) &&
         !file_name.endsWith("~") && !file_name.endsWith(".orig")
     }
     catch { case _: SecurityException => false }
   }
 
   private def list_external(): List[(String, String)] =
   {
     val Description = """.*\bDESCRIPTION: *(.*)""".r
     for {
       dir <- dirs() if dir.is_dir
       file_name <- File.read_dir(dir) if is_external(dir, file_name)
     } yield {
       val source = File.read(dir + Path.explode(file_name))
       val name = Library.perhaps_unsuffix(".scala", file_name)
       val description =
         split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
       (name, description)
     }
   }
 
   private def find_external(name: String): Option[List[String] => Unit] =
     dirs.collectFirst({
       case dir if is_external(dir, name + ".scala") =>
         compile(dir + Path.explode(name + ".scala"))
       case dir if is_external(dir, name) =>
         (args: List[String]) =>
           {
             val tool = dir + Path.explode(name)
             val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
             sys.exit(result.print_stdout.rc)
           }
     })
 
 
   /* internal tools */
 
   private lazy val internal_tools: List[Isabelle_Tool] =
     Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
       .flatMap(_.tools.toList)
 
   private def list_internal(): List[(String, String)] =
     for (tool <- internal_tools.toList)
       yield (tool.name, tool.description)
 
   private def find_internal(name: String): Option[List[String] => Unit] =
     internal_tools.collectFirst({
       case tool if tool.name == name =>
         args => Command_Line.tool0 { tool.body(args) }
       })
 
 
   /* command line entry point */
 
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       args.toList match {
         case Nil | List("-?") =>
           val tool_descriptions =
             (list_external() ::: list_internal()).sortBy(_._1).
               map({ case (a, "") => a case (a, b) => a + " - " + b })
           Getopts("""
 Usage: isabelle TOOL [ARGS ...]
 
   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
 
 Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
         case tool_name :: tool_args =>
           find_external(tool_name) orElse find_internal(tool_name) match {
             case Some(tool) => tool(tool_args)
             case None => error("Unknown Isabelle tool: " + quote(tool_name))
           }
       }
     }
   }
 }
 
 sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
 
 class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
 
 class Tools extends Isabelle_Scala_Tools(
   Build.isabelle_tool,
   Build_Docker.isabelle_tool,
   Doc.isabelle_tool,
   Dump.isabelle_tool,
   Export.isabelle_tool,
   ML_Process.isabelle_tool,
   Mkroot.isabelle_tool,
   Options.isabelle_tool,
+  Phabricator.isabelle_tool1,
+  Phabricator.isabelle_tool2,
   Present.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,
   Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,
   Update_Header.isabelle_tool,
   Update_Then.isabelle_tool,
   Update_Theorems.isabelle_tool,
   isabelle.vscode.Grammar.isabelle_tool,
   isabelle.vscode.Server.isabelle_tool)
 
 class Admin_Tools extends Isabelle_Scala_Tools(
   Build_Cygwin.isabelle_tool,
   Build_Doc.isabelle_tool,
   Build_Fonts.isabelle_tool,
   Build_JDK.isabelle_tool,
   Build_PolyML.isabelle_tool1,
   Build_PolyML.isabelle_tool2,
   Build_Status.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool)
diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala
new file mode 100644
--- /dev/null
+++ b/src/Pure/Tools/phabricator.scala
@@ -0,0 +1,203 @@
+/*  Title:      Pure/Tools/phabricator.scala
+    Author:     Makarius
+
+Support for Phabricator server. See also:
+  - https://www.phacility.com/phabricator
+  - https://secure.phabricator.com/book/phabricator
+*/
+
+package isabelle
+
+
+object Phabricator
+{
+  /** defaults **/
+
+  val default_name = "vcs"
+
+  def default_prefix(name: String): String = "phabricator_" + name
+
+  def default_root(options: Options, name: String): Path =
+    Path.explode(options.string("phabricator_www_root")) + Path.basic(default_prefix(name))
+
+  def default_repo(options: Options, name: String): Path =
+    default_root(options, name) + Path.basic("repo")
+
+  val packages: List[String] =
+    Build_Docker.packages :::
+    // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
+    List("git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql",
+      "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring")
+
+
+
+  /** global configuration **/
+
+  val global_config = Path.explode("/etc/isabelle-phabricator.conf")
+
+  sealed case class Config(name: String, root: Path)
+
+  def read_config(): List[Config] =
+  {
+    if (global_config.is_file) {
+      for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
+      yield {
+        space_explode(':', entry) match {
+          case List(name, root) => Config(name, Path.explode(root))
+          case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
+        }
+      }
+    }
+    else Nil
+  }
+
+  def write_config(configs: List[Config])
+  {
+    File.write(global_config,
+      configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
+  }
+
+  def get_config(name: String): Config =
+    read_config().find(config => config.name == name) getOrElse
+      error("Bad Isabelle/Phabricator installation " + quote(name))
+
+
+
+  /** setup **/
+
+  def phabricator_setup(
+    options: Options,
+    name: String = default_name,
+    prefix: String = "",
+    root: String = "",
+    repo: String = "",
+    progress: Progress = No_Progress)
+  {
+    /* system environment */
+
+    Linux.check_system_root()
+
+    Linux.package_update(progress = progress)
+    Linux.check_reboot_required()
+
+    Linux.package_install(packages, progress = progress)
+    Linux.check_reboot_required()
+
+
+    /* basic installation */
+
+    val prefix_name = proper_string(prefix) getOrElse default_prefix(name)
+    val root_path = if (root.nonEmpty) Path.explode(root) else default_root(options, name)
+    val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(options, name)
+
+    val configs = read_config()
+
+    for (config <- configs if config.name == name) {
+      error("Duplicate Phabricator installation " + quote(name) + " in " + config.root)
+    }
+
+    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
+      error("Failed to create root directory " + root_path)
+    }
+
+    progress.bash(cwd = root_path.file, echo = true,
+      script = """
+        set -e
+        chown """ + Bash.string(options.string("phabricator_www_user")) + """ .
+        chmod 755 .
+
+        git clone https://github.com/phacility/libphutil.git
+        git clone https://github.com/phacility/arcanist.git
+        git clone https://github.com/phacility/phabricator.git
+      """).check
+
+    val config = Config(name, root_path)
+    write_config(configs ::: List(config))
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool1 =
+    Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
+    {
+      var options = Options.init()
+      var prefix = ""
+      var root = ""
+      var repo = ""
+
+      val getopts =
+        Getopts("""
+Usage: isabelle phabricator_setup [OPTIONS] [NAME]
+
+  Options are:
+    -R DIR       repository directory (default: """ + default_repo(options, "NAME") + """)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p PREFIX    prefix for derived names (default: """ + default_prefix("NAME") + """)
+    -r DIR       installation root directory (default: """ + default_root(options, "NAME") + """)
+
+  Install Phabricator as Ubuntu LAMP application (Linux, Apache, MySQL, PHP).
+
+  Slogan: "Discuss. Plan. Code. Review. Test.
+  Every application your project needs, all in one tool."
+
+  The installation NAME (default: """ + quote(default_name) + """) is mapped to
+  a regular Unix user and used for public SSH access.
+""",
+          "R:" -> (arg => repo = arg),
+          "o:" -> (arg => options = options + arg),
+          "p:" -> (arg => prefix = arg),
+          "r:" -> (arg => root = arg))
+
+      val more_args = getopts(args)
+
+      val name =
+        more_args match {
+          case Nil => default_name
+          case List(name) => name
+          case _ => getopts.usage()
+        }
+
+      val progress = new Console_Progress
+
+      phabricator_setup(options, name, prefix = prefix, root = root, repo = repo,
+        progress = progress)
+    })
+
+
+
+  /** update **/
+
+  def phabricator_update(name: String, progress: Progress = No_Progress)
+  {
+    Linux.check_system_root()
+
+    ???
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool2 =
+    Isabelle_Tool("phabricator_update", "update Phabricator server installation", args =>
+    {
+      val getopts =
+        Getopts("""
+Usage: isabelle phabricator_update [NAME]
+
+  Update Phabricator installation, with lookup of NAME (default + """ + quote(default_name) + """)
+  in """ + global_config + "\n")
+
+      val more_args = getopts(args)
+      val name =
+        more_args match {
+          case Nil => default_name
+          case List(name) => name
+          case _ => getopts.usage()
+        }
+
+      val progress = new Console_Progress
+
+      phabricator_update(name, progress = progress)
+    })
+}
diff --git a/src/Pure/build-jars b/src/Pure/build-jars
--- a/src/Pure/build-jars
+++ b/src/Pure/build-jars
@@ -1,321 +1,322 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # build-jars - build Isabelle/Scala
 #
 # Requires proper Isabelle settings environment.
 
 ## sources
 
 declare -a SOURCES=(
   Admin/afp.scala
   Admin/build_cygwin.scala
   Admin/build_doc.scala
   Admin/build_fonts.scala
   Admin/build_history.scala
   Admin/build_jdk.scala
   Admin/build_log.scala
   Admin/build_polyml.scala
   Admin/build_release.scala
   Admin/build_status.scala
   Admin/check_sources.scala
   Admin/ci_profile.scala
   Admin/components.scala
   Admin/isabelle_cronjob.scala
   Admin/isabelle_devel.scala
   Admin/jenkins.scala
   Admin/other_isabelle.scala
   Concurrent/consumer_thread.scala
   Concurrent/counter.scala
   Concurrent/event_timer.scala
   Concurrent/future.scala
   Concurrent/mailbox.scala
   Concurrent/par_list.scala
   Concurrent/standard_thread.scala
   Concurrent/synchronized.scala
   GUI/color_value.scala
   GUI/gui.scala
   GUI/gui_thread.scala
   GUI/popup.scala
   GUI/wrap_panel.scala
   General/antiquote.scala
   General/bytes.scala
   General/cache.scala
   General/codepoint.scala
   General/comment.scala
   General/completion.scala
   General/csv.scala
   General/date.scala
   General/exn.scala
   General/file.scala
   General/file_watcher.scala
   General/graph.scala
   General/graph_display.scala
   General/graphics_file.scala
   General/http.scala
   General/json.scala
   General/linear_set.scala
   General/logger.scala
   General/long_name.scala
   General/mercurial.scala
   General/multi_map.scala
   General/output.scala
   General/path.scala
   General/position.scala
   General/pretty.scala
   General/properties.scala
   General/rdf.scala
   General/scan.scala
   General/sha1.scala
   General/sql.scala
   General/ssh.scala
   General/symbol.scala
   General/time.scala
   General/timing.scala
   General/untyped.scala
   General/url.scala
   General/utf8.scala
   General/uuid.scala
   General/value.scala
   General/word.scala
   General/xz.scala
   Isar/document_structure.scala
   Isar/keyword.scala
   Isar/line_structure.scala
   Isar/outer_syntax.scala
   Isar/parse.scala
   Isar/token.scala
   ML/ml_console.scala
   ML/ml_lex.scala
   ML/ml_process.scala
   ML/ml_statistics.scala
   ML/ml_syntax.scala
   PIDE/byte_message.scala
   PIDE/command.scala
   PIDE/command_span.scala
   PIDE/document.scala
   PIDE/document_id.scala
   PIDE/document_status.scala
   PIDE/editor.scala
   PIDE/headless.scala
   PIDE/line.scala
   PIDE/markup.scala
   PIDE/markup_tree.scala
   PIDE/protocol.scala
   PIDE/protocol_handlers.scala
   PIDE/protocol_message.scala
   PIDE/prover.scala
   PIDE/query_operation.scala
   PIDE/rendering.scala
   PIDE/resources.scala
   PIDE/session.scala
   PIDE/text.scala
   PIDE/xml.scala
   PIDE/yxml.scala
   ROOT.scala
   System/bash.scala
   System/command_line.scala
   System/cygwin.scala
   System/distribution.scala
   System/getopts.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
   System/isabelle_fonts.scala
   System/isabelle_process.scala
   System/isabelle_system.scala
   System/isabelle_tool.scala
   System/linux.scala
   System/numa.scala
   System/options.scala
   System/platform.scala
   System/posix_interrupt.scala
   System/process_result.scala
   System/progress.scala
   System/system_channel.scala
   System/tty_loop.scala
   Thy/bibtex.scala
   Thy/export.scala
   Thy/export_theory.scala
   Thy/file_format.scala
   Thy/html.scala
   Thy/latex.scala
   Thy/present.scala
   Thy/sessions.scala
   Thy/thy_element.scala
   Thy/thy_header.scala
   Thy/thy_syntax.scala
   Tools/build.scala
   Tools/build_docker.scala
   Tools/check_keywords.scala
   Tools/debugger.scala
   Tools/doc.scala
   Tools/dump.scala
   Tools/fontforge.scala
   Tools/main.scala
   Tools/mkroot.scala
+  Tools/phabricator.scala
   Tools/print_operation.scala
   Tools/profiling_report.scala
   Tools/server.scala
   Tools/server_commands.scala
   Tools/simplifier_trace.scala
   Tools/spell_checker.scala
   Tools/task_statistics.scala
   Tools/update.scala
   Tools/update_cartouches.scala
   Tools/update_comments.scala
   Tools/update_header.scala
   Tools/update_then.scala
   Tools/update_theorems.scala
   library.scala
   pure_thy.scala
   term.scala
   term_xml.scala
   thm_name.scala
   ../Tools/Graphview/graph_file.scala
   ../Tools/Graphview/graph_panel.scala
   ../Tools/Graphview/graphview.scala
   ../Tools/Graphview/layout.scala
   ../Tools/Graphview/main_panel.scala
   ../Tools/Graphview/metrics.scala
   ../Tools/Graphview/model.scala
   ../Tools/Graphview/mutator.scala
   ../Tools/Graphview/mutator_dialog.scala
   ../Tools/Graphview/mutator_event.scala
   ../Tools/Graphview/popups.scala
   ../Tools/Graphview/shapes.scala
   ../Tools/Graphview/tree_panel.scala
   ../Tools/VSCode/src/build_vscode.scala
   ../Tools/VSCode/src/channel.scala
   ../Tools/VSCode/src/document_model.scala
   ../Tools/VSCode/src/dynamic_output.scala
   ../Tools/VSCode/src/grammar.scala
   ../Tools/VSCode/src/preview_panel.scala
   ../Tools/VSCode/src/protocol.scala
   ../Tools/VSCode/src/server.scala
   ../Tools/VSCode/src/state_panel.scala
   ../Tools/VSCode/src/vscode_javascript.scala
   ../Tools/VSCode/src/vscode_rendering.scala
   ../Tools/VSCode/src/vscode_resources.scala
   ../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
 
 
 ## build
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
 TARGET="$TARGET_DIR/Pure.jar"
 
 declare -a UPDATED=()
 
 if [ -n "$FRESH" ]; then
   OUTDATED=true
 else
   OUTDATED=false
   if [ ! -e "$TARGET" ]; then
     OUTDATED=true
   else
     for DEP in "${SOURCES[@]}"
     do
       [ ! -e "$DEP" ] && fail "Missing file: $DEP"
       [ "$DEP" -nt "$TARGET" ] && {
         OUTDATED=true
         UPDATED["${#UPDATED[@]}"]="$DEP"
       }
     done
   fi
 fi
 
 if [ "$OUTDATED" = true ]
 then
   echo "### Building Isabelle/Scala ..."
 
   [ "${#UPDATED[@]}" -gt 0 ] && {
     echo "Changed files:"
     for FILE in "${UPDATED[@]}"
     do
       echo "  $FILE"
     done
   }
 
   rm -f "$TARGET"
   rm -rf classes && mkdir classes
 
   SCALAC_OPTIONS="$ISABELLE_SCALAC_OPTIONS -d classes"
 
   (
     classpath classes
     export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
 
     isabelle_scala scalac $SCALAC_OPTIONS "${SOURCES[@]}" || \
       fail "Failed to compile sources"
   ) || exit "$?"
 
   mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
 
   pushd classes >/dev/null
 
   CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
   mkdir -p "$(dirname "$CHARSET_SERVICE")"
   echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"
 
   cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/.
   cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/.
 
   isabelle_jdk jar cfe "$(platform_path "$TARGET")" isabelle.Main META-INF isabelle || \
     fail "Failed to produce $TARGET"
 
   popd >/dev/null
 
   rm -rf classes
 fi