# HG changeset patch
# User wenzelm
# Date 1576935787 -3600
# Node ID 836fde6f9d7e081cc1c01145401df9cc4461e0f5
# Parent  2217c731d228f93d3dc69c344147c8e355608c59
proper search with multiple "pages" of results;

diff -r 2217c731d228 -r 836fde6f9d7e src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Dec 20 15:24:34 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Sat Dec 21 14:43:07 2019 +0100
@@ -11,6 +11,7 @@
 package isabelle
 
 
+import scala.collection.mutable
 import scala.util.matching.Regex
 
 
@@ -921,6 +922,22 @@
     def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
       API.make_result(execute_raw(method, params = params))
 
+    def execute_search[A](
+      method: String, params: JSON.Object.T, unapply: JSON.T => Option[A]): List[A] =
+    {
+      val results = new mutable.ListBuffer[A]
+      var after = ""
+
+      do {
+        val result =
+          execute(method, params = params ++ JSON.optional("after" -> proper_string(after)))
+        results ++= result.get_value(JSON.list(_, "data", unapply))
+        after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after")))
+      } while (after.nonEmpty)
+
+      results.toList
+    }
+
 
     /* concrete methods */
 
@@ -938,29 +955,30 @@
           if value.nonEmpty
         } yield (key, List(value))).toMap
 
-      execute("diffusion.repository.search",
-          JSON.Object("queryKey" -> "active", "constraints" -> constraints))
-        .get_value(JSON.list(_, "data", data => JSON.value(data, "fields", fields =>
-          for {
-            vcs_name <- JSON.string(fields, "vcs")
-            id <- JSON.long(data, "id")
-            phid <- JSON.string(data, "phid")
-            name <- JSON.string(fields, "name")
-            callsign <- JSON.string0(fields, "callsign")
-            short_name <- JSON.string0(fields, "shortName")
-            importing <- JSON.bool(fields, "isImporting")
-          }
-          yield {
-            val vcs = API.VCS.read(vcs_name)
-            val url_path = if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name
-            val ssh_url =
-              vcs match {
-                case API.VCS.hg => hg_url + url_path
-                case API.VCS.git => hg_url + url_path + ".git"
-                case API.VCS.svn => ""
+      execute_search("diffusion.repository.search",
+          JSON.Object("queryKey" -> "active", "constraints" -> constraints),
+            data => JSON.value(data, "fields", fields =>
+              for {
+                vcs_name <- JSON.string(fields, "vcs")
+                id <- JSON.long(data, "id")
+                phid <- JSON.string(data, "phid")
+                name <- JSON.string(fields, "name")
+                callsign <- JSON.string0(fields, "callsign")
+                short_name <- JSON.string0(fields, "shortName")
+                importing <- JSON.bool(fields, "isImporting")
               }
-            API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url)
-          })))
+              yield {
+                val vcs = API.VCS.read(vcs_name)
+                val url_path =
+                  if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name
+                val ssh_url =
+                  vcs match {
+                    case API.VCS.hg => hg_url + url_path
+                    case API.VCS.git => hg_url + url_path + ".git"
+                    case API.VCS.svn => ""
+                  }
+                API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url)
+              }))
     }
 
     def the_repository(phid: String): API.Repository =