--- 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
--- 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>
--- 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 {
--- 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)
})
}