src/Pure/PIDE/command_span.scala
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 58802 3cc68ec558b0
child 59683 d6824d8490be
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/PIDE/command_span.scala
     2     Author:     Makarius
     3 
     4 Syntactic representation of command spans.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 
    12 
    13 object Command_Span
    14 {
    15   sealed abstract class Kind {
    16     override def toString: String =
    17       this match {
    18         case Command_Span(name, _) => if (name != "") name else "<command>"
    19         case Ignored_Span => "<ignored>"
    20         case Malformed_Span => "<malformed>"
    21       }
    22   }
    23   case class Command_Span(name: String, pos: Position.T) extends Kind
    24   case object Ignored_Span extends Kind
    25   case object Malformed_Span extends Kind
    26 
    27   sealed case class Span(kind: Kind, content: List[Token])
    28   {
    29     def length: Int = (0 /: content)(_ + _.source.length)
    30 
    31     def compact_source: (String, Span) =
    32     {
    33       val source: String =
    34         content match {
    35           case List(tok) => tok.source
    36           case toks => toks.map(_.source).mkString
    37         }
    38 
    39       val content1 = new mutable.ListBuffer[Token]
    40       var i = 0
    41       for (Token(kind, s) <- content) {
    42         val n = s.length
    43         val s1 = source.substring(i, i + n)
    44         content1 += Token(kind, s1)
    45         i += n
    46       }
    47       (source, Span(kind, content1.toList))
    48     }
    49   }
    50 
    51   val empty: Span = Span(Ignored_Span, Nil)
    52 
    53   def unparsed(source: String): Span =
    54     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
    55 
    56 
    57   /* resolve inlined files */
    58 
    59   private def find_file(tokens: List[Token]): Option[String] =
    60   {
    61     def clean(toks: List[Token]): List[Token] =
    62       toks match {
    63         case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    64         case t :: ts => t :: clean(ts)
    65         case Nil => Nil
    66       }
    67     clean(tokens.filter(_.is_proper)) match {
    68       case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
    69       case _ => None
    70     }
    71   }
    72 
    73   def span_files(syntax: Prover.Syntax, span: Span): List[String] =
    74     span.kind match {
    75       case Command_Span(name, _) =>
    76         syntax.load_command(name) match {
    77           case Some(exts) =>
    78             find_file(span.content) match {
    79               case Some(file) =>
    80                 if (exts.isEmpty) List(file)
    81                 else exts.map(ext => file + "." + ext)
    82               case None => Nil
    83             }
    84           case None => Nil
    85         }
    86       case _ => Nil
    87     }
    88 
    89   def resolve_files(
    90       resources: Resources,
    91       syntax: Prover.Syntax,
    92       node_name: Document.Node.Name,
    93       span: Span,
    94       get_blob: Document.Node.Name => Option[Document.Blob])
    95     : List[Command.Blob] =
    96   {
    97     span_files(syntax, span).map(file_name =>
    98       Exn.capture {
    99         val name =
   100           Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
   101         val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
   102         (name, blob)
   103       })
   104   }
   105 }
   106