# HG changeset patch
# User desharna
# Date 1627410503 -7200
# Node ID 2af4e088c01c4c90fcb6297a859d248c77e3bf29
# Parent  6c8473b4f51862fff13934e9249529471065e42d# Parent  dc98bb7a439bf45b9849030d62e7ab1f8aa1582f
merged

diff -r 6c8473b4f518 -r 2af4e088c01c NEWS
--- a/NEWS	Tue Jul 27 20:25:42 2021 +0200
+++ b/NEWS	Tue Jul 27 20:28:23 2021 +0200
@@ -284,10 +284,13 @@
 process of all Scala/Java modules explicitly. Normally this is done
 implicitly on demand, e.g. for "isabelle scala" or "isabelle jedit".
 
-* Command-line tool "isabelle scala_project" is now more thorough in
-providing Scala/Java sources of all components with etc/build.props,
-including user add-ons. This includes jEdit sources and Isabelle/jEdit
-plugins (jedit_base and jedit_main).
+* Command-line tool "isabelle scala_project" is has been improved in
+various ways:
+  - sources from all components with etc/build.props are included,
+  - sources of for the jEdit text editor and the Isabelle/jEdit
+    plugins (jedit_base and jedit_main) are included by default,
+  - more sources may be given on the command-line,
+  - options -f and -D make the tool more convenient.
 
 * Isabelle/jEdit is now composed more conventionally from the original
 jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle
diff -r 6c8473b4f518 -r 2af4e088c01c src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Tue Jul 27 20:25:42 2021 +0200
+++ b/src/Doc/System/Scala.thy	Tue Jul 27 20:28:23 2021 +0200
@@ -266,12 +266,17 @@
 
 text \<open>
   The @{tool_def scala_project} tool creates a project configuration for all
-  Isabelle/Scala/Java modules specified in components via \<^path>\<open>etc/build.props\<close>:
+  Isabelle/Scala/Java modules specified in components via
+  \<^path>\<open>etc/build.props\<close>, together with additional source files given on
+  the command-line:
+
   @{verbatim [display]
-\<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
+\<open>Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...]
 
   Options are:
-    -L           make symlinks to original scala files
+    -D DIR       project directory (default: "$ISABELLE_HOME_USER/scala_project")
+    -L           make symlinks to original source files
+    -f           force update of existing directory
 
   Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
   such as IntelliJ IDEA.\<close>}
@@ -281,19 +286,36 @@
   IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the
   sources with static analysis and other hints in real-time.
 
-  The specified project directory needs to be fresh. The generated files refer
-  to physical file-system locations, using the path notation of the underlying
-  OS platform. Thus the project needs to be recreated whenever the Isabelle
-  installation is changed or moved.
+  The generated files refer to physical file-system locations, using the path
+  notation of the underlying OS platform. Thus the project needs to be
+  recreated whenever the Isabelle installation is changed or moved.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
+  develop Isabelle/Scala/jEdit modules within an external IDE. Note that the
+  result cannot be built within the IDE: it requires implicit or explicit
+  \<^verbatim>\<open>isabelle scala_build\<close> (\secref{sec:tool-scala-build}) instead.
+
+  The default is to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has
+  no permanent effect on the originals.
 
   \<^medskip>
-  By default, Scala sources are \<^emph>\<open>copied\<close> from the Isabelle distribution and
-  editing them within the IDE has no permanent effect.
+  Option \<^verbatim>\<open>-D\<close> specifies an explicit project directory, instead of the default
+  \<^path>\<open>$ISABELLE_HOME_USER/scala_project\<close>. Option \<^verbatim>\<open>-f\<close> forces an existing
+  project directory to be \<^emph>\<open>purged\<close> --- after some sanity checks that it has
+  been generated by @{tool "scala_project"} before.
+\<close>
+
 
-  Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
-  develop Isabelle/Scala/jEdit within an external Scala IDE. Note that the
-  result cannot be built within the IDE: it requires implicit or explicit
-  \<^verbatim>\<open>isabelle scala_build\<close> (\secref{sec:tool-scala-build}).
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  Create a project directory and for editing the original sources:
+
+  @{verbatim [display] \<open>isabelle scala_project -f -L\<close>}
+
+  On Windows, this usually requires Administrator rights, in order to create
+  native symlinks.
 \<close>
 
 
diff -r 6c8473b4f518 -r 2af4e088c01c src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jul 27 20:25:42 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 27 20:28:23 2021 +0200
@@ -253,7 +253,7 @@
 
   /* symbolic link */
 
-  def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
+  def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit =
   {
     val src_file = src.file
     val dst_file = dst.file
@@ -262,7 +262,14 @@
     if (force) target.delete
 
     def cygwin_link(): Unit =
-      isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
+    {
+      if (native) {
+        error("Failed to create native symlink on Windows: " + quote(src_file.toString) +
+          "\n(but it could work as Administrator)")
+      }
+      else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
+    }
+
 
     try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
     catch {
diff -r 6c8473b4f518 -r 2af4e088c01c src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Tue Jul 27 20:25:42 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala	Tue Jul 27 20:28:23 2021 +0200
@@ -35,17 +35,17 @@
     val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
     val jars2 = contexts.flatMap(_.requirements)
 
-    val jar_files =
+    val jars =
       Library.distinct(jars1 ::: jars2).filterNot(path => contexts.exists(_.is_module(path)))
 
-    val source_files =
+    val sources =
       (for {
         context <- contexts.iterator
         path <- context.sources.iterator
         if path.is_scala || path.is_java
       } yield path).toList
 
-    (jar_files, source_files)
+    (jars, sources)
   }
 
   lazy val isabelle_scala_files: Map[String, Path] =
@@ -92,6 +92,8 @@
 
   /* scala project */
 
+  val default_project_dir = Path.explode("$ISABELLE_HOME_USER/scala_project")
+
   def package_dir(source_file: Path): Option[Path] =
   {
     val lines = split_lines(File.read(source_file))
@@ -107,26 +109,44 @@
   def the_package_dir(source_file: Path): Path =
     package_dir(source_file) getOrElse error("Failed to guess package from " + source_file)
 
-  def scala_project(project_dir: Path, symlinks: Boolean = false): Unit =
+  def scala_project(
+    project_dir: Path = default_project_dir,
+    more_sources: List[Path] = Nil,
+    symlinks: Boolean = false,
+    force: Boolean = false,
+    progress: Progress = new Progress): Unit =
   {
-    if (symlinks && Platform.is_windows)
-      error("Cannot create symlinks on Windows")
+    if (project_dir.file.exists) {
+      val detect =
+        project_dir.is_dir &&
+        (project_dir + Path.explode("build.gradle")).is_file &&
+        (project_dir + Path.explode("src/main/scala")).is_dir
 
-    if (project_dir.is_file || project_dir.is_dir)
-      error("Project directory already exists: " + project_dir)
+      if (force && detect) {
+        progress.echo("Purging existing project directory: " + project_dir.absolute)
+        Isabelle_System.rm_tree(project_dir)
+      }
+      else error("Project directory already exists: " + project_dir.absolute)
+    }
 
-    val java_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/java"))
-    val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
+    progress.echo("Creating project directory: " + project_dir.absolute)
+    Isabelle_System.make_directory(project_dir)
 
-    val (jar_files, source_files) = isabelle_files
+    val java_src_dir = Isabelle_System.make_directory(Path.explode("src/main/java"))
+    val scala_src_dir = Isabelle_System.make_directory(Path.explode("src/main/scala"))
+
+    val (jars, sources) = isabelle_files
     isabelle_scala_files
 
-    for (source <- source_files) {
-      val dir = if (source.is_java) java_src_dir else scala_src_dir
-      val target = dir + the_package_dir(source)
-      Isabelle_System.make_directory(target)
-      if (symlinks) Isabelle_System.symlink(source, target)
-      else Isabelle_System.copy_file(source, target)
+    for (source <- sources ::: more_sources) {
+      val dir = (if (source.is_java) java_src_dir else scala_src_dir) + the_package_dir(source)
+      val target_dir = project_dir + dir
+      if (!target_dir.is_dir) {
+        progress.echo("  Creating package directory: " + dir)
+        Isabelle_System.make_directory(target_dir)
+      }
+      if (symlinks) Isabelle_System.symlink(source.absolute, target_dir, native = true)
+      else Isabelle_System.copy_file(source, target_dir)
     }
 
     File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n")
@@ -142,7 +162,7 @@
 dependencies {
   implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """'
   compile files(
-    """ + jar_files.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
+    """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
 """
 }
 """)
@@ -155,27 +175,31 @@
     Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit",
       Scala_Project.here, args =>
     {
+      var project_dir = default_project_dir
       var symlinks = false
+      var force = false
 
       val getopts = Getopts("""
-Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
+Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...]
 
   Options are:
-    -L           make symlinks to original scala files
+    -D DIR       project directory (default: """ + default_project_dir + """)
+    -L           make symlinks to original source files
+    -f           force update of existing directory
 
   Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
   such as IntelliJ IDEA.
 """,
-        "L" -> (_ => symlinks = true))
+        "D:" -> (arg => project_dir = Path.explode(arg)),
+        "L" -> (_ => symlinks = true),
+        "f" -> (_ => force = true))
 
       val more_args = getopts(args)
 
-      val project_dir =
-        more_args match {
-          case List(dir) => Path.explode(dir)
-          case _ => getopts.usage()
-        }
+      val more_sources = more_args.map(Path.explode)
+      val progress = new Console_Progress
 
-      scala_project(project_dir, symlinks = symlinks)
+      scala_project(project_dir = project_dir, more_sources = more_sources,
+        symlinks = symlinks, force = force, progress = progress)
     })
 }