# HG changeset patch
# User wenzelm
# Date 1393495152 -3600
# Node ID 9fdd01fa48d1bee708e92630133f78004e55d9ef
# Parent  30fb00b5a9d3a9c2e0a17de1e16390253e3749b4
tuned iterator;

diff -r 30fb00b5a9d3 -r 9fdd01fa48d1 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 10:58:43 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 10:59:12 2014 +0100
@@ -83,7 +83,11 @@
     } yield model
 
   def document_blobs(): Document.Blobs =
-    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
+    (for {
+      buffer <- JEdit_Lib.jedit_buffers()
+      model <- document_model(buffer)
+      if !model.is_theory
+    } yield (model.node_name -> model.blob())).toMap
 
   def exit_models(buffers: List[Buffer])
   {