tuned;
authorwenzelm
Thu Feb 27 10:58:43 2014 +0100 (2014-02-27)
changeset 5577930fb00b5a9d3
parent 55778 e1fd8780f997
child 55780 9fdd01fa48d1
tuned;
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 10:38:47 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 10:58:43 2014 +0100
     1.3 @@ -282,13 +282,16 @@
     1.4    /* reparse range of command spans */
     1.5  
     1.6    @tailrec private def chop_common(
     1.7 -      cmds: List[Command], spans: List[(List[Command.Blob], List[Token])])
     1.8 -      : (List[Command], List[(List[Command.Blob], List[Token])]) =
     1.9 -    (cmds, spans) match {
    1.10 -      case (c :: cs, (blobs, span) :: ps) if c.blobs == blobs && c.span == span =>
    1.11 -        chop_common(cs, ps)
    1.12 -      case _ => (cmds, spans)
    1.13 +      cmds: List[Command],
    1.14 +      blobs_spans: List[(List[Command.Blob], List[Token])])
    1.15 +    : (List[Command], List[(List[Command.Blob], List[Token])]) =
    1.16 +  {
    1.17 +    (cmds, blobs_spans) match {
    1.18 +      case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
    1.19 +        chop_common(cmds, rest)
    1.20 +      case _ => (cmds, blobs_spans)
    1.21      }
    1.22 +  }
    1.23  
    1.24    private def reparse_spans(
    1.25      thy_load: Thy_Load,
    1.26 @@ -299,24 +302,24 @@
    1.27      first: Command, last: Command): Linear_Set[Command] =
    1.28    {
    1.29      val cmds0 = commands.iterator(first, last).toList
    1.30 -    val spans0 =
    1.31 +    val blobs_spans0 =
    1.32        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    1.33          map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
    1.34  
    1.35 -    val (cmds1, spans1) = chop_common(cmds0, spans0)
    1.36 +    val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    1.37  
    1.38 -    val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
    1.39 +    val (rev_cmds2, rev_blobs_spans2) = chop_common(cmds1.reverse, blobs_spans1.reverse)
    1.40      val cmds2 = rev_cmds2.reverse
    1.41 -    val spans2 = rev_spans2.reverse
    1.42 +    val blobs_spans2 = rev_blobs_spans2.reverse
    1.43  
    1.44      cmds2 match {
    1.45        case Nil =>
    1.46 -        assert(spans2.isEmpty)
    1.47 +        assert(blobs_spans2.isEmpty)
    1.48          commands
    1.49        case cmd :: _ =>
    1.50          val hook = commands.prev(cmd)
    1.51          val inserted =
    1.52 -          spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
    1.53 +          blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
    1.54          (commands /: cmds2)(_ - _).append_after(hook, inserted)
    1.55      }
    1.56    }