wenzelm@57905: /*  Title:      Pure/PIDE/command_span.scala
wenzelm@57905:     Author:     Makarius
wenzelm@57905: 
wenzelm@57905: Syntactic representation of command spans.
wenzelm@57905: */
wenzelm@57905: 
wenzelm@57905: package isabelle
wenzelm@57905: 
wenzelm@57905: 
wenzelm@57905: import scala.collection.mutable
wenzelm@57905: 
wenzelm@57905: 
wenzelm@57905: object Command_Span
wenzelm@57905: {
wenzelm@57905:   sealed abstract class Kind {
wenzelm@57905:     override def toString: String =
wenzelm@57905:       this match {
wenzelm@57910:         case Command_Span(name, _) => if (name != "") name else "<command>"
wenzelm@57905:         case Ignored_Span => "<ignored>"
wenzelm@57905:         case Malformed_Span => "<malformed>"
wenzelm@57905:       }
wenzelm@57905:   }
wenzelm@57910:   case class Command_Span(name: String, pos: Position.T) extends Kind
wenzelm@57905:   case object Ignored_Span extends Kind
wenzelm@57905:   case object Malformed_Span extends Kind
wenzelm@57905: 
wenzelm@57905:   sealed case class Span(kind: Kind, content: List[Token])
wenzelm@57905:   {
wenzelm@57905:     def compact_source: (String, Span) =
wenzelm@57905:     {
wenzelm@57905:       val source: String =
wenzelm@57905:         content match {
wenzelm@57905:           case List(tok) => tok.source
wenzelm@57905:           case toks => toks.map(_.source).mkString
wenzelm@57905:         }
wenzelm@57905: 
wenzelm@57905:       val content1 = new mutable.ListBuffer[Token]
wenzelm@57905:       var i = 0
wenzelm@57905:       for (Token(kind, s) <- content) {
wenzelm@57905:         val n = s.length
wenzelm@57905:         val s1 = source.substring(i, i + n)
wenzelm@57905:         content1 += Token(kind, s1)
wenzelm@57905:         i += n
wenzelm@57905:       }
wenzelm@57905:       (source, Span(kind, content1.toList))
wenzelm@57905:     }
wenzelm@57905:   }
wenzelm@57905: 
wenzelm@57905:   val empty: Span = Span(Ignored_Span, Nil)
wenzelm@57905: 
wenzelm@57905:   def unparsed(source: String): Span =
wenzelm@57905:     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@57905: 
wenzelm@57905: 
wenzelm@57905:   /* resolve inlined files */
wenzelm@57905: 
wenzelm@57905:   private def find_file(tokens: List[Token]): Option[String] =
wenzelm@57905:   {
wenzelm@57905:     def clean(toks: List[Token]): List[Token] =
wenzelm@57905:       toks match {
wenzelm@57905:         case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
wenzelm@57905:         case t :: ts => t :: clean(ts)
wenzelm@57905:         case Nil => Nil
wenzelm@57905:       }
wenzelm@57905:     clean(tokens.filter(_.is_proper)) match {
wenzelm@57905:       case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
wenzelm@57905:       case _ => None
wenzelm@57905:     }
wenzelm@57905:   }
wenzelm@57905: 
wenzelm@57905:   def span_files(syntax: Prover.Syntax, span: Span): List[String] =
wenzelm@57905:     span.kind match {
wenzelm@57910:       case Command_Span(name, _) =>
wenzelm@57905:         syntax.load_command(name) match {
wenzelm@57905:           case Some(exts) =>
wenzelm@57905:             find_file(span.content) match {
wenzelm@57905:               case Some(file) =>
wenzelm@57905:                 if (exts.isEmpty) List(file)
wenzelm@57905:                 else exts.map(ext => file + "." + ext)
wenzelm@57905:               case None => Nil
wenzelm@57905:             }
wenzelm@57905:           case None => Nil
wenzelm@57905:         }
wenzelm@57905:       case _ => Nil
wenzelm@57905:     }
wenzelm@57905: 
wenzelm@57905:   def resolve_files(
wenzelm@57905:       resources: Resources,
wenzelm@57905:       syntax: Prover.Syntax,
wenzelm@57905:       node_name: Document.Node.Name,
wenzelm@57905:       span: Span,
wenzelm@57905:       get_blob: Document.Node.Name => Option[Document.Blob])
wenzelm@57905:     : List[Command.Blob] =
wenzelm@57905:   {
wenzelm@57905:     span_files(syntax, span).map(file_name =>
wenzelm@57905:       Exn.capture {
wenzelm@57905:         val name =
wenzelm@57905:           Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
wenzelm@57905:         val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
wenzelm@57905:         (name, blob)
wenzelm@57905:       })
wenzelm@57905:   }
wenzelm@57905: }
wenzelm@57905: