# HG changeset patch
# User wenzelm
# Date 1606575226 -3600
# Node ID 38e05b7ded612b87159862616664dfa11e4db2fc
# Parent  72ac27ea12b247e5dd7465c33e3c4745ecaf71e5
tuned signature --- more explicit types;

diff -r 72ac27ea12b2 -r 38e05b7ded61 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Nov 28 15:17:14 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Nov 28 15:53:46 2020 +0100
@@ -442,16 +442,16 @@
 
       // auxiliary files
       case _ =>
-        val (files, index) = span.loaded_files(syntax)
+        val loaded_files = span.loaded_files(syntax)
         val blobs =
-          files.map(file =>
+          loaded_files.files.map(file =>
             (Exn.capture {
               val src_path = Path.explode(file)
               val name = Document.Node.Name(resources.append(node_name, src_path))
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               Blob(name, src_path, content)
             }).user_error)
-        (blobs, index)
+        (blobs, loaded_files.index)
     }
   }
 }
diff -r 72ac27ea12b2 -r 38e05b7ded61 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Sat Nov 28 15:17:14 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Sat Nov 28 15:53:46 2020 +0100
@@ -14,9 +14,11 @@
 {
   /* loaded files */
 
-  type Loaded_Files = (List[String], Int)
-
-  val no_loaded_files: Loaded_Files = (Nil, -1)
+  object Loaded_Files
+  {
+    val none: Loaded_Files = Loaded_Files(Nil, -1)
+  }
+  sealed case class Loaded_Files(files: List[String], index: Int)
 
   class Load_Command(val name: String) extends Isabelle_System.Service
   {
@@ -28,10 +30,10 @@
       tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match {
         case Some((file, i)) =>
           extensions match {
-            case Nil => (List(file), i)
-            case exts => (exts.map(ext => file + "." + ext), i)
+            case Nil => Loaded_Files(List(file), i)
+            case exts => Loaded_Files(exts.map(ext => file + "." + ext), i)
           }
-        case None => no_loaded_files
+        case None => Loaded_Files.none
       }
   }
 
@@ -119,7 +121,7 @@
 
     def loaded_files(syntax: Outer_Syntax): Loaded_Files =
       syntax.load_command(name) match {
-        case None => no_loaded_files
+        case None => Loaded_Files.none
         case Some(a) =>
           load_commands.find(_.name == a) match {
             case Some(load_command) => load_command.loaded_files(clean_arguments)
diff -r 72ac27ea12b2 -r 38e05b7ded61 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Nov 28 15:17:14 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Nov 28 15:53:46 2020 +0100
@@ -121,7 +121,7 @@
         val dir = Path.explode(name.master_dir)
         (for {
           span <- spans.iterator
-          file <- span.loaded_files(syntax)._1
+          file <- span.loaded_files(syntax).files
         } yield (dir + Path.explode(file)).expand).toList
       }
       else Nil