tuned -- more uniform ML vs. Scala;

--- a/src/Pure/PIDE/command_span.ML	Thu Mar 12 14:58:32 2015 +0100
+++ b/src/Pure/PIDE/command_span.ML	Thu Mar 12 16:47:47 2015 +0100
@@ -28,22 +28,20 @@
 
 local
 
-fun clean ((i1, t1) :: (i2, t2) :: toks) =
-      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
-      else (i1, t1) :: clean ((i2, t2) :: toks)
+fun clean ((t1, i1) :: (t2, i2) :: rest) =
+      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean rest
+      else (t1, i1) :: clean ((t2, i2) :: rest)
   | clean toks = toks;
 
-fun clean_tokens toks =
-  ((0 upto length toks - 1) ~~ toks)
-  |> filter (fn (_, tok) => Token.is_proper tok)
-  |> clean;
+fun clean_tokens tokens =
+  clean (filter (fn (t, _) => Token.is_proper t) (tokens ~~ (0 upto length tokens - 1)));
 
-fun find_file ((_, tok) :: toks) =
+fun find_file ((tok, _) :: toks) =
       if Token.is_command tok then
-        toks |> get_first (fn (i, tok) =>
-          if Token.is_name tok then
-            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
-              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
+        toks |> get_first (fn (t, i) =>
+          if Token.is_name t then
+            SOME ((Path.explode (Token.content_of t), Token.pos_of t), i)
+              handle ERROR msg => error (msg ^ Position.here (Token.pos_of t))
           else NONE)
       else NONE
   | find_file [] = NONE;
@@ -56,7 +54,7 @@
       if Keyword.is_theory_load keywords cmd then
         (case find_file (clean_tokens toks) of
           NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
-        | SOME (i, path) =>
+        | SOME (path, i) =>
             let
               val toks' = toks |> map_index (fn (j, tok) =>
                 if i = j then Token.put_files (read_files cmd path) tok

--- a/src/Pure/PIDE/command_span.scala	Thu Mar 12 14:58:32 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala	Thu Mar 12 16:47:47 2015 +0100
@@ -56,34 +56,41 @@
 
   /* resolve inlined files */
 
-  private def find_file(tokens: List[Token]): Option[String] =
+  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
   {
-    def clean(toks: List[Token]): List[Token] =
+    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
       toks match {
-        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
-        case t :: ts => t :: clean(ts)
-        case Nil => Nil
+        case (t1, i1) :: (t2, i2) :: rest =>
+          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+          else (t1, i1) :: clean((t2, i2) :: rest)
+        case _ => toks
       }
-    clean(tokens.filter(_.is_proper)) match {
-      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
-      case _ => None
-    }
+    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
   }
 
-  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
+  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+    tokens match {
+      case (tok, _) :: toks =>
+        if (tok.is_command)
+          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+        else None
+      case Nil => None
+    }
+
+  def span_files(syntax: Prover.Syntax, span: Span): (List[String], Int) =
     span.kind match {
       case Command_Span(name, _) =>
         syntax.load_command(name) match {
           case Some(exts) =>
-            find_file(span.content) match {
-              case Some(file) =>
-                if (exts.isEmpty) List(file)
-                else exts.map(ext => file + "." + ext)
-              case None => Nil
+            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
+          case None => (Nil, -1)
         }
-      case _ => Nil
+      case _ => (Nil, -1)
     }
 
   def resolve_files(
@@ -94,7 +101,7 @@
       get_blob: Document.Node.Name => Option[Document.Blob])
     : List[Command.Blob] =
   {
-    span_files(syntax, span).map(file_name =>
+    span_files(syntax, span)._1.map(file_name =>
       Exn.capture {
         val name =
           Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
@@ -103,4 +110,3 @@
       })
   }
 }
-

--- a/src/Pure/PIDE/resources.scala	Thu Mar 12 14:58:32 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Mar 12 16:47:47 2015 +0100
@@ -57,7 +57,7 @@
   def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
     if (syntax.load_commands_in(text)) {
       val spans = syntax.parse_spans(text)
-      spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
+      spans.iterator.map(Command_Span.span_files(syntax, _)._1).flatten.toList
     }
     else Nil