src/Pure/PIDE/blob.scala
changeset 49414 d7b5fb2e9ca2
parent 45455 4f974c0c5c2f
--- a/src/Pure/PIDE/blob.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/PIDE/blob.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -24,5 +24,5 @@
   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)
+  val init_state: Blob.State = Blob.State(this)
 }