# HG changeset patch
# User wenzelm
# Date 1385150066 -3600
# Node ID ceb190f4f69ff4b22f1bd89eebbc14fd6fc1e0be
# Parent  7f36da77130d40c81e19c55268578065f2978602
exclude gzipped files from document model, to avoid confusion about actual file name and content;

diff -r 7f36da77130d -r ceb190f4f69f src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Nov 22 20:37:19 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Nov 22 20:54:26 2013 +0100
@@ -104,21 +104,24 @@
       val init_edits =
         (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
-            val node_name = thy_load.node_name(buffer)
-            val (model_edits, model) =
-              document_model(buffer) match {
-                case Some(model) if model.node_name == node_name => (Nil, model)
-                case _ =>
-                  val model = Document_Model.init(session, buffer, node_name)
-                  (model.init_edits(), model)
+            if (buffer.getBooleanProperty(Buffer.GZIPPED)) edits
+            else {
+              val node_name = thy_load.node_name(buffer)
+              val (model_edits, model) =
+                document_model(buffer) match {
+                  case Some(model) if model.node_name == node_name => (Nil, model)
+                  case _ =>
+                    val model = Document_Model.init(session, buffer, node_name)
+                    (model.init_edits(), model)
+                }
+              if (model.is_theory) {
+                for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
+                  if (document_view(text_area).map(_.model) != Some(model))
+                    Document_View.init(model, text_area)
+                }
               }
-            if (model.is_theory) {
-              for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
-                if (document_view(text_area).map(_.model) != Some(model))
-                  Document_View.init(model, text_area)
-              }
+              model_edits ::: edits
             }
-            model_edits ::: edits
           }
         }
       session.update(document_blobs(), init_edits)