store full blob source for the sake of markup_to_XML;

--- a/src/Pure/PIDE/document.scala	Fri Dec 22 20:15:16 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 22 21:05:54 2017 +0100
@@ -45,7 +45,7 @@
 
   /* document blobs: auxiliary files */
 
-  sealed case class Blob(bytes: Bytes, chunk: Symbol.Text_Chunk, changed: Boolean)
+  sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean)
   {
     def unchanged: Blob = copy(changed = false)
   }
@@ -325,7 +325,7 @@
 
     def source: String =
       get_blob match {
-        case Some(blob) => blob.bytes.text
+        case Some(blob) => blob.source
         case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
       }
   }
@@ -836,7 +836,7 @@
         } yield tree).toList
       }
       else {
-        val node_source = Symbol.decode(node.source)  // FIXME treat mixed encode/decode situation
+        val node_source = node.source
         Text.Range(0, node_source.length).try_restrict(range) match {
           case None => Nil
           case Some(node_range) =>

--- a/src/Pure/Thy/present.scala	Fri Dec 22 20:15:16 2017 +0100
+++ b/src/Pure/Thy/present.scala	Fri Dec 22 21:05:54 2017 +0100
@@ -121,8 +121,7 @@
     val name = snapshot.node_name
     if (plain_text) {
       val title = "File " + quote(name.path.base_name)
-      val source = Symbol.decode(snapshot.node.source)  // FIXME treat mixed encode/decode situation
-      val content = output_document(title, HTML.text(source))
+      val content = output_document(title, HTML.text(snapshot.node.source))
       Preview(title, content)
     }
     else if (name.is_bibtex) {

--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 22 20:15:16 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 22 21:05:54 2017 +0100
@@ -143,7 +143,7 @@
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
-    else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)))
+    else Some((Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)))
 
 
   /* bibtex entries */

--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 20:15:16 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 21:05:54 2017 +0100
@@ -419,7 +419,7 @@
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
-    else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
+    else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
     if (is_bibtex) content.bibtex_entries else Nil
@@ -511,7 +511,7 @@
   /* blob */
 
   // owned by GUI thread
-  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None
+  private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
 
   private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
 
@@ -519,17 +519,19 @@
     GUI_Thread.require {
       if (is_theory) None
       else {
-        val (bytes, chunk) =
+        val (bytes, text, chunk) =
           _blob match {
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.make_file_content(buffer)
-              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
-              _blob = Some((bytes, chunk))
-              (bytes, chunk)
+              val text = buffer.getText(0, buffer.getLength)
+              val chunk = Symbol.Text_Chunk(text)
+              val x = (bytes, text, chunk)
+              _blob = Some(x)
+              x
           }
         val changed = pending_edits.nonEmpty
-        Some(Document.Blob(bytes, chunk, changed))
+        Some(Document.Blob(bytes, text, chunk, changed))
       }
     }