# HG changeset patch
# User wenzelm
# Date 1680942294 -7200
# Node ID 127d077cccfeee993f6bb364b93be3869c680d03
# Parent  c55c4c0c9ef945c3efcc695b3965c66dbed3fe88
clarified signature: avoid object-oriented "dispatch";

diff -r c55c4c0c9ef9 -r 127d077cccfe src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Apr 03 21:16:32 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 10:24:54 2023 +0200
@@ -300,7 +300,7 @@
       contents: List[File.Content] = Nil,
       rev: String = ""
     ): Unit = {
-      require(ssh == SSH.Local, "local repository required")
+      require(ssh.is_local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
         val context0 = context.copy(progress = new Progress)
diff -r c55c4c0c9ef9 -r 127d077cccfe src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Apr 03 21:16:32 2023 +0200
+++ b/src/Pure/General/ssh.scala	Sat Apr 08 10:24:54 2023 +0200
@@ -105,6 +105,8 @@
   ) extends System {
     ssh =>
 
+    override def is_local: Boolean = false
+
     def port_suffix: String = if (port > 0) ":" + port else ""
     def user_prefix: String = if (user.nonEmpty) user + "@" else ""
 
@@ -370,6 +372,8 @@
   /* system operations */
 
   trait System extends AutoCloseable {
+    def is_local: Boolean
+
     def close(): Unit = ()
 
     override def toString: String = "SSH.Local"
@@ -424,5 +428,7 @@
       Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY)
   }
 
-  object Local extends System
+  object Local extends System {
+    override def is_local: Boolean = true
+  }
 }