equal
deleted
inserted
replaced
162 theory = theory_name(qualifier, theory_base) |
162 theory = theory_name(qualifier, theory_base) |
163 theory_node <- find_theory_node(theory) |
163 theory_node <- find_theory_node(theory) |
164 if File.eq(theory_node.path.file, file) |
164 if File.eq(theory_node.path.file, file) |
165 } yield theory_node |
165 } yield theory_node |
166 } |
166 } |
167 |
|
168 def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] = |
|
169 (for { |
|
170 (options, thys) <- info.theories.iterator |
|
171 if options.bool("dump_checkpoint") |
|
172 (thy, _) <- thys.iterator |
|
173 } yield import_name(info, thy)).toSet |
|
174 |
167 |
175 def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = |
168 def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = |
176 { |
169 { |
177 val context_session = session_base.theory_qualifier(context_name) |
170 val context_session = session_base.theory_qualifier(context_name) |
178 val context_dir = |
171 val context_dir = |
260 def parse_change( |
253 def parse_change( |
261 reparse_limit: Int, |
254 reparse_limit: Int, |
262 previous: Document.Version, |
255 previous: Document.Version, |
263 doc_blobs: Document.Blobs, |
256 doc_blobs: Document.Blobs, |
264 edits: List[Document.Edit_Text], |
257 edits: List[Document.Edit_Text], |
265 consolidate: List[Document.Node.Name], |
258 consolidate: List[Document.Node.Name]): Session.Change = |
266 share_common_data: Boolean): Session.Change = |
259 Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) |
267 Thy_Syntax.parse_change( |
|
268 resources, reparse_limit, previous, doc_blobs, edits, consolidate, share_common_data) |
|
269 |
260 |
270 def commit(change: Session.Change) { } |
261 def commit(change: Session.Change) { } |
271 |
262 |
272 |
263 |
273 /* theory and file dependencies */ |
264 /* theory and file dependencies */ |