src/Pure/PIDE/resources.scala
changeset 68381 2fd3a6d6ba2e
parent 68336 09ac56914b29
child 68762 8750edd967ce
--- a/src/Pure/PIDE/resources.scala	Tue Jun 05 14:15:49 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Jun 05 16:12:26 2018 +0200
@@ -216,7 +216,7 @@
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text],
-      consolidate: Boolean): Session.Change =
+      consolidate: List[Document.Node.Name]): Session.Change =
     Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
   def commit(change: Session.Change) { }