src/Pure/PIDE/command_span.scala

tuned -- more uniform ML vs. Scala;

/*  Title:      Pure/PIDE/command_span.scala
    Author:     Makarius

Syntactic representation of command spans.
*/

package isabelle


import scala.collection.mutable


object Command_Span
{
  sealed abstract class Kind {
    override def toString: String =
      this match {
        case Command_Span(name, _) => if (name != "") name else "<command>"
        case Ignored_Span => "<ignored>"
        case Malformed_Span => "<malformed>"
      }
  }
  case class Command_Span(name: String, pos: Position.T) extends Kind
  case object Ignored_Span extends Kind
  case object Malformed_Span extends Kind

  sealed case class Span(kind: Kind, content: List[Token])
  {
    def length: Int = (0 /: content)(_ + _.source.length)

    def compact_source: (String, Span) =
    {
      val source: String =
        content match {
          case List(tok) => tok.source
          case toks => toks.map(_.source).mkString
        }

      val content1 = new mutable.ListBuffer[Token]
      var i = 0
      for (Token(kind, s) <- content) {
        val n = s.length
        val s1 = source.substring(i, i + n)
        content1 += Token(kind, s1)
        i += n
      }
      (source, Span(kind, content1.toList))
    }
  }

  val empty: Span = Span(Ignored_Span, Nil)

  def unparsed(source: String): Span =
    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))


  /* resolve inlined 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 == "%" || t1.source == "--")) 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)] =
    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(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)
        }
      case _ => (Nil, -1)
    }

  def resolve_files(
      resources: Resources,
      syntax: Prover.Syntax,
      node_name: Document.Node.Name,
      span: Span,
      get_blob: Document.Node.Name => Option[Document.Blob])
    : List[Command.Blob] =
  {
    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)))
        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
        (name, blob)
      })
  }
}