removed unused module Blob;
authorwenzelm
Mon Oct 01 20:35:09 2012 +0200 (2012-10-01 ago)
changeset 49678954d1c94f55f
parent 49677 c4e2762a265c
child 49679 835d55b4fc8c
removed unused module Blob;
src/Pure/PIDE/blob.scala
src/Pure/PIDE/document.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/PIDE/blob.scala	Mon Oct 01 20:17:30 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,28 +0,0 @@
     1.4 -/*  Title:      Pure/PIDE/blob.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Unidentified text with markup.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -object Blob
    1.14 -{
    1.15 -  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
    1.16 -  {
    1.17 -    def + (info: Text.Markup): State = copy(markup = markup + info)
    1.18 -  }
    1.19 -}
    1.20 -
    1.21 -
    1.22 -sealed case class Blob(val source: String)
    1.23 -{
    1.24 -  def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.25 -
    1.26 -  lazy val symbol_index = new Symbol.Index(source)
    1.27 -  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
    1.28 -  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.29 -
    1.30 -  val init_state: Blob.State = Blob.State(this)
    1.31 -}
     2.1 --- a/src/Pure/PIDE/document.scala	Mon Oct 01 20:17:30 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon Oct 01 20:35:09 2012 +0200
     2.3 @@ -110,22 +110,18 @@
     2.4    final class Node private(
     2.5      val header: Node.Header = Node.bad_header("Bad theory header"),
     2.6      val perspective: Command.Perspective = Command.Perspective.empty,
     2.7 -    val blobs: Map[String, Blob] = Map.empty,
     2.8      val commands: Linear_Set[Command] = Linear_Set.empty)
     2.9    {
    2.10      def clear: Node = new Node(header = header)
    2.11  
    2.12      def update_header(new_header: Node.Header): Node =
    2.13 -      new Node(new_header, perspective, blobs, commands)
    2.14 +      new Node(new_header, perspective, commands)
    2.15  
    2.16      def update_perspective(new_perspective: Command.Perspective): Node =
    2.17 -      new Node(header, new_perspective, blobs, commands)
    2.18 -
    2.19 -    def update_blobs(new_blobs: Map[String, Blob]): Node =
    2.20 -      new Node(header, perspective, new_blobs, commands)
    2.21 +      new Node(header, new_perspective, commands)
    2.22  
    2.23      def update_commands(new_commands: Linear_Set[Command]): Node =
    2.24 -      new Node(header, perspective, blobs, new_commands)
    2.25 +      new Node(header, perspective, new_commands)
    2.26  
    2.27  
    2.28      /* commands */
     3.1 --- a/src/Pure/build-jars	Mon Oct 01 20:17:30 2012 +0200
     3.2 +++ b/src/Pure/build-jars	Mon Oct 01 20:35:09 2012 +0200
     3.3 @@ -30,7 +30,6 @@
     3.4    Isar/outer_syntax.scala
     3.5    Isar/parse.scala
     3.6    Isar/token.scala
     3.7 -  PIDE/blob.scala
     3.8    PIDE/command.scala
     3.9    PIDE/document.scala
    3.10    PIDE/isabelle_markup.scala