tuned signature -- more static typing;
authorwenzelm
Mon Mar 31 15:28:14 2014 +0200 (2014-03-31)
changeset 5633660434514ec0a
parent 56335 8953d4cc060a
child 56337 520148f9921d
tuned signature -- more static typing;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Mar 31 15:05:24 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Mar 31 15:28:14 2014 +0200
     1.3 @@ -52,19 +52,17 @@
     1.4  
     1.5    object Blobs
     1.6    {
     1.7 -    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs, Nodes.empty)
     1.8 +    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
     1.9      val empty: Blobs = apply(Map.empty)
    1.10    }
    1.11  
    1.12 -  final class Blobs private(blobs: Map[Node.Name, Blob], default_nodes: Nodes)
    1.13 +  final class Blobs private(blobs: Map[Node.Name, Blob])
    1.14    {
    1.15      private lazy val digests: Map[SHA1.Digest, Blob] =
    1.16        for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
    1.17  
    1.18      def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
    1.19 -
    1.20 -    def get(name: Node.Name): Option[Blob] =
    1.21 -      blobs.get(name) orElse default_nodes(name).get_blob
    1.22 +    def get(name: Node.Name): Option[Blob] = blobs.get(name)
    1.23  
    1.24      def changed(name: Node.Name): Boolean =
    1.25        get(name) match {
    1.26 @@ -72,8 +70,6 @@
    1.27          case None => false
    1.28        }
    1.29  
    1.30 -    def default(nodes: Nodes): Blobs = new Blobs(blobs, nodes)
    1.31 -
    1.32      override def toString: String = blobs.mkString("Blobs(", ",", ")")
    1.33    }
    1.34  
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Mar 31 15:05:24 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Mar 31 15:28:14 2014 +0200
     2.3 @@ -262,14 +262,14 @@
     2.4        syntax: Outer_Syntax,
     2.5        node_name: Document.Node.Name,
     2.6        span: List[Token],
     2.7 -      doc_blobs_default: Document.Blobs)
     2.8 +      get_blob: Document.Node.Name => Option[Document.Blob])
     2.9      : List[Command.Blob] =
    2.10    {
    2.11      span_files(syntax, span).map(file_name =>
    2.12        Exn.capture {
    2.13          val name =
    2.14            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
    2.15 -        val blob = doc_blobs_default.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
    2.16 +        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
    2.17          (name, blob)
    2.18        })
    2.19    }
    2.20 @@ -292,7 +292,7 @@
    2.21    private def reparse_spans(
    2.22      resources: Resources,
    2.23      syntax: Outer_Syntax,
    2.24 -    doc_blobs_default: Document.Blobs,
    2.25 +    get_blob: Document.Node.Name => Option[Document.Blob],
    2.26      name: Document.Node.Name,
    2.27      commands: Linear_Set[Command],
    2.28      first: Command, last: Command): Linear_Set[Command] =
    2.29 @@ -300,7 +300,7 @@
    2.30      val cmds0 = commands.iterator(first, last).toList
    2.31      val blobs_spans0 =
    2.32        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    2.33 -        map(span => (resolve_files(resources, syntax, name, span, doc_blobs_default), span))
    2.34 +        map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
    2.35  
    2.36      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    2.37  
    2.38 @@ -327,7 +327,7 @@
    2.39    private def recover_spans(
    2.40      resources: Resources,
    2.41      syntax: Outer_Syntax,
    2.42 -    doc_blobs_default: Document.Blobs,
    2.43 +    get_blob: Document.Node.Name => Option[Document.Blob],
    2.44      name: Document.Node.Name,
    2.45      perspective: Command.Perspective,
    2.46      commands: Linear_Set[Command]): Linear_Set[Command] =
    2.47 @@ -343,7 +343,7 @@
    2.48          case Some(first_unparsed) =>
    2.49            val first = next_invisible_command(cmds.reverse, first_unparsed)
    2.50            val last = next_invisible_command(cmds, first_unparsed)
    2.51 -          recover(reparse_spans(resources, syntax, doc_blobs_default, name, cmds, first, last))
    2.52 +          recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
    2.53          case None => cmds
    2.54        }
    2.55      recover(commands)
    2.56 @@ -355,7 +355,7 @@
    2.57    private def consolidate_spans(
    2.58      resources: Resources,
    2.59      syntax: Outer_Syntax,
    2.60 -    doc_blobs_default: Document.Blobs,
    2.61 +    get_blob: Document.Node.Name => Option[Document.Blob],
    2.62      reparse_limit: Int,
    2.63      name: Document.Node.Name,
    2.64      perspective: Command.Perspective,
    2.65 @@ -375,8 +375,7 @@
    2.66                  last = it.next
    2.67                  i += last.length
    2.68                }
    2.69 -              reparse_spans(
    2.70 -                resources, syntax, doc_blobs_default, name, commands, first_unfinished, last)
    2.71 +              reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
    2.72              case None => commands
    2.73            }
    2.74          case None => commands
    2.75 @@ -400,7 +399,7 @@
    2.76    private def text_edit(
    2.77      resources: Resources,
    2.78      syntax: Outer_Syntax,
    2.79 -    doc_blobs_default: Document.Blobs,
    2.80 +    get_blob: Document.Node.Name => Option[Document.Blob],
    2.81      reparse_limit: Int,
    2.82      node: Document.Node, edit: Document.Edit_Text): Document.Node =
    2.83    {
    2.84 @@ -414,8 +413,7 @@
    2.85            val commands0 = node.commands
    2.86            val commands1 = edit_text(text_edits, commands0)
    2.87            val commands2 =
    2.88 -            recover_spans(
    2.89 -              resources, syntax, doc_blobs_default, name, node.perspective.visible, commands1)
    2.90 +            recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
    2.91            node.update_commands(commands2)
    2.92          }
    2.93          else node
    2.94 @@ -429,7 +427,7 @@
    2.95          if (node.same_perspective(perspective)) node
    2.96          else
    2.97            node.update_perspective(perspective).update_commands(
    2.98 -            consolidate_spans(resources, syntax, doc_blobs_default, reparse_limit,
    2.99 +            consolidate_spans(resources, syntax, get_blob, reparse_limit,
   2.100                name, visible, node.commands))
   2.101      }
   2.102    }
   2.103 @@ -441,6 +439,9 @@
   2.104        doc_blobs: Document.Blobs,
   2.105        edits: List[Document.Edit_Text]): Session.Change =
   2.106    {
   2.107 +    def get_blob(name: Document.Node.Name) =
   2.108 +      doc_blobs.get(name) orElse previous.nodes(name).get_blob
   2.109 +
   2.110      val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
   2.111        header_edits(resources.base_syntax, previous, edits)
   2.112  
   2.113 @@ -456,8 +457,6 @@
   2.114              })
   2.115          val reparse_set = reparse.toSet
   2.116  
   2.117 -        val doc_blobs_default = doc_blobs.default(previous.nodes)
   2.118 -
   2.119          var nodes = nodes0
   2.120          val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
   2.121  
   2.122 @@ -473,11 +472,11 @@
   2.123              val node1 =
   2.124                if (reparse_set(name) && !commands.isEmpty)
   2.125                  node.update_commands(
   2.126 -                  reparse_spans(resources, syntax, doc_blobs_default,
   2.127 +                  reparse_spans(resources, syntax, get_blob,
   2.128                      name, commands, commands.head, commands.last))
   2.129                else node
   2.130              val node2 =
   2.131 -              (node1 /: edits)(text_edit(resources, syntax, doc_blobs_default, reparse_limit, _, _))
   2.132 +              (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
   2.133  
   2.134              if (!(node.same_perspective(node2.perspective)))
   2.135                doc_edits += (name -> node2.perspective)