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