# HG changeset patch # User wenzelm # Date 1756982300 -7200 # Node ID c2305d9cca09c6191301bd64d9d94b3ee79c6d3d # Parent 5e8fd30caf43f23dcb6be9269ed7e567394336b5 less verbose by default; diff -r 5e8fd30caf43 -r c2305d9cca09 src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy Thu Sep 04 12:23:18 2025 +0200 +++ b/src/Doc/System/Scala.thy Thu Sep 04 12:38:20 2025 +0200 @@ -259,6 +259,7 @@ -L make symlinks to original source files -M use Maven as build tool -f force update of existing directory + -v verbose Setup project for Isabelle/Scala/jEdit --- to support common IDEs such as IntelliJ IDEA. Either option -G or -M is mandatory to specify the @@ -291,6 +292,9 @@ \<^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. + + \<^medskip> + Option \<^verbatim>\-v\ enables verbose mode. \ diff -r 5e8fd30caf43 -r c2305d9cca09 src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala Thu Sep 04 12:23:18 2025 +0200 +++ b/src/Pure/Tools/scala_project.scala Thu Sep 04 12:38:20 2025 +0200 @@ -242,7 +242,7 @@ val dir = build_tool.package_dir(source) val target_dir = project_dir + dir if (!target_dir.is_dir) { - progress.echo(" Creating package directory: " + dir) + progress.echo(" Creating package directory: " + dir, verbose = true) Isabelle_System.make_directory(target_dir) } if (symlinks) Isabelle_System.symlink(source.absolute, target_dir, native = true) @@ -261,6 +261,7 @@ var project_dir = default_project_dir var symlinks = false var force = false + var verbose = false val getopts = Getopts(""" Usage: isabelle scala_project [OPTIONS] [MORE_SOURCES ...] @@ -271,6 +272,7 @@ -L make symlinks to original source files -M use Maven as build tool -f force update of existing directory + -v verbose Setup project for Isabelle/Scala/jEdit --- to support common IDEs such as IntelliJ IDEA. Either option -G or -M is mandatory to specify the @@ -280,12 +282,13 @@ "G" -> (_ => build_tool = Some(Gradle)), "L" -> (_ => symlinks = true), "M" -> (_ => build_tool = Some(Maven)), - "f" -> (_ => force = true)) + "f" -> (_ => force = true), + "v" -> (_ => verbose = true)) val more_args = getopts(args) val more_sources = more_args.map(Path.explode) - val progress = new Console_Progress + val progress = new Console_Progress(verbose = verbose) if (build_tool.isEmpty) { error("Unspecified build tool: need to provide option -G or -M")