--- a/src/Tools/jEdit/src/plugin.scala Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Feb 27 14:07:04 2014 +0100
@@ -83,11 +83,12 @@
} yield model
def document_blobs(): Document.Blobs =
- (for {
- buffer <- JEdit_Lib.jedit_buffers()
- model <- document_model(buffer)
- if !model.is_theory
- } yield (model.node_name -> model.blob())).toMap
+ Document.Blobs(
+ (for {
+ buffer <- JEdit_Lib.jedit_buffers()
+ model <- document_model(buffer)
+ blob <- model.get_blob()
+ } yield (model.node_name -> blob)).toMap)
def exit_models(buffers: List[Buffer])
{