# HG changeset patch
# User wenzelm
# Date 1393531329 -3600
# Node ID 5821b1937fa5a6a6b0d4ffb398688a436e9e1aaf
# Parent  4670f18baba58125a9db767d0f45d2e410bb6677
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
clarified asynchronous event propagation: determine buffers where they are actually accessed;
tuned signature;

diff -r 4670f18baba5 -r 5821b1937fa5 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 17:56:59 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 21:02:09 2014 +0100
@@ -163,24 +163,6 @@
 
   /* edits */
 
-  def init_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
-  {
-    Swing_Thread.require()
-
-    val header = node_header()
-    val text = JEdit_Lib.buffer_text(buffer)
-    val (_, perspective) = node_perspective(doc_blobs)
-
-    if (is_theory)
-      List(session.header_edit(node_name, header),
-        node_name -> Document.Node.Clear(),
-        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
-        node_name -> perspective)
-    else
-      List(node_name -> Document.Node.Blob(),
-        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))))
-  }
-
   def node_edits(
     clear: Boolean,
     text_edits: List[Text.Edit],
@@ -257,7 +239,7 @@
   {
     override def bufferLoaded(buffer: JEditBuffer)
     {
-      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
+      pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
     }
 
     override def contentInserted(buffer: JEditBuffer,
@@ -280,6 +262,7 @@
 
   private def activate()
   {
+    pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
     buffer.addBufferListener(buffer_listener)
     Token_Markup.refresh_buffer(buffer)
   }
diff -r 4670f18baba5 -r 5821b1937fa5 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 17:56:59 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 21:02:09 2014 +0100
@@ -38,10 +38,7 @@
   @volatile var plugin: Plugin = null
   @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
 
-  def options_changed() {
-    session.global_options.event(Session.Global_Options(options.value))
-    plugin.load_theories()
-  }
+  def options_changed() { plugin.options_changed() }
 
   def thy_load(): JEdit_Thy_Load =
     session.thy_load.asInstanceOf[JEdit_Thy_Load]
@@ -102,33 +99,30 @@
       }
   }
 
-  def init_models(buffers: List[Buffer])
+  def init_models()
   {
     Swing_Thread.now {
       PIDE.editor.flush()
-      val doc_blobs = document_blobs()
-      val init_edits =
-        (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
-          JEdit_Lib.buffer_lock(buffer) {
-            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(doc_blobs), model)
-                }
-              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
+
+      for {
+        buffer <- JEdit_Lib.jedit_buffers()
+        if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED)
+      } {
+        JEdit_Lib.buffer_lock(buffer) {
+          val node_name = thy_load.node_name(buffer)
+          val model =
+            document_model(buffer) match {
+              case Some(model) if model.node_name == node_name => model
+              case _ => Document_Model.init(session, buffer, node_name)
             }
-          }
+          for {
+            text_area <- JEdit_Lib.jedit_text_areas(buffer)
+            if document_view(text_area).map(_.model) != Some(model)
+          } Document_View.init(model, text_area)
         }
-      session.update(doc_blobs, init_edits)
+      }
+
+      PIDE.editor.invoke()
     }
   }
 
@@ -174,16 +168,22 @@
 
 class Plugin extends EBPlugin
 {
+  /* options */
+
+  def options_changed() {
+    PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+    Swing_Thread.later { delay_load.invoke() }
+  }
+
+
   /* theory files */
 
   private lazy val delay_init =
     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
-      PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
+      PIDE.init_models()
     }
 
-  def load_theories() { Swing_Thread.later { delay_load.invoke() }}
-
   private lazy val delay_load =
     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
@@ -251,7 +251,7 @@
 
             case Session.Ready =>
               PIDE.session.update_options(PIDE.options.value)
-              PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
+              PIDE.init_models()
               Swing_Thread.later { delay_load.invoke() }
 
             case Session.Shutdown =>
@@ -291,9 +291,8 @@
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
           if (PIDE.session.is_ready) {
-            val buffer = msg.getBuffer
-            if (buffer != null && !buffer.isLoading) delay_init.invoke()
-            load_theories()
+            delay_init.invoke()
+            delay_load.invoke()
           }
 
         case msg: EditPaneUpdate