src/Tools/jEdit/src/document_model.scala

 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
 
 
-object Document_Model
-{
+object Document_Model {
   /* document models */
 
   sealed case class State(
     models: Map[Document.Node.Name, Document_Model] = Map.empty,
     buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
-    overlays: Document.Overlays = Document.Overlays.empty)
-  {
+    overlays: Document.Overlays = Document.Overlays.empty
+  ) {
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
         (node_name, model) <- models.iterator
         if model.isInstanceOf[File_Model]
       } yield (node_name, model.asInstanceOf[File_Model])

         (for {
           (node_name, model) <- models.iterator
           blob <- model.get_blob
         } yield (node_name -> blob)).toMap)
 
-    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
-      : (Buffer_Model, State) =
-    {
+    def open_buffer(
+      session: Session,
+      node_name: Document.Node.Name,
+      buffer: Buffer
+    ) : (Buffer_Model, State) = {
       val old_model =
         models.get(node_name) match {
           case Some(file_model: File_Model) => Some(file_model)
           case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
           case _ => None

       (buffer_model,
         copy(models = models + (node_name -> buffer_model),
           buffer_models = buffer_models + (buffer -> buffer_model)))
     }
 
-    def close_buffer(buffer: JEditBuffer): State =
-    {
+    def close_buffer(buffer: JEditBuffer): State = {
       buffer_models.get(buffer) match {
         case None => this
         case Some(buffer_model) =>
           val file_model = buffer_model.exit()
           copy(models = models + (file_model.node_name -> file_model),

     state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
 
 
   /* sync external files */
 
-  def sync_files(changed_files: Set[JFile]): Boolean =
-  {
-    state.change_result(st =>
-      {
-        val changed_models =
-          (for {
-            (node_name, model) <- st.file_models_iterator
-            file <- model.file if changed_files(file)
-            text <- PIDE.resources.read_file_content(node_name)
-            if model.content.text != text
-          } yield {
-            val content = Document_Model.File_Content(text)
-            val edits = Text.Edit.replace(0, model.content.text, text)
-            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
-          }).toList
-        if (changed_models.isEmpty) (false, st)
-        else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
-      })
+  def sync_files(changed_files: Set[JFile]): Boolean = {
+    state.change_result(st => {
+      val changed_models =
+        (for {
+          (node_name, model) <- st.file_models_iterator
+          file <- model.file if changed_files(file)
+          text <- PIDE.resources.read_file_content(node_name)
+          if model.content.text != text
+        } yield {
+          val content = Document_Model.File_Content(text)
+          val edits = Text.Edit.replace(0, model.content.text, text)
+          (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
+        }).toList
+      if (changed_models.isEmpty) (false, st)
+      else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
+    })
   }
 
 
   /* syntax */
 
-  def syntax_changed(names: List[Document.Node.Name]): Unit =
-  {
+  def syntax_changed(names: List[Document.Node.Name]): Unit = {
     GUI_Thread.require {}
 
     val models = state.value.models
     for (name <- names.iterator; model <- models.get(name)) {
       model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }

   }
 
 
   /* init and exit */
 
-  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
-  {
+  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = {
     GUI_Thread.require {}
     state.change_result(st =>
       st.buffer_models.get(buffer) match {
         case Some(buffer_model) if buffer_model.node_name == node_name =>
           buffer_model.init_token_marker()

           buffer.propertiesChanged()
           res
       })
   }
 
-  def exit(buffer: Buffer): Unit =
-  {
+  def exit(buffer: Buffer): Unit = {
     GUI_Thread.require {}
     state.change(st =>
       if (st.buffer_models.isDefinedAt(buffer)) {
         val res = st.close_buffer(buffer)
         buffer.propertiesChanged()
         res
       }
       else st)
   }
 
-  def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit =
-  {
+  def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit = {
     GUI_Thread.require {}
     state.change(st =>
       files.foldLeft(st) {
         case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
       })

       (node_name, model) <- state.value.models.iterator
       if model.node_required
     } yield node_name).toSet
 
   def node_required(
-    name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit =
-  {
+    name: Document.Node.Name,
+    toggle: Boolean = false,
+    set: Boolean = false
+  ) : Unit = {
     GUI_Thread.require {}
 
     val changed =
       state.change_result(st =>
         st.models.get(name) match {

       node_required(model.node_name, toggle = toggle, set = set))
 
 
   /* flushed edits */
 
-  def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
-  {
-    GUI_Thread.require {}
-
-    state.change_result(st =>
-      {
-        val doc_blobs = st.document_blobs
-
-        val buffer_edits =
-          (for {
-            (_, model) <- st.buffer_models.iterator
-            edit <- model.flush_edits(doc_blobs, hidden).iterator
-          } yield edit).toList
-
-        val file_edits =
-          (for {
-            (node_name, model) <- st.file_models_iterator
-            (edits, model1) <- model.flush_edits(doc_blobs, hidden)
-          } yield (edits, node_name -> model1)).toList
-
-        val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
-
-        val purge_edits =
-          if (purge) {
-            val purged =
-              (for ((node_name, model) <- st.file_models_iterator)
-               yield (node_name -> model.purge_edits(doc_blobs))).toList
-
-            val imports =
-            {
-              val open_nodes =
-                (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
-              val touched_nodes = model_edits.map(_._1)
-              val pending_nodes = for ((node_name, None) <- purged) yield node_name
-              (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
-            }
-            val retain = PIDE.resources.dependencies(imports).theories.toSet
-
-            for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
-              yield edit
+  def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = {
+    GUI_Thread.require {}
+
+    state.change_result(st => {
+      val doc_blobs = st.document_blobs
+
+      val buffer_edits =
+        (for {
+          (_, model) <- st.buffer_models.iterator
+          edit <- model.flush_edits(doc_blobs, hidden).iterator
+        } yield edit).toList
+
+      val file_edits =
+        (for {
+          (node_name, model) <- st.file_models_iterator
+          (edits, model1) <- model.flush_edits(doc_blobs, hidden)
+        } yield (edits, node_name -> model1)).toList
+
+      val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
+
+      val purge_edits =
+        if (purge) {
+          val purged =
+            (for ((node_name, model) <- st.file_models_iterator)
+             yield (node_name -> model.purge_edits(doc_blobs))).toList
+
+          val imports = {
+            val open_nodes =
+              (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
+            val touched_nodes = model_edits.map(_._1)
+            val pending_nodes = for ((node_name, None) <- purged) yield node_name
+            (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
           }
-          else Nil
-
-        val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
-        PIDE.plugin.file_watcher.purge(
-          (for {
-            (_, model) <- st1.file_models_iterator
-            file <- model.file
-          } yield file.getParentFile).toSet)
-
-        ((doc_blobs, model_edits ::: purge_edits), st1)
-      })
+          val retain = PIDE.resources.dependencies(imports).theories.toSet
+
+          for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
+            yield edit
+        }
+        else Nil
+
+      val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
+      PIDE.plugin.file_watcher.purge(
+        (for {
+          (_, model) <- st1.file_models_iterator
+          file <- model.file
+        } yield file.getParentFile).toSet)
+
+      ((doc_blobs, model_edits ::: purge_edits), st1)
+    })
   }
 
 
   /* file content */
 
-  sealed case class File_Content(text: String)
-  {
+  sealed case class File_Content(text: String) {
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
   }
 
 
   /* HTTP preview */
 
-  def open_preview(view: View, plain_text: Boolean): Unit =
-  {
+  def open_preview(view: View, plain_text: Boolean): Unit = {
     Document_Model.get(view.getBuffer) match {
       case Some(model) =>
         val url = Preview_Service.server_url(plain_text, model.node_name)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
   }
 
-  object Preview_Service extends HTTP.Service("preview")
-  {
+  object Preview_Service extends HTTP.Service("preview") {
     service =>
 
     private val plain_text_prefix = "plain_text="
 
     def server_url(plain_text: Boolean, node_name: Document.Node.Name): String =

         HTTP.Response.html(document.content)
       }
   }
 }
 
-sealed abstract class Document_Model extends Document.Model
-{
+sealed abstract class Document_Model extends Document.Model {
   /* perspective */
 
   def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
 
   def node_perspective(
-    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
-  {
+    doc_blobs: Document.Blobs,
+    hidden: Boolean
+  ): (Boolean, Document.Node.Perspective_Text) = {
     GUI_Thread.require {}
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
 

   }
 
 
   /* snapshot */
 
-  @tailrec final def await_stable_snapshot(): Document.Snapshot =
-  {
+  @tailrec final def await_stable_snapshot(): Document.Snapshot = {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       PIDE.options.seconds("editor_output_delay").sleep()
       await_stable_snapshot()
     }
     else snapshot
   }
 }
 
-object File_Model
-{
+object File_Model {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
       false, Document.Node.no_perspective_text, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
     node_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
-    pending_edits: List[Text.Edit] = Nil): File_Model =
-  {
+    pending_edits: List[Text.Edit] = Nil
+  ): File_Model = {
     val file = JEdit_Lib.check_file(node_name.node)
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
     val node_required1 = node_required || File_Format.registry.is_theory(node_name)

   node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
   node_required: Boolean,
   last_perspective: Document.Node.Perspective_Text,
-  pending_edits: List[Text.Edit]) extends Document_Model
-{
+  pending_edits: List[Text.Edit]
+) extends Document_Model {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     range.try_substring(content.text)
 

         val content1 = Document_Model.File_Content(text)
         val pending_edits1 = pending_edits ::: edits
         Some(copy(content = content1, pending_edits = pending_edits1))
     }
 
-  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
-    : Option[(List[Document.Edit_Text], File_Model)] =
-  {
+  def flush_edits(
+    doc_blobs: Document.Blobs,
+    hidden: Boolean
+  ) : Option[(List[Document.Edit_Text], File_Model)] = {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val edits = node_edits(node_header, pending_edits, perspective)
       Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
     }

   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
-  extends Document_Model
-{
+extends Document_Model {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     JEdit_Lib.get_text(buffer, range)
 
 
   /* header */
 
-  def node_header(): Document.Node.Header =
-  {
+  def node_header(): Document.Node.Header = {
     GUI_Thread.require {}
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
         PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)

     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer)
       doc_view <- Document_View.get(text_area)
     } yield doc_view
 
-  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
-  {
+  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = {
     GUI_Thread.require {}
 
     (for {
       doc_view <- document_view_iterator
       range <- doc_view.perspective(snapshot).ranges.iterator

     }
 
 
   /* pending edits */
 
-  private object pending_edits
-  {
+  private object pending_edits {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = Document.Node.no_perspective_text
 
     def nonEmpty: Boolean = synchronized { pending.nonEmpty }
     def get_edits: List[Text.Edit] = synchronized { pending.toList }

     pending_edits.flush_edits(doc_blobs, hidden)
 
 
   /* buffer listener */
 
-  private val buffer_listener: BufferListener = new BufferAdapter
-  {
-    override def contentInserted(buffer: JEditBuffer,
-      start_line: Int, offset: Int, num_lines: Int, length: Int): Unit =
-    {
+  private val buffer_listener: BufferListener = new BufferAdapter {
+    override def contentInserted(
+      buffer: JEditBuffer,
+      start_line: Int,
+      offset: Int,
+      num_lines: Int,
+      length: Int
+    ): Unit = {
       pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
     }
 
-    override def preContentRemoved(buffer: JEditBuffer,
-      start_line: Int, offset: Int, num_lines: Int, removed_length: Int): Unit =
-    {
+    override def preContentRemoved(
+      buffer: JEditBuffer,
+      start_line: Int,
+      offset: Int,
+      num_lines: Int,
+      removed_length: Int
+    ): Unit = {
       pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
     }
   }
 
 
   /* syntax */
 
-  def syntax_changed(): Unit =
-  {
+  def syntax_changed(): Unit = {
     JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
     for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
       Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
         invoke(text_area)
     buffer.invalidateCachedFoldLevels()
   }
 
-  def init_token_marker(): Unit =
-  {
+  def init_token_marker(): Unit = {
     Isabelle.buffer_token_marker(buffer) match {
       case Some(marker) if marker != buffer.getTokenMarker =>
         buffer.setTokenMarker(marker)
         syntax_changed()
       case _ =>

   }
 
 
   /* init */
 
-  def init(old_model: Option[File_Model]): Buffer_Model =
-  {
+  def init(old_model: Option[File_Model]): Buffer_Model = {
     GUI_Thread.require {}
 
     old_model match {
       case None =>
         pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))

   }
 
 
   /* exit */
 
-  def exit(): File_Model =
-  {
+  def exit(): File_Model = {
     GUI_Thread.require {}
 
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()