# HG changeset patch
# User desharna
# Date 1641212945 -3600
# Node ID 507203e30db4f4a1ef778aee9d46964ee7a17dc3
# Parent  3f55c5feca58bb48cef6dea884f82322e378ea96# Parent  8a378e99d9a88d248b83f72e29309b3c899b475d
merged

diff -r 3f55c5feca58 -r 507203e30db4 NEWS
--- a/NEWS	Mon Jan 03 13:28:31 2022 +0100
+++ b/NEWS	Mon Jan 03 13:29:05 2022 +0100
@@ -45,6 +45,15 @@
     in TH0 and TH1.
 
 
+*** System ***
+
+* Command-line tool "isabelle scala_project" supports Gradle as
+alternative to Maven: either option -G or -M needs to be specified
+explicitly. This increases the chances that the Java/Scala IDE project
+works properly.
+
+
+
 New in Isabelle2021-1 (December 2021)
 -------------------------------------
 
diff -r 3f55c5feca58 -r 507203e30db4 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Doc/System/Scala.thy	Mon Jan 03 13:29:05 2022 +0100
@@ -266,7 +266,7 @@
 
 text \<open>
   The @{tool_def scala_project} tool creates a project configuration for all
-  Isabelle/Scala/Java modules specified in components via
+  Isabelle/Java/Scala modules specified in components via
   \<^path>\<open>etc/build.props\<close>, together with additional source files given on
   the command-line:
 
@@ -275,22 +275,32 @@
 
   Options are:
     -D DIR       project directory (default: "$ISABELLE_HOME_USER/scala_project")
+    -G           use Gradle as build tool
     -L           make symlinks to original source files
+    -M           use Maven as build tool
     -f           force update of existing directory
 
-  Setup Maven project for Isabelle/Scala/jEdit --- to support common IDEs
-  such as IntelliJ IDEA.\<close>}
+  Setup project for Isabelle/Scala/jEdit --- to support common IDEs such
+  as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
+  build tool.\<close>}
 
-  The generated configuration is for Maven\<^footnote>\<open>\<^url>\<open>https://maven.apache.org\<close>\<close>, but
-  the main purpose is to import it into common IDEs, such as IntelliJ
-  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 generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close> or
+  Maven\<^footnote>\<open>\<^url>\<open>https://maven.apache.org\<close>\<close>, but the main purpose is to import it
+  into common IDEs like IntelliJ 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 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>-G\<close> selects Gradle and \<^verbatim>\<open>-M\<close> selects Maven as Java/Scala build
+  tool: either one needs to be specified explicitly. These tools have a
+  tendency to break down unexpectedly, so supporting both increases the
+  chances that the generated IDE project works properly.
+
+  \<^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. The default is
   to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has no permanent
diff -r 3f55c5feca58 -r 507203e30db4 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/GCD.thy	Mon Jan 03 13:29:05 2022 +0100
@@ -1637,6 +1637,26 @@
 
 end
 
+text \<open>And some consequences: cancellation modulo @{term m}\<close>
+lemma mult_mod_cancel_right:
+  fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+  assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n" 
+  shows "a mod m = b mod m"
+proof -
+  have "m dvd (a*n - b*n)" 
+    using eq mod_eq_dvd_iff by blast
+  then have "m dvd a-b"
+    by (metis \<open>coprime m n\<close> coprime_dvd_mult_left_iff left_diff_distrib')
+  then show ?thesis
+    using mod_eq_dvd_iff by blast
+qed
+
+lemma mult_mod_cancel_left:
+  fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+  assumes "(n * a) mod m = (n * b) mod m" and "coprime m n" 
+  shows "a mod m = b mod m"
+  by (metis assms mult.commute mult_mod_cancel_right)
+
 
 subsection \<open>GCD and LCM for multiplicative normalisation functions\<close>
 
diff -r 3f55c5feca58 -r 507203e30db4 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Mon Jan 03 13:29:05 2022 +0100
@@ -87,10 +87,10 @@
 lemma bij_prod_decode: "bij prod_decode"
   by (rule bijI [OF inj_prod_decode surj_prod_decode])
 
-lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
+lemma prod_encode_eq [simp]: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
   by (rule inj_prod_encode [THEN inj_eq])
 
-lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
+lemma prod_decode_eq [simp]: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
   by (rule inj_prod_decode [THEN inj_eq])
 
 
diff -r 3f55c5feca58 -r 507203e30db4 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/List.thy	Mon Jan 03 13:29:05 2022 +0100
@@ -1244,6 +1244,9 @@
 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
 by(rule rev_cases[of xs]) auto
 
+lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)"
+by (induct xs rule: rev_induct) auto
+
 
 subsubsection \<open>\<^const>\<open>set\<close>\<close>
 
diff -r 3f55c5feca58 -r 507203e30db4 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Jan 03 13:29:05 2022 +0100
@@ -22,6 +22,9 @@
 lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))"
   by (auto simp: card_Suc_eq numeral_eq_Suc)
 
+lemma card_3_iff: "card S = 3 \<longleftrightarrow> (\<exists>x y z. S = {x,y,z} \<and> x \<noteq> y \<and> y \<noteq> z \<and> x \<noteq> z)"
+  by (fastforce simp: card_Suc_eq numeral_eq_Suc)
+
 context ord
 begin
 
diff -r 3f55c5feca58 -r 507203e30db4 src/Pure/General/json_api.scala
--- a/src/Pure/General/json_api.scala	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/General/json_api.scala	Mon Jan 03 13:29:05 2022 +0100
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import java.net.URL
+
 
 object JSON_API
 {
@@ -14,11 +16,25 @@
   def api_error(msg: String): Nothing = error("JSON API error: " + msg)
   def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n  "))
 
+  class Service(val url: URL)
+  {
+    override def toString: String = url.toString
+
+    def get(route: String): HTTP.Content =
+      HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
+
+    def get_root(route: String = ""): Root =
+      Root(get(if (route.isEmpty) "" else "/" + route).json)
+  }
+
   sealed case class Root(json: JSON.T)
   {
     def get_links: Option[Links] = JSON.value(json, "links").map(Links)
+    def get_next: Option[Service] = get_links.flatMap(_.get_next)
+
     def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
     def get_data: Option[Data] = JSON.value(json, "data").map(Data(_, get_included))
+
     def get_errors: Option[List[JSON.T]] = JSON.list(json, "errors", Some(_))
 
     def ok: Boolean = get_errors.isEmpty
@@ -29,14 +45,38 @@
         case Some(errs) => api_errors(errs.map(JSON.Format.apply))
       }
     def check_data: Data = check.get_data getOrElse api_error("missing data")
+    def check_resource: Resource = check_data.resource
+    def check_resources: List[Resource] = check_data.resources
+
+    def iterator: Iterator[Root] =
+    {
+      val init = Some(this)
+      new Iterator[Root] {
+        private var state: Option[Root] = init
+        def hasNext: Boolean = state.nonEmpty
+        def next(): Root =
+          state match {
+            case None => Iterator.empty.next()
+            case Some(res) =>
+              state = res.get_next.map(_.get_root())
+              res
+          }
+      }
+    }
+    def iterator_data: Iterator[Data] = iterator.map(_.check_data)
+    def iterator_resource: Iterator[Resource] = iterator.map(_.check_resource)
+    def iterator_resources: Iterator[Resource] = iterator.flatMap(_.check_resources)
 
     override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
   }
 
   sealed case class Links(json: JSON.T)
   {
-    def get_next: Option[Root] =
-      for (next <- JSON.value(json, "next") if next != null) yield Root(next)
+    def get_next: Option[Service] =
+      for {
+        JSON.Value.String(next) <- JSON.value(json, "next")
+        if Url.is_wellformed(next)
+      } yield new Service(Url(next))
 
     override def toString: String =
       if (get_next.isEmpty) "Links()" else "Links(next)"
diff -r 3f55c5feca58 -r 507203e30db4 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jan 03 13:29:05 2022 +0100
@@ -162,7 +162,9 @@
     (Restricted_Parser (fn restricted =>
       Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
 
-val local_theory' = local_theory_command Toplevel.local_theory';
+val local_theory' =
+  local_theory_command
+    (fn a => fn b => fn c => Toplevel.local_theory' a b c Toplevel.no_presentation);
 val local_theory = local_theory_command Toplevel.local_theory;
 val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
 val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
diff -r 3f55c5feca58 -r 507203e30db4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Jan 03 13:29:05 2022 +0100
@@ -32,6 +32,8 @@
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
   type presentation = state -> Latex.text option
+  val presentation: (state -> Latex.text) -> presentation
+  val no_presentation: presentation
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -55,14 +57,14 @@
   val ignored: Position.T -> transition
   val malformed: Position.T -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
-  val theory': (bool -> theory -> theory) -> transition -> transition
+  val theory': (bool -> theory -> theory) -> presentation -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
   val end_main_target: transition -> transition
   val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition
   val end_nested_target: transition -> transition
   val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
-    (bool -> local_theory -> local_theory) -> transition -> transition
+    (bool -> local_theory -> local_theory) -> presentation -> transition -> transition
   val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
     (local_theory -> local_theory) -> transition -> transition
   val present_local_theory: (xstring * Position.T) option -> (state -> Latex.text) ->
@@ -267,8 +269,8 @@
 (* presentation *)
 
 type presentation = state -> Latex.text option;
+fun presentation g : presentation = SOME o g;
 val no_presentation: presentation = K NONE;
-fun presentation g : presentation = SOME o g;
 
 
 (* primitive transitions *)
@@ -452,7 +454,7 @@
   (fn Theory gthy => node_presentation (Theory (f gthy))
     | _ => raise UNDEF));
 
-fun theory' f = transaction (fn int =>
+fun theory' f = present_transaction (fn int =>
   (fn Theory (Context.Theory thy) =>
       let val thy' = thy
         |> Sign.new_group
@@ -461,7 +463,7 @@
       in node_presentation (Theory (Context.Theory thy')) end
     | _ => raise UNDEF));
 
-fun theory f = theory' (K f);
+fun theory f = theory' (K f) no_presentation;
 
 fun begin_main_target begin f = transaction (fn _ =>
   (fn Theory (Context.Theory thy) =>
@@ -510,10 +512,10 @@
             |> f int
             |> Local_Theory.reset_group;
         in (Theory (finish lthy'), lthy') end
-    | _ => raise UNDEF))
-  no_presentation;
+    | _ => raise UNDEF));
 
-fun local_theory restricted target f = local_theory' restricted target (K f);
+fun local_theory restricted target f =
+  local_theory' restricted target (K f) no_presentation;
 
 fun present_local_theory target g = present_transaction (fn _ =>
   (fn Theory gthy =>
diff -r 3f55c5feca58 -r 507203e30db4 src/Pure/Tools/flarum.scala
--- a/src/Pure/Tools/flarum.scala	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Tools/flarum.scala	Mon Jan 03 13:29:05 2022 +0100
@@ -13,20 +13,18 @@
 object Flarum
 {
   // see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
-  val Date_Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
+  val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
 
   def server(url: URL): Server = new Server(url)
 
-  class Server private[Flarum](url: URL)
+  class Server private[Flarum](url: URL) extends JSON_API.Service(url)
   {
-    override def toString: String = url.toString
+    def get_api(route: String): JSON_API.Root =
+      get_root("api" + (if (route.isEmpty) "" else "/" + route))
 
-    def get(route: String): HTTP.Content =
-      HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
-
-    def get_api(route: String = ""): JSON_API.Root =
-      JSON_API.Root(get("api" + (if (route.isEmpty) "" else "/" + route)).json)
-
-    val api: JSON_API.Root = get_api()
+    val root: JSON_API.Root = get_api("")
+    def users: JSON_API.Root = get_api("users")
+    def groups: JSON_API.Root = get_api("groups")
+    def discussions: JSON_API.Root = get_api("discussions")
   }
 }
diff -r 3f55c5feca58 -r 507203e30db4 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Tools/scala_project.scala	Mon Jan 03 13:29:05 2022 +0100
@@ -1,8 +1,8 @@
 /*  Title:      Pure/Tools/scala_project.scala
     Author:     Makarius
 
-Manage Isabelle/Scala/Java project sources, with output to Maven for
-IntelliJ IDEA.
+Manage Isabelle/Scala/Java project sources, with output to Gradle or
+Maven for IntelliJ IDEA.
 */
 
 package isabelle
@@ -10,17 +10,95 @@
 
 object Scala_Project
 {
-  /* Maven project */
+  /** build tools **/
 
   def java_version: String = "15"
   def scala_version: String = scala.util.Properties.versionNumberString
 
-  def maven_project(jars: List[Path]): String =
+  abstract class Build_Tool
+  {
+    def project_root: Path
+    def init_project(dir: Path, jars: List[Path]): Unit
+
+    val java_src_dir: Path = Path.explode("src/main/java")
+    val scala_src_dir: Path = Path.explode("src/main/scala")
+
+    def detect_project(dir: Path): Boolean =
+      (dir + project_root).is_file &&
+      (dir + scala_src_dir).is_dir
+
+    def package_dir(source_file: Path): Path =
+    {
+      val is_java = source_file.is_java
+      val dir =
+        package_name(source_file) match {
+          case Some(name) =>
+            if (is_java) Path.explode(space_explode('.', name).mkString("/"))
+            else Path.basic(name)
+          case None => error("Failed to guess package from " + source_file)
+        }
+      (if (is_java) java_src_dir else scala_src_dir) + dir
+    }
+  }
+
+  def build_tools: List[Build_Tool] = List(Gradle, Maven)
+
+
+  /* Gradle */
+
+  object Gradle extends Build_Tool
   {
-    def dependency(jar: Path): String =
+    override def toString: String = "Gradle"
+
+    val project_settings: Path = Path.explode("settings.gradle")
+    override val project_root: Path = Path.explode("build.gradle")
+
+    private def groovy_string(s: String): String =
+    {
+      s.map(c =>
+        c match {
+          case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c
+          case _ => c.toString
+        }).mkString("'", "", "'")
+    }
+
+    override def init_project(dir: Path, jars: List[Path]): Unit =
     {
-      val name = jar.expand.drop_ext.base.implode
-      val system_path = File.platform_path(jar.absolute)
+      File.write(dir + project_settings, "rootProject.name = 'Isabelle'\n")
+      File.write(dir + project_root,
+"""plugins {
+  id 'scala'
+}
+
+repositories {
+  mavenCentral()
+}
+
+dependencies {
+  implementation 'org.scala-lang:scala-library:""" + scala_version + """'
+  compileOnly files(
+    """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n    ", ")") +
+"""
+}
+""")
+    }
+  }
+
+
+  /* Maven */
+
+  object Maven extends Build_Tool
+  {
+    override def toString: String = "Maven"
+
+    override val project_root: Path = Path.explode("pom.xml")
+
+    override def init_project(dir: Path, jars: List[Path]): Unit =
+    {
+      def dependency(jar: Path): String =
+      {
+        val name = jar.expand.drop_ext.base.implode
+        val system_path = File.platform_path(jar.absolute)
       """  <dependency>
     <groupId>classpath</groupId>
     <artifactId>""" + XML.text(name) + """</artifactId>
@@ -28,9 +106,9 @@
     <scope>system</scope>
     <systemPath>""" + XML.text(system_path) + """</systemPath>
   </dependency>"""
-    }
+      }
 
-    """<?xml version="1.0" encoding="UTF-8"?>
+      val project = """<?xml version="1.0" encoding="UTF-8"?>
 <project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
   xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
   <modelVersion>4.0.0</modelVersion>
@@ -60,6 +138,9 @@
 
   <dependencies>""" + jars.map(dependency).mkString("\n", "\n", "\n") + """</dependencies>
 </project>"""
+
+      File.write(dir + project_root, project)
+    }
   }
 
 
@@ -148,17 +229,8 @@
     lines.collectFirst({ case Package(name) => name })
   }
 
-  def the_package_dir(source_file: Path): Path =
-  {
-    package_name(source_file) match {
-      case Some(name) =>
-        if (source_file.is_java) Path.explode(space_explode('.', name).mkString("/"))
-        else Path.basic(name)
-      case None => error("Failed to guess package from " + source_file)
-    }
-  }
-
   def scala_project(
+    build_tool: Build_Tool,
     project_dir: Path = default_project_dir,
     more_sources: List[Path] = Nil,
     symlinks: Boolean = false,
@@ -166,10 +238,7 @@
     progress: Progress = new Progress): Unit =
   {
     if (project_dir.file.exists) {
-      val detect =
-        project_dir.is_dir &&
-        (project_dir + Path.explode("pom.xml")).is_file &&
-        (project_dir + Path.explode("src/main/scala")).is_dir
+      val detect = project_dir.is_dir && build_tools.exists(_.detect_project(project_dir))
 
       if (force && detect) {
         progress.echo("Purging existing project directory: " + project_dir.absolute)
@@ -178,19 +247,19 @@
       else error("Project directory already exists: " + project_dir.absolute)
     }
 
-    progress.echo("Creating project directory: " + project_dir.absolute)
+    progress.echo("Creating " + build_tool + " project directory: " + project_dir.absolute)
     Isabelle_System.make_directory(project_dir)
 
-    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 java_src_dir = Isabelle_System.make_directory(project_dir + build_tool.java_src_dir)
+    val scala_src_dir = Isabelle_System.make_directory(project_dir + build_tool.scala_src_dir)
 
     val (jars, sources) = isabelle_files
     isabelle_scala_files
 
-    File.write(project_dir + Path.explode("pom.xml"), maven_project(jars))
+    build_tool.init_project(project_dir, jars)
 
     for (source <- sources ::: more_sources) {
-      val dir = (if (source.is_java) java_src_dir else scala_src_dir) + the_package_dir(source)
+      val dir = build_tool.package_dir(source)
       val target_dir = project_dir + dir
       if (!target_dir.is_dir) {
         progress.echo("  Creating package directory: " + dir)
@@ -205,9 +274,10 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("scala_project", "setup Maven project for Isabelle/Scala/jEdit",
+    Isabelle_Tool("scala_project", "setup IDE project for Isabelle/Java/Scala sources",
       Scala_Project.here, args =>
     {
+      var build_tool: Option[Build_Tool] = None
       var project_dir = default_project_dir
       var symlinks = false
       var force = false
@@ -217,14 +287,19 @@
 
   Options are:
     -D DIR       project directory (default: """ + default_project_dir + """)
+    -G           use Gradle as build tool
     -L           make symlinks to original source files
+    -M           use Maven as build tool
     -f           force update of existing directory
 
-  Setup Maven project for Isabelle/Scala/jEdit --- to support common IDEs
-  such as IntelliJ IDEA.
+  Setup project for Isabelle/Scala/jEdit --- to support common IDEs such
+  as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
+  build tool.
 """,
         "D:" -> (arg => project_dir = Path.explode(arg)),
+        "G" -> (_ => build_tool = Some(Gradle)),
         "L" -> (_ => symlinks = true),
+        "M" -> (_ => build_tool = Some(Maven)),
         "f" -> (_ => force = true))
 
       val more_args = getopts(args)
@@ -232,7 +307,11 @@
       val more_sources = more_args.map(Path.explode)
       val progress = new Console_Progress
 
-      scala_project(project_dir = project_dir, more_sources = more_sources,
+      if (build_tool.isEmpty) {
+        error("Unspecified build tool: need to provide option -G or -M")
+      }
+
+      scala_project(build_tool.get, project_dir = project_dir, more_sources = more_sources,
         symlinks = symlinks, force = force, progress = progress)
     })
 }