| author | blanchet | 
| Tue, 14 Aug 2012 16:09:45 +0200 | |
| changeset 48803 | ffa31bf5c662 | 
| parent 45455 | 4f974c0c5c2f | 
| child 49414 | d7b5fb2e9ca2 | 
| permissions | -rw-r--r-- | 
| 
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 | 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  | 
}  |