store blob content within document node: aux. files that were once open are made persistent;
authorwenzelm
Mon Mar 31 15:05:24 2014 +0200 (2014-03-31)
changeset 563358953d4cc060a
parent 56334 6b3739fee456
child 56336 60434514ec0a
store blob content within document node: aux. files that were once open are made persistent;
proper structural equality for Command.File and Symbol.Index;
src/Pure/General/symbol.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/General/symbol.scala	Mon Mar 31 12:35:39 2014 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Mon Mar 31 15:05:24 2014 +0200
     1.3 @@ -165,6 +165,13 @@
     1.4        else index(i).chr + sym - index(i).sym
     1.5      }
     1.6      def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
     1.7 +
     1.8 +    override def hashCode: Int = index.hashCode
     1.9 +    override def equals(that: Any): Boolean =
    1.10 +      that match {
    1.11 +        case other: Index => index.sameElements(other.index)
    1.12 +        case _ => false
    1.13 +      }
    1.14    }
    1.15  
    1.16  
     2.1 --- a/src/Pure/PIDE/command.scala	Mon Mar 31 12:35:39 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Mon Mar 31 15:05:24 2014 +0200
     2.3 @@ -225,6 +225,7 @@
     2.4      }
     2.5    }
     2.6  
     2.7 +  // file name and position information, *without* persistent text
     2.8    class File(val file_name: String, text: CharSequence) extends Chunk
     2.9    {
    2.10      val length = text.length
    2.11 @@ -232,6 +233,17 @@
    2.12      private val symbol_index = Symbol.Index(text)
    2.13      def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
    2.14  
    2.15 +    private val hash: Int = (file_name, length, symbol_index).hashCode
    2.16 +    override def hashCode: Int = hash
    2.17 +    override def equals(that: Any): Boolean =
    2.18 +      that match {
    2.19 +        case other: File =>
    2.20 +          hash == other.hash &&
    2.21 +          file_name == other.file_name &&
    2.22 +          length == other.length &&
    2.23 +          symbol_index == other.symbol_index
    2.24 +        case _ => false
    2.25 +      }
    2.26      override def toString: String = "Command.File(" + file_name + ")"
    2.27    }
    2.28  
     3.1 --- a/src/Pure/PIDE/document.scala	Mon Mar 31 12:35:39 2014 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Mon Mar 31 15:05:24 2014 +0200
     3.3 @@ -46,20 +46,25 @@
     3.4    /* document blobs: auxiliary files */
     3.5  
     3.6    sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
     3.7 +  {
     3.8 +    def unchanged: Blob = copy(changed = false)
     3.9 +  }
    3.10  
    3.11    object Blobs
    3.12    {
    3.13 -    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
    3.14 +    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs, Nodes.empty)
    3.15      val empty: Blobs = apply(Map.empty)
    3.16    }
    3.17  
    3.18 -  final class Blobs private(blobs: Map[Node.Name, Blob])
    3.19 +  final class Blobs private(blobs: Map[Node.Name, Blob], default_nodes: Nodes)
    3.20    {
    3.21      private lazy val digests: Map[SHA1.Digest, Blob] =
    3.22        for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
    3.23  
    3.24      def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
    3.25 -    def get(name: Node.Name): Option[Blob] = blobs.get(name)
    3.26 +
    3.27 +    def get(name: Node.Name): Option[Blob] =
    3.28 +      blobs.get(name) orElse default_nodes(name).get_blob
    3.29  
    3.30      def changed(name: Node.Name): Boolean =
    3.31        get(name) match {
    3.32 @@ -67,6 +72,8 @@
    3.33          case None => false
    3.34        }
    3.35  
    3.36 +    def default(nodes: Nodes): Blobs = new Blobs(blobs, nodes)
    3.37 +
    3.38      override def toString: String = blobs.mkString("Blobs(", ",", ")")
    3.39    }
    3.40  
    3.41 @@ -157,7 +164,7 @@
    3.42        }
    3.43      }
    3.44      case class Clear[A, B]() extends Edit[A, B]
    3.45 -    case class Blob[A, B]() extends Edit[A, B]
    3.46 +    case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
    3.47  
    3.48      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    3.49      case class Deps[A, B](header: Header) extends Edit[A, B]
    3.50 @@ -222,7 +229,7 @@
    3.51    }
    3.52  
    3.53    final class Node private(
    3.54 -    val is_blob: Boolean = false,
    3.55 +    val get_blob: Option[Document.Blob] = None,
    3.56      val header: Node.Header = Node.bad_header("Bad theory header"),
    3.57      val perspective: Node.Perspective_Command =
    3.58        Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    3.59 @@ -230,13 +237,13 @@
    3.60    {
    3.61      def clear: Node = new Node(header = header)
    3.62  
    3.63 -    def init_blob: Node = new Node(is_blob = true)
    3.64 +    def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
    3.65  
    3.66      def update_header(new_header: Node.Header): Node =
    3.67 -      new Node(is_blob, new_header, perspective, _commands)
    3.68 +      new Node(get_blob, new_header, perspective, _commands)
    3.69  
    3.70      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    3.71 -      new Node(is_blob, header, new_perspective, _commands)
    3.72 +      new Node(get_blob, header, new_perspective, _commands)
    3.73  
    3.74      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    3.75        perspective.required == other_perspective.required &&
    3.76 @@ -248,7 +255,7 @@
    3.77  
    3.78      def update_commands(new_commands: Linear_Set[Command]): Node =
    3.79        if (new_commands eq _commands.commands) this
    3.80 -      else new Node(is_blob, header, perspective, Node.Commands(new_commands))
    3.81 +      else new Node(get_blob, header, perspective, Node.Commands(new_commands))
    3.82  
    3.83      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    3.84        _commands.range(i)
     4.1 --- a/src/Pure/PIDE/protocol.scala	Mon Mar 31 12:35:39 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Mar 31 15:05:24 2014 +0200
     4.3 @@ -319,9 +319,8 @@
     4.4  {
     4.5    /* inlined files */
     4.6  
     4.7 -  def define_blob(blob: Document.Blob): Unit =
     4.8 -    protocol_command_raw(
     4.9 -      "Document.define_blob", Bytes(blob.bytes.sha1_digest.toString), blob.bytes)
    4.10 +  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
    4.11 +    protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes)
    4.12  
    4.13  
    4.14    /* commands */
     5.1 --- a/src/Pure/PIDE/session.scala	Mon Mar 31 12:35:39 2014 +0200
     5.2 +++ b/src/Pure/PIDE/session.scala	Mon Mar 31 15:05:24 2014 +0200
     5.3 @@ -384,7 +384,7 @@
     5.4            change.doc_blobs.get(digest) match {
     5.5              case Some(blob) =>
     5.6                global_state >> (_.define_blob(digest))
     5.7 -              prover.get.define_blob(blob)
     5.8 +              prover.get.define_blob(digest, blob.bytes)
     5.9              case None =>
    5.10                System.err.println("Missing blob for SHA1 digest " + digest)
    5.11            }
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Mar 31 12:35:39 2014 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Mar 31 15:05:24 2014 +0200
     6.3 @@ -262,14 +262,14 @@
     6.4        syntax: Outer_Syntax,
     6.5        node_name: Document.Node.Name,
     6.6        span: List[Token],
     6.7 -      doc_blobs: Document.Blobs)
     6.8 +      doc_blobs_default: Document.Blobs)
     6.9      : List[Command.Blob] =
    6.10    {
    6.11      span_files(syntax, span).map(file_name =>
    6.12        Exn.capture {
    6.13          val name =
    6.14            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
    6.15 -        val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
    6.16 +        val blob = doc_blobs_default.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
    6.17          (name, blob)
    6.18        })
    6.19    }
    6.20 @@ -292,7 +292,7 @@
    6.21    private def reparse_spans(
    6.22      resources: Resources,
    6.23      syntax: Outer_Syntax,
    6.24 -    doc_blobs: Document.Blobs,
    6.25 +    doc_blobs_default: Document.Blobs,
    6.26      name: Document.Node.Name,
    6.27      commands: Linear_Set[Command],
    6.28      first: Command, last: Command): Linear_Set[Command] =
    6.29 @@ -300,7 +300,7 @@
    6.30      val cmds0 = commands.iterator(first, last).toList
    6.31      val blobs_spans0 =
    6.32        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    6.33 -        map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span))
    6.34 +        map(span => (resolve_files(resources, syntax, name, span, doc_blobs_default), span))
    6.35  
    6.36      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    6.37  
    6.38 @@ -327,7 +327,7 @@
    6.39    private def recover_spans(
    6.40      resources: Resources,
    6.41      syntax: Outer_Syntax,
    6.42 -    doc_blobs: Document.Blobs,
    6.43 +    doc_blobs_default: Document.Blobs,
    6.44      name: Document.Node.Name,
    6.45      perspective: Command.Perspective,
    6.46      commands: Linear_Set[Command]): Linear_Set[Command] =
    6.47 @@ -343,7 +343,7 @@
    6.48          case Some(first_unparsed) =>
    6.49            val first = next_invisible_command(cmds.reverse, first_unparsed)
    6.50            val last = next_invisible_command(cmds, first_unparsed)
    6.51 -          recover(reparse_spans(resources, syntax, doc_blobs, name, cmds, first, last))
    6.52 +          recover(reparse_spans(resources, syntax, doc_blobs_default, name, cmds, first, last))
    6.53          case None => cmds
    6.54        }
    6.55      recover(commands)
    6.56 @@ -355,7 +355,7 @@
    6.57    private def consolidate_spans(
    6.58      resources: Resources,
    6.59      syntax: Outer_Syntax,
    6.60 -    doc_blobs: Document.Blobs,
    6.61 +    doc_blobs_default: Document.Blobs,
    6.62      reparse_limit: Int,
    6.63      name: Document.Node.Name,
    6.64      perspective: Command.Perspective,
    6.65 @@ -375,7 +375,8 @@
    6.66                  last = it.next
    6.67                  i += last.length
    6.68                }
    6.69 -              reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last)
    6.70 +              reparse_spans(
    6.71 +                resources, syntax, doc_blobs_default, name, commands, first_unfinished, last)
    6.72              case None => commands
    6.73            }
    6.74          case None => commands
    6.75 @@ -399,24 +400,25 @@
    6.76    private def text_edit(
    6.77      resources: Resources,
    6.78      syntax: Outer_Syntax,
    6.79 -    doc_blobs: Document.Blobs,
    6.80 +    doc_blobs_default: Document.Blobs,
    6.81      reparse_limit: Int,
    6.82      node: Document.Node, edit: Document.Edit_Text): Document.Node =
    6.83    {
    6.84      edit match {
    6.85        case (_, Document.Node.Clear()) => node.clear
    6.86  
    6.87 -      case (_, Document.Node.Blob()) => node.init_blob
    6.88 +      case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
    6.89  
    6.90        case (name, Document.Node.Edits(text_edits)) =>
    6.91 -        if (node.is_blob) node
    6.92 -        else {
    6.93 +        if (name.is_theory) {
    6.94            val commands0 = node.commands
    6.95            val commands1 = edit_text(text_edits, commands0)
    6.96            val commands2 =
    6.97 -            recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1)
    6.98 +            recover_spans(
    6.99 +              resources, syntax, doc_blobs_default, name, node.perspective.visible, commands1)
   6.100            node.update_commands(commands2)
   6.101          }
   6.102 +        else node
   6.103  
   6.104        case (_, Document.Node.Deps(_)) => node
   6.105  
   6.106 @@ -427,7 +429,7 @@
   6.107          if (node.same_perspective(perspective)) node
   6.108          else
   6.109            node.update_perspective(perspective).update_commands(
   6.110 -            consolidate_spans(resources, syntax, doc_blobs, reparse_limit,
   6.111 +            consolidate_spans(resources, syntax, doc_blobs_default, reparse_limit,
   6.112                name, visible, node.commands))
   6.113      }
   6.114    }
   6.115 @@ -454,6 +456,8 @@
   6.116              })
   6.117          val reparse_set = reparse.toSet
   6.118  
   6.119 +        val doc_blobs_default = doc_blobs.default(previous.nodes)
   6.120 +
   6.121          var nodes = nodes0
   6.122          val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
   6.123  
   6.124 @@ -469,11 +473,11 @@
   6.125              val node1 =
   6.126                if (reparse_set(name) && !commands.isEmpty)
   6.127                  node.update_commands(
   6.128 -                  reparse_spans(resources, syntax, doc_blobs,
   6.129 +                  reparse_spans(resources, syntax, doc_blobs_default,
   6.130                      name, commands, commands.head, commands.last))
   6.131                else node
   6.132              val node2 =
   6.133 -              (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
   6.134 +              (node1 /: edits)(text_edit(resources, syntax, doc_blobs_default, reparse_limit, _, _))
   6.135  
   6.136              if (!(node.same_perspective(node2.perspective)))
   6.137                doc_edits += (name -> node2.perspective)
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Mar 31 12:35:39 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Mar 31 15:05:24 2014 +0200
     7.3 @@ -164,28 +164,25 @@
     7.4    /* edits */
     7.5  
     7.6    def node_edits(
     7.7 -    clear: Boolean,
     7.8 -    text_edits: List[Text.Edit],
     7.9 -    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
    7.10 -  {
    7.11 -    Swing_Thread.require()
    7.12 -
    7.13 -    if (is_theory) {
    7.14 -      val header_edit = session.header_edit(node_name, node_header())
    7.15 -      if (clear)
    7.16 -        List(header_edit,
    7.17 -          node_name -> Document.Node.Clear(),
    7.18 -          node_name -> Document.Node.Edits(text_edits),
    7.19 -          node_name -> perspective)
    7.20 -      else
    7.21 -        List(header_edit,
    7.22 -          node_name -> Document.Node.Edits(text_edits),
    7.23 -          node_name -> perspective)
    7.24 +      clear: Boolean,
    7.25 +      text_edits: List[Text.Edit],
    7.26 +      perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
    7.27 +    get_blob() match {
    7.28 +      case None =>
    7.29 +        val header_edit = session.header_edit(node_name, node_header())
    7.30 +        if (clear)
    7.31 +          List(header_edit,
    7.32 +            node_name -> Document.Node.Clear(),
    7.33 +            node_name -> Document.Node.Edits(text_edits),
    7.34 +            node_name -> perspective)
    7.35 +        else
    7.36 +          List(header_edit,
    7.37 +            node_name -> Document.Node.Edits(text_edits),
    7.38 +            node_name -> perspective)
    7.39 +      case Some(blob) =>
    7.40 +        List(node_name -> Document.Node.Blob(blob),
    7.41 +          node_name -> Document.Node.Edits(text_edits))
    7.42      }
    7.43 -    else
    7.44 -      List(node_name -> Document.Node.Blob(),
    7.45 -        node_name -> Document.Node.Edits(text_edits))
    7.46 -  }
    7.47  
    7.48  
    7.49    /* pending edits */