equal
deleted
inserted
replaced
136 } |
136 } |
137 |
137 |
138 |
138 |
139 /* blob */ |
139 /* blob */ |
140 |
140 |
141 private var _blob: Option[(Bytes, Command.Chunk.File)] = None // owned by Swing thread |
141 private var _blob: Option[(Bytes, Text.Chunk.File)] = None // owned by Swing thread |
142 |
142 |
143 private def reset_blob(): Unit = Swing_Thread.require { _blob = None } |
143 private def reset_blob(): Unit = Swing_Thread.require { _blob = None } |
144 |
144 |
145 def get_blob(): Option[Document.Blob] = |
145 def get_blob(): Option[Document.Blob] = |
146 Swing_Thread.require { |
146 Swing_Thread.require { |
149 val (bytes, file) = |
149 val (bytes, file) = |
150 _blob match { |
150 _blob match { |
151 case Some(x) => x |
151 case Some(x) => x |
152 case None => |
152 case None => |
153 val bytes = PIDE.resources.file_content(buffer) |
153 val bytes = PIDE.resources.file_content(buffer) |
154 val file = |
154 val file = new Text.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength)) |
155 new Command.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength)) |
|
156 _blob = Some((bytes, file)) |
155 _blob = Some((bytes, file)) |
157 (bytes, file) |
156 (bytes, file) |
158 } |
157 } |
159 val changed = pending_edits.is_pending() |
158 val changed = pending_edits.is_pending() |
160 Some(Document.Blob(bytes, file, changed)) |
159 Some(Document.Blob(bytes, file, changed)) |