some support for blobs (arbitrary text files) within document nodes;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/blob.scala	Sat Jul 09 13:29:33 2011 +0200
@@ -0,0 +1,28 @@
+/*  Title:      Pure/PIDE/blob.scala
+    Author:     Makarius
+
+Unidentified text with markup.
+*/
+
+package isabelle
+
+
+object Blob
+{
+  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
+  {
+    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
+  }
+}
+
+
+sealed case class Blob(val source: String)
+{
+  def source(range: Text.Range): String = source.substring(range.start, range.stop)
+
+  lazy val symbol_index = new Symbol.Index(source)
+  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
+  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+
+  val empty_state: Blob.State = Blob.State(this)
+}

--- a/src/Pure/PIDE/document.scala	Sat Jul 09 12:56:51 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Jul 09 13:29:33 2011 +0200
@@ -46,10 +46,10 @@
 
   object Node
   {
-    class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
-    val empty_header = new Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
+    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
+    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
 
-    val empty: Node = new Node(empty_header, Linear_Set())
+    val empty: Node = Node(empty_header, Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -65,11 +65,14 @@
 
   private val block_size = 1024
 
-  class Node(val header: Node.Header, val commands: Linear_Set[Command])
+  sealed case class Node(
+    val header: Node.Header,
+    val blobs: Map[String, Blob],
+    val commands: Linear_Set[Command])
   {
     /* header */
 
-    def set_header(header: Node.Header): Node = new Node(header, commands)
+    def set_header(new_header: Node.Header): Node = copy(header = new_header)
 
 
     /* commands */
@@ -209,7 +212,7 @@
     }
   }
 
-  case class State(
+  sealed case class State(
     val versions: Map[Version_ID, Version] = Map(),
     val commands: Map[Command_ID, Command.State] = Map(),
     val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),

--- a/src/Pure/Thy/thy_syntax.scala	Sat Jul 09 12:56:51 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jul 09 13:29:33 2011 +0200
@@ -194,7 +194,7 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Some(cmd_edits))
-          nodes += (name -> new Document.Node(node.header, commands2))
+          nodes += (name -> Document.Node(node.header, node.blobs, commands2))
       }
       (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
     }

--- a/src/Pure/build-jars	Sat Jul 09 12:56:51 2011 +0200
+++ b/src/Pure/build-jars	Sat Jul 09 13:29:33 2011 +0200
@@ -30,6 +30,7 @@
   Isar/outer_syntax.scala
   Isar/parse.scala
   Isar/token.scala
+  PIDE/blob.scala
   PIDE/command.scala
   PIDE/document.scala
   PIDE/isar_document.scala

--- a/src/Tools/jEdit/src/document_model.scala	Sat Jul 09 12:56:51 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jul 09 13:29:33 2011 +0200
@@ -62,7 +62,7 @@
   /* pending text edits */
 
   private def node_header(): Document.Node.Header =
-    new Document.Node.Header(master_dir,
+    Document.Node.Header(master_dir,
       Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
 
   private object pending_edits  // owned by Swing thread