src/Pure/Thy/thy_syntax.scala
changeset 57905 c0c5652e796e
parent 57904 922273b7bf8a
child 57906 020df63dd0a9
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
     1.3 @@ -13,84 +13,6 @@
     1.4  
     1.5  object Thy_Syntax
     1.6  {
     1.7 -  /** spans **/
     1.8 -
     1.9 -  sealed abstract class Span_Kind {
    1.10 -    override def toString: String =
    1.11 -      this match {
    1.12 -        case Command_Span(name) => if (name != "") name else "<command>"
    1.13 -        case Ignored_Span => "<ignored>"
    1.14 -        case Malformed_Span => "<malformed>"
    1.15 -      }
    1.16 -  }
    1.17 -  case class Command_Span(name: String) extends Span_Kind
    1.18 -  case object Ignored_Span extends Span_Kind
    1.19 -  case object Malformed_Span extends Span_Kind
    1.20 -
    1.21 -  sealed case class Span(kind: Span_Kind, content: List[Token])
    1.22 -  {
    1.23 -    def compact_source: (String, Span) =
    1.24 -    {
    1.25 -      val source: String =
    1.26 -        content match {
    1.27 -          case List(tok) => tok.source
    1.28 -          case toks => toks.map(_.source).mkString
    1.29 -        }
    1.30 -
    1.31 -      val content1 = new mutable.ListBuffer[Token]
    1.32 -      var i = 0
    1.33 -      for (Token(kind, s) <- content) {
    1.34 -        val n = s.length
    1.35 -        val s1 = source.substring(i, i + n)
    1.36 -        content1 += Token(kind, s1)
    1.37 -        i += n
    1.38 -      }
    1.39 -      (source, Span(kind, content1.toList))
    1.40 -    }
    1.41 -  }
    1.42 -
    1.43 -  val empty_span: Span = Span(Ignored_Span, Nil)
    1.44 -
    1.45 -  def unparsed_span(source: String): Span =
    1.46 -    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
    1.47 -
    1.48 -
    1.49 -  /* parse */
    1.50 -
    1.51 -  def parse_spans(toks: List[Token]): List[Span] =
    1.52 -  {
    1.53 -    val result = new mutable.ListBuffer[Span]
    1.54 -    val content = new mutable.ListBuffer[Token]
    1.55 -    val improper = new mutable.ListBuffer[Token]
    1.56 -
    1.57 -    def ship(span: List[Token])
    1.58 -    {
    1.59 -      val kind =
    1.60 -        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
    1.61 -          Command_Span(span.head.source)
    1.62 -        else if (span.forall(_.is_improper)) Ignored_Span
    1.63 -        else Malformed_Span
    1.64 -      result += Span(kind, span)
    1.65 -    }
    1.66 -
    1.67 -    def flush()
    1.68 -    {
    1.69 -      if (!content.isEmpty) { ship(content.toList); content.clear }
    1.70 -      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
    1.71 -    }
    1.72 -
    1.73 -    for (tok <- toks) {
    1.74 -      if (tok.is_command) { flush(); content += tok }
    1.75 -      else if (tok.is_improper) improper += tok
    1.76 -      else { content ++= improper; improper.clear; content += tok }
    1.77 -    }
    1.78 -    flush()
    1.79 -
    1.80 -    result.toList
    1.81 -  }
    1.82 -
    1.83 -
    1.84 -
    1.85    /** perspective **/
    1.86  
    1.87    def command_perspective(
    1.88 @@ -222,62 +144,12 @@
    1.89    }
    1.90  
    1.91  
    1.92 -  /* inlined files */
    1.93 -
    1.94 -  private def find_file(tokens: List[Token]): Option[String] =
    1.95 -  {
    1.96 -    def clean(toks: List[Token]): List[Token] =
    1.97 -      toks match {
    1.98 -        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    1.99 -        case t :: ts => t :: clean(ts)
   1.100 -        case Nil => Nil
   1.101 -      }
   1.102 -    clean(tokens.filter(_.is_proper)) match {
   1.103 -      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
   1.104 -      case _ => None
   1.105 -    }
   1.106 -  }
   1.107 -
   1.108 -  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
   1.109 -    span.kind match {
   1.110 -      case Command_Span(name) =>
   1.111 -        syntax.load_command(name) match {
   1.112 -          case Some(exts) =>
   1.113 -            find_file(span.content) match {
   1.114 -              case Some(file) =>
   1.115 -                if (exts.isEmpty) List(file)
   1.116 -                else exts.map(ext => file + "." + ext)
   1.117 -              case None => Nil
   1.118 -            }
   1.119 -          case None => Nil
   1.120 -        }
   1.121 -      case _ => Nil
   1.122 -    }
   1.123 -
   1.124 -  def resolve_files(
   1.125 -      resources: Resources,
   1.126 -      syntax: Prover.Syntax,
   1.127 -      node_name: Document.Node.Name,
   1.128 -      span: Span,
   1.129 -      get_blob: Document.Node.Name => Option[Document.Blob])
   1.130 -    : List[Command.Blob] =
   1.131 -  {
   1.132 -    span_files(syntax, span).map(file_name =>
   1.133 -      Exn.capture {
   1.134 -        val name =
   1.135 -          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
   1.136 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
   1.137 -        (name, blob)
   1.138 -      })
   1.139 -  }
   1.140 -
   1.141 -
   1.142    /* reparse range of command spans */
   1.143  
   1.144    @tailrec private def chop_common(
   1.145        cmds: List[Command],
   1.146 -      blobs_spans: List[(List[Command.Blob], Span)])
   1.147 -    : (List[Command], List[(List[Command.Blob], Span)]) =
   1.148 +      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
   1.149 +    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
   1.150    {
   1.151      (cmds, blobs_spans) match {
   1.152        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
   1.153 @@ -296,8 +168,8 @@
   1.154    {
   1.155      val cmds0 = commands.iterator(first, last).toList
   1.156      val blobs_spans0 =
   1.157 -      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
   1.158 -        map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
   1.159 +      syntax.parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
   1.160 +        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
   1.161  
   1.162      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
   1.163