--- a/src/Pure/PIDE/resources.scala Mon Oct 07 10:51:20 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Oct 07 11:35:43 2019 +0200
@@ -165,13 +165,6 @@
} yield theory_node
}
- def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] =
- (for {
- (options, thys) <- info.theories.iterator
- if options.bool("dump_checkpoint")
- (thy, _) <- thys.iterator
- } yield import_name(info, thy)).toSet
-
def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
{
val context_session = session_base.theory_qualifier(context_name)
@@ -262,10 +255,8 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: List[Document.Node.Name],
- share_common_data: Boolean): Session.Change =
- Thy_Syntax.parse_change(
- resources, reparse_limit, previous, doc_blobs, edits, consolidate, share_common_data)
+ consolidate: List[Document.Node.Name]): Session.Change =
+ Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
def commit(change: Session.Change) { }