# 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 \ The @{tool_def scala_project} tool creates a project configuration for all - Isabelle/Scala/Java modules specified in components via \<^path>\etc/build.props\: + Isabelle/Scala/Java modules specified in components via + \<^path>\etc/build.props\, together with additional source files given on + the command-line: + @{verbatim [display] -\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: "$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.\} @@ -281,19 +286,36 @@ IDEA\<^footnote>\\<^url>\https://www.jetbrains.com/idea\\. 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>\-L\ produces \<^emph>\symlinks\ 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>\isabelle scala_build\ (\secref{sec:tool-scala-build}) instead. + + The default is to \<^emph>\copy\ source files, so editing them within the IDE has + no permanent effect on the originals. \<^medskip> - By default, Scala sources are \<^emph>\copied\ from the Isabelle distribution and - editing them within the IDE has no permanent effect. + Option \<^verbatim>\-D\ specifies an explicit project directory, instead of the default + \<^path>\$ISABELLE_HOME_USER/scala_project\. Option \<^verbatim>\-f\ forces an existing + project directory to be \<^emph>\purged\ --- after some sanity checks that it has + been generated by @{tool "scala_project"} before. +\ + - Option \<^verbatim>\-L\ produces \<^emph>\symlinks\ 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>\isabelle scala_build\ (\secref{sec:tool-scala-build}). +subsubsection \Examples\ + +text \ + Create a project directory and for editing the original sources: + + @{verbatim [display] \isabelle scala_project -f -L\} + + On Windows, this usually requires Administrator rights, in order to create + native symlinks. \ 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) }) }