# HG changeset patch
# User wenzelm
# Date 1606482054 -3600
# Node ID bda424c5819f121b5e779df84a7fe203a7074f49
# Parent  b808eddc83cf2f9c2782bb6595fedd936a5ae78e
clarified modules;

diff -r b808eddc83cf -r bda424c5819f src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Nov 27 11:50:23 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Nov 27 14:00:54 2020 +0100
@@ -468,37 +468,6 @@
 
   /* blobs: inlined errors and auxiliary files */
 
-  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
-  {
-    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
-      toks match {
-        case (t1, i1) :: (t2, i2) :: rest =>
-          if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
-          else (t1, i1) :: clean((t2, i2) :: rest)
-        case _ => toks
-      }
-    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
-  }
-
-  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
-    if (tokens.exists({ case (t, _) => t.is_command })) {
-      tokens.dropWhile({ case (t, _) => !t.is_command }).
-        collectFirst({ case (t, i) if t.is_embedded => (t.content, i) })
-    }
-    else None
-
-  def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) =
-    syntax.load_command(span.name) match {
-      case Some(exts) =>
-        find_file(clean_tokens(span.content)) match {
-          case Some((file, i)) =>
-            if (exts.isEmpty) (List(file), i)
-            else (exts.map(ext => file + "." + ext), i)
-          case None => (Nil, -1)
-        }
-      case None => (Nil, -1)
-    }
-
   def blobs_info(
     resources: Resources,
     syntax: Outer_Syntax,
@@ -534,12 +503,12 @@
 
       // auxiliary files
       case _ =>
-        val (files, index) = span_files(syntax, span)
+        val (files, index) = span.loaded_files(syntax)
         val blobs =
           files.map(file =>
             (Exn.capture {
               val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
-              val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+              val blob = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               (name, blob)
             }).user_error)
         (blobs, index)
diff -r b808eddc83cf -r bda424c5819f src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Fri Nov 27 11:50:23 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Fri Nov 27 14:00:54 2020 +0100
@@ -67,6 +67,18 @@
       }
       (source, Span(kind, content1.toList))
     }
+
+    def loaded_files(syntax: Outer_Syntax): (List[String], Int) =
+      syntax.load_command(name) match {
+        case Some(exts) =>
+          find_file(clean_tokens(content)) match {
+            case Some((file, i)) =>
+              if (exts.isEmpty) (List(file), i)
+              else (exts.map(ext => file + "." + ext), i)
+            case None => (Nil, -1)
+          }
+        case None => (Nil, -1)
+      }
   }
 
   val empty: Span = Span(Ignored_Span, Nil)
@@ -78,6 +90,28 @@
   }
 
 
+  /* loaded files */
+
+  def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
+  {
+    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
+      toks match {
+        case (t1, i1) :: (t2, i2) :: rest =>
+          if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
+          else (t1, i1) :: clean((t2, i2) :: rest)
+        case _ => toks
+      }
+    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
+  }
+
+  def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+    if (tokens.exists({ case (t, _) => t.is_command })) {
+      tokens.dropWhile({ case (t, _) => !t.is_command }).
+        collectFirst({ case (t, i) if t.is_embedded => (t.content, i) })
+    }
+    else None
+
+
   /* XML data representation */
 
   def encode: XML.Encode.T[Span] = (span: Span) =>
diff -r b808eddc83cf -r bda424c5819f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Nov 27 11:50:23 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Nov 27 14:00:54 2020 +0100
@@ -117,8 +117,10 @@
         val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
         val spans = syntax.parse_spans(text)
         val dir = Path.explode(name.master_dir)
-        spans.iterator.flatMap(Command.span_files(syntax, _)._1).
-          map(a => (dir + Path.explode(a)).expand).toList
+        (for {
+          span <- spans.iterator
+          file <- span.loaded_files(syntax)._1
+        } yield (dir + Path.explode(file)).expand).toList
       }
       else Nil
     }