added "isabelle scala_project" to support e.g. IntelliJ IDEA;

--- a/NEWS	Wed Jan 15 13:22:16 2020 +0100
+++ b/NEWS	Wed Jan 15 15:05:33 2020 +0100
@@ -110,6 +110,10 @@
 
 *** System ***
 
+* The command-line tool "isabelle scala_project" creates a Gradle
+project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
+such as IntelliJ IDEA.
+
 * Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
 have been discontinued -- deprecated since Isabelle2018.
 

--- a/src/Doc/System/Scala.thy	Wed Jan 15 13:22:16 2020 +0100
+++ b/src/Doc/System/Scala.thy	Wed Jan 15 15:05:33 2020 +0100
@@ -93,4 +93,38 @@
   form.
 \<close>
 
+
+section \<open>Project setup for common Scala IDEs\<close>
+
+text \<open>
+  The @{tool_def scala_project} tool creates a Gradle 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 project 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 must not exist yet. The generated files
+  refer to physical file 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.
+
+  Alternatively, option \<^verbatim>\<open>-l\<close> may be used to produce symlinks 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>
+
 end

--- a/src/Pure/System/isabelle_tool.scala	Wed Jan 15 13:22:16 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Wed Jan 15 15:05:33 2020 +0100
@@ -159,6 +159,7 @@
   Present.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,
+  Scala_Project.isabelle_tool,
   Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/scala_project.scala	Wed Jan 15 15:05:33 2020 +0100
@@ -0,0 +1,143 @@
+/*  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 */
+
+  def 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"))
+        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/jars/Isabelle-jEdit-base.jar" &&
+          name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar"
+      } yield name)
+
+    files1 ::: files2
+  }
+
+  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"))
+
+
+  /* scala project */
+
+  def scala_project(project_dir: Path, symlinks: Boolean = false)
+  {
+    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")
+    Isabelle_System.mkdirs(src_dir)
+
+    val files = isabelle_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), src_dir + p)
+        }).getOrElse(error("Unknown directory prefix for " + quote(file)))
+
+      Isabelle_System.mkdirs(target)
+      if (symlinks) File.link(path, target) else File.copy(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", 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)
+    })
+}

--- a/src/Pure/build-jars	Wed Jan 15 13:22:16 2020 +0100
+++ b/src/Pure/build-jars	Wed Jan 15 15:05:33 2020 +0100
@@ -157,6 +157,7 @@
   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