diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala
+++ b/src/Pure/Tools/scala_project.scala
@@ -1,191 +1,199 @@
/* Title: Pure/Tools/scala_project.scala
Author: Makarius
Setup Gradle project for Isabelle/Scala/jEdit.
*/
package isabelle
import scala.jdk.CollectionConverters._
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 plugin_contexts(): List[isabelle.setup.Build.Context] =
+ for (plugin <- List("jedit_base", "jedit_main"))
+ yield {
+ val dir = Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin)
+ isabelle.setup.Build.directory_context(dir.java_path)
+ }
+
lazy val isabelle_files: (List[Path], List[Path]) =
{
- val component_contexts =
- isabelle.setup.Build.component_contexts().asScala.toList
+ val contexts =
+ isabelle.setup.Build.component_contexts().asScala.toList :::
+ plugin_contexts()
val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
val jars2 =
(for {
- context <- component_contexts.iterator
+ context <- contexts.iterator
s <- context.requirements().asScala.iterator
path <- context.requirement_paths(s).asScala.iterator
} yield File.path(path.toFile)).toList
val jar_files =
- (jars1 ::: jars2).filterNot(path =>
- component_contexts.exists(context =>
+ Library.distinct(jars1 ::: jars2).filterNot(path =>
+ contexts.exists(context =>
{
val name: String = context.module_name()
name.nonEmpty && File.eq(context.path(name).toFile, path.file)
}))
val source_files =
(for {
- context <- component_contexts.iterator
+ context <- contexts.iterator
file <- context.sources.asScala.iterator
if file.endsWith(".scala") || file.endsWith(".java")
} yield File.path(context.path(file).toFile)).toList
(jar_files, source_files)
}
lazy val isabelle_scala_files: Map[String, Path] =
{
val context = isabelle.setup.Build.component_context(Path.ISABELLE_HOME.java_path)
context.sources().asScala.iterator.foldLeft(Map.empty[String, Path]) {
case (map, name) =>
if (name.endsWith(".scala")) {
val path = File.path(context.path(name).toFile)
val base = path.base.implode
map.get(base) match {
case None => map + (base -> path)
case Some(path2) => error("Conflicting base names: " + path + " vs. " + path2)
}
}
else map
}
}
/* compile-time position */
def here: Here =
{
val exn = new Exception
exn.getStackTrace.toList match {
case _ :: caller :: _ =>
val name = proper_string(caller.getFileName).getOrElse("")
val line = caller.getLineNumber
new Here(name, line)
case _ => new Here("", 0)
}
}
class Here private[Scala_Project](name: String, line: Int)
{
override def toString: String = name + ":" + line
def position: Position.T =
isabelle_scala_files.get(name) match {
case Some(path) => Position.Line_File(line, path.implode)
case None => Position.none
}
}
/* scala project */
def package_dir(source_file: Path): Option[Path] =
{
val is_java = source_file.file_name.endsWith(".java")
val lines = split_lines(File.read(source_file))
val Package = """\s*\bpackage\b\s*(?:object\b\s*)?((?:\w|\.)+)\b.*""".r
lines.collectFirst(
{
case Package(name) =>
if (is_java) Path.explode(space_explode('.', name).mkString("/"))
else Path.basic(name)
})
}
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 =
{
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 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"))
val (jar_files, source_files) = isabelle_files
isabelle_scala_files
for (source <- source_files) {
val dir = if (source.file_name.endsWith(".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)
}
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(
""" + jar_files.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",
Scala_Project.here, 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)
})
}
diff --git a/src/Tools/jEdit/src/main.scala b/src/Tools/jEdit/src/main.scala
--- a/src/Tools/jEdit/src/main.scala
+++ b/src/Tools/jEdit/src/main.scala
@@ -1,146 +1,142 @@
/* Title: src/Tools/jEdit/src/main.scala
Author: Makarius
Main Isabelle application entry point.
*/
package isabelle.jedit
import isabelle._
import org.gjt.sp.jedit.{MiscUtilities, jEdit}
object Main
{
/* main entry point */
def main(args: Array[String]): Unit =
{
if (args.nonEmpty && args(0) == "-init") {
Isabelle_System.init()
}
else {
val start =
{
try {
Isabelle_System.init()
Isabelle_Fonts.init()
GUI.init_lafs()
/* ROOTS template */
{
val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
if (!roots.is_file) File.write(roots, """# Additional session root directories
#
# * each line contains one directory entry in Isabelle path notation, e.g.
#
# $ISABELLE_HOME/../AFP/thys
#
# for a copy of AFP put side-by-side to the Isabelle distribution
#
# * Isabelle/jEdit provides formal markup for C-hover-click and completion
#
# * lines starting with "#" are stripped
#
# * changes require restart of the Isabelle application
#
#:mode=text:encoding=UTF-8:
#$ISABELLE_HOME/../AFP/thys
""")
}
/* settings directory */
val settings_dir = Path.explode("$JEDIT_SETTINGS")
val properties = settings_dir + Path.explode("properties")
if (properties.is_file) {
val props1 = split_lines(File.read(properties))
val props2 = props1.filterNot(_.startsWith("plugin-blacklist.isabelle_jedit"))
if (props1 != props2) File.write(properties, cat_lines(props2))
}
Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager"))
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
"""""")
File.write(settings_dir + Path.explode("perspective.xml"),
XML.header +
"""
""")
}
- for (plugin <- List("jedit_base", "jedit_main")) {
- val dir = Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin)
- val context = isabelle.setup.Build.directory_context(dir.java_path)
- isabelle.setup.Build.build(context, false)
- }
+ Scala_Project.plugin_contexts().foreach(isabelle.setup.Build.build(_, false))
/* args */
val jedit_settings =
"-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
val jedit_server =
System.getProperty("isabelle.jedit_server") match {
case null | "" => "-noserver"
case name => "-server=" + name
}
val jedit_options =
Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
val more_args =
{
args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
case Nil | List("--") =>
args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
case List(":") => args.slice(0, args.size - 1)
case _ => args
}
}
/* environment */
for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
MiscUtilities.putenv(name, File.platform_path(Isabelle_System.getenv(name)))
}
MiscUtilities.putenv("ISABELLE_ROOT", null)
/* properties */
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME")))
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
System.setProperty("scala.color", "false")
/* main startup */
() => jEdit.main(Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
}
catch {
case exn: Throwable =>
GUI.init_laf()
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
sys.exit(2)
}
}
start()
}
}
}