src/Pure/PIDE/blob.scala
author wenzelm
Wed, 04 Apr 2012 14:19:47 +0200
changeset 47336 bed4b2738d8a
parent 45455 4f974c0c5c2f
child 49414 d7b5fb2e9ca2
permissions -rw-r--r--
separate module for prover command execution;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43715
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/blob.scala
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     3
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     4
Unidentified text with markup.
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     5
*/
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     6
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     7
package isabelle
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     8
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
     9
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    10
object Blob
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    11
{
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    12
  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    13
  {
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 43715
diff changeset
    14
    def + (info: Text.Markup): State = copy(markup = markup + info)
43715
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    15
  }
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    16
}
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    17
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    18
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    19
sealed case class Blob(val source: String)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    20
{
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    21
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    22
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    23
  lazy val symbol_index = new Symbol.Index(source)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    24
  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    25
  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    26
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    27
  val empty_state: Blob.State = Blob.State(this)
518e44a0ee15 some support for blobs (arbitrary text files) within document nodes;
wenzelm
parents:
diff changeset
    28
}