# HG changeset patch
# User wenzelm
# Date 1349116509 -7200
# Node ID 954d1c94f55ff397e4e631c4d0da0271673b1ba2
# Parent  c4e2762a265c38d8c41376476cd530269d4c6985
removed unused module Blob;

diff -r c4e2762a265c -r 954d1c94f55f src/Pure/PIDE/blob.scala
--- a/src/Pure/PIDE/blob.scala	Mon Oct 01 20:17:30 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-/*  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.Markup): 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 init_state: Blob.State = Blob.State(this)
-}
diff -r c4e2762a265c -r 954d1c94f55f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Oct 01 20:17:30 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Oct 01 20:35:09 2012 +0200
@@ -110,22 +110,18 @@
   final class Node private(
     val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Command.Perspective = Command.Perspective.empty,
-    val blobs: Map[String, Blob] = Map.empty,
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
     def clear: Node = new Node(header = header)
 
     def update_header(new_header: Node.Header): Node =
-      new Node(new_header, perspective, blobs, commands)
+      new Node(new_header, perspective, commands)
 
     def update_perspective(new_perspective: Command.Perspective): Node =
-      new Node(header, new_perspective, blobs, commands)
-
-    def update_blobs(new_blobs: Map[String, Blob]): Node =
-      new Node(header, perspective, new_blobs, commands)
+      new Node(header, new_perspective, commands)
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
-      new Node(header, perspective, blobs, new_commands)
+      new Node(header, perspective, new_commands)
 
 
     /* commands */
diff -r c4e2762a265c -r 954d1c94f55f src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Oct 01 20:17:30 2012 +0200
+++ b/src/Pure/build-jars	Mon Oct 01 20:35:09 2012 +0200
@@ -30,7 +30,6 @@
   Isar/outer_syntax.scala
   Isar/parse.scala
   Isar/token.scala
-  PIDE/blob.scala
   PIDE/command.scala
   PIDE/document.scala
   PIDE/isabelle_markup.scala