maintain document model for all files, with document view for theory only, and special blob for non-theory files;

--- a/src/Pure/PIDE/document.ML	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Nov 18 17:16:56 2013 +0100
@@ -70,7 +70,7 @@
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
-val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);

--- a/src/Pure/PIDE/document.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -64,6 +64,8 @@
 
     def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
 
+    val no_header = bad_header("No theory header")
+
     object Name
     {
       val empty = Name("", "", "")
@@ -83,6 +85,8 @@
           case _ => false
         }
       override def toString: String = theory
+
+      def is_theory: Boolean = !theory.isEmpty
     }
 
 
@@ -121,6 +125,7 @@
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
+    case class Blob[A, B](blob: Bytes) extends Edit[A, B]
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
@@ -184,27 +189,31 @@
     val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Node.Perspective_Command =
       Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
+    val blob: Bytes = Bytes.empty,
     _commands: Node.Commands = Node.Commands.empty)
   {
     def clear: Node = new Node(header = header)
 
     def update_header(new_header: Node.Header): Node =
-      new Node(new_header, perspective, _commands)
+      new Node(new_header, perspective, blob, _commands)
 
     def update_perspective(new_perspective: Node.Perspective_Command): Node =
-      new Node(header, new_perspective, _commands)
+      new Node(header, new_perspective, blob, _commands)
 
     def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
+    def update_blob(new_blob: Bytes): Node =
+      new Node(header, perspective, new_blob, _commands)
+
     def commands: Linear_Set[Command] = _commands.commands
     def thy_load_commands: List[Command] = _commands.thy_load_commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else new Node(header, perspective, Node.Commands(new_commands))
+      else new Node(header, perspective, blob, Node.Commands(new_commands))
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.range(i)

--- a/src/Pure/PIDE/protocol.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -335,6 +335,7 @@
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
+          // FIXME Document.Node.Blob (!??)
           { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>

--- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -355,6 +355,8 @@
         else
           node.update_perspective(perspective).update_commands(
             consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
+
+      case (_, Document.Node.Blob(blob)) => node.update_blob(blob)
     }
   }
 

--- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -60,17 +60,23 @@
 {
   /* header */
 
+  def is_theory: Boolean = node_name.is_theory
+
   def node_header(): Document.Node.Header =
   {
     Swing_Thread.require()
-    JEdit_Lib.buffer_lock(buffer) {
-      Exn.capture {
-        PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
-      } match {
-        case Exn.Res(header) => header
-        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
+
+    if (is_theory) {
+      JEdit_Lib.buffer_lock(buffer) {
+        Exn.capture {
+          PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
+        } match {
+          case Exn.Res(header) => header
+          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
+        }
       }
     }
+    else Document.Node.no_header
   }
 
 
@@ -96,7 +102,7 @@
   {
     Swing_Thread.require()
 
-    if (Isabelle.continuous_checking) {
+    if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
       Document.Node.Perspective(node_required, Text.Perspective(
         for {
@@ -108,6 +114,14 @@
   }
 
 
+  /* blob */
+
+  // FIXME caching
+  // FIXME precise file content (encoding)
+  def blob(): Bytes =
+    Swing_Thread.require { Bytes(buffer.getText(0, buffer.getLength)) }
+
+
   /* edits */
 
   def init_edits(): List[Document.Edit_Text] =
@@ -118,10 +132,13 @@
     val text = JEdit_Lib.buffer_text(buffer)
     val perspective = node_perspective()
 
-    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)
+    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(blob()))
   }
 
   def node_edits(
@@ -131,16 +148,20 @@
   {
     Swing_Thread.require()
 
-    val header_edit = session.header_edit(node_name, node_header())
-    if (clear)
-      List(header_edit,
-        node_name -> Document.Node.Clear(),
-        node_name -> Document.Node.Edits(text_edits),
-        node_name -> perspective)
+    if (is_theory) {
+      val header_edit = session.header_edit(node_name, node_header())
+      if (clear)
+        List(header_edit,
+          node_name -> Document.Node.Clear(),
+          node_name -> Document.Node.Edits(text_edits),
+          node_name -> perspective)
+      else
+        List(header_edit,
+          node_name -> Document.Node.Edits(text_edits),
+          node_name -> perspective)
+    }
     else
-      List(header_edit,
-        node_name -> Document.Node.Edits(text_edits),
-        node_name -> perspective)
+      List(node_name -> Document.Node.Blob(blob()))
   }
 
 

--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -133,15 +133,15 @@
 
 
 class Isabelle_Sidekick_Default extends
-  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name)
+  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
 
 
 class Isabelle_Sidekick_Options extends
-  Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy)
+  Isabelle_Sidekick_Structure("isabelle-options", b => Some(PIDE.thy_load.dummy_node_name(b)))
 
 
 class Isabelle_Sidekick_Root extends
-  Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy)
+  Isabelle_Sidekick_Structure("isabelle-root", b => Some(PIDE.thy_load.dummy_node_name(b)))
 
 
 class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -22,13 +22,19 @@
 {
   /* document node names */
 
-  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
-    Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName))
+  def dummy_node_name(buffer: Buffer): Document.Node.Name =
+    Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName)
 
-  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+  def node_name(buffer: Buffer): Document.Node.Name =
   {
     val name = JEdit_Lib.buffer_name(buffer)
-    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+    Document.Node.Name(name, buffer.getDirectory, Thy_Header.thy_name(name).getOrElse(""))
+  }
+
+  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
+  {
+    val name = node_name(buffer)
+    if (name.is_theory) Some(name) else None
   }
 
 

--- a/src/Tools/jEdit/src/plugin.scala	Mon Nov 18 09:45:50 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Nov 18 17:16:56 2013 +0100
@@ -96,21 +96,18 @@
       val init_edits =
         (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
-            val (model_edits, opt_model) =
-              thy_load.buffer_node_name(buffer) match {
-                case Some(node_name) =>
-                  document_model(buffer) match {
-                    case Some(model) if model.node_name == node_name => (Nil, Some(model))
-                    case _ =>
-                      val model = Document_Model.init(session, buffer, node_name)
-                      (model.init_edits(), Some(model))
-                  }
-                case None => (Nil, None)
+            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 (opt_model.isDefined) {
+            if (model.is_theory) {
               for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
-                if (document_view(text_area).map(_.model) != opt_model)
-                  Document_View.init(opt_model.get, text_area)
+                if (document_view(text_area).map(_.model) != Some(model))
+                  Document_View.init(model, text_area)
               }
             }
             model_edits ::: edits
@@ -124,8 +121,8 @@
   {
     JEdit_Lib.swing_buffer_lock(buffer) {
       document_model(buffer) match {
-        case Some(model) => Document_View.init(model, text_area)
-        case None =>
+        case Some(model) if model.is_theory => Document_View.init(model, text_area)
+        case _ =>
       }
     }
   }
@@ -163,8 +160,11 @@
             buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
 
           val thys =
-            for (buffer <- buffers; model <- PIDE.document_model(buffer))
-              yield model.node_name
+            for {
+              buffer <- buffers
+              model <- PIDE.document_model(buffer)
+              if model.is_theory
+            } yield model.node_name
 
           val thy_info = new Thy_Info(PIDE.thy_load)
           // FIXME avoid I/O in Swing thread!?!