# HG changeset patch
# User wenzelm
# Date 1513970116 -3600
# Node ID 16f74b7c248a6a7a1eafc03e8dfc6a2d217d47bf
# Parent  449a989f42cd8327c3bcfb77ed634289c7f70af9
PIDE markup for non-theory nodes;

diff -r 449a989f42cd -r 16f74b7c248a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 22 18:32:59 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 22 20:15:16 2017 +0100
@@ -821,17 +821,36 @@
 
     def markup_to_XML(
       version: Version,
-      node: Node,
+      node_name: Node.Name,
       range: Text.Range,
       elements: Markup.Elements): XML.Body =
     {
-      (for {
-        command <- node.commands.iterator
-        command_range <- command.range.try_restrict(range).iterator
-        markup =
-          command_markup(version, command, Command.Markup_Index.markup, command_range, elements)
-        tree <- markup.to_XML(command_range, command.source, elements).iterator
-      } yield tree).toList
+      val node = version.nodes(node_name)
+      if (node_name.is_theory) {
+        val markup_index = Command.Markup_Index.markup
+        (for {
+          command <- node.commands.iterator
+          command_range <- command.range.try_restrict(range).iterator
+          markup = command_markup(version, command, markup_index, command_range, elements)
+          tree <- markup.to_XML(command_range, command.source, elements).iterator
+        } yield tree).toList
+      }
+      else {
+        val node_source = Symbol.decode(node.source)  // FIXME treat mixed encode/decode situation
+        Text.Range(0, node_source.length).try_restrict(range) match {
+          case None => Nil
+          case Some(node_range) =>
+            val markup =
+              version.nodes.commands_loading(node_name).headOption match {
+                case None => Markup_Tree.empty
+                case Some(command) =>
+                  val chunk_name = Symbol.Text_Chunk.File(node_name.node)
+                  val markup_index = Command.Markup_Index(false, chunk_name)
+                  command_markup(version, command, markup_index, node_range, elements)
+              }
+            markup.to_XML(node_range, node_source, elements)
+        }
+      }
     }
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
@@ -910,7 +929,7 @@
           else version.nodes.commands_loading(other_node_name).headOption
 
         def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
-          state.markup_to_XML(version, node, range, elements)
+          state.markup_to_XML(version, node_name, range, elements)
 
 
         /* find command */
diff -r 449a989f42cd -r 16f74b7c248a src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Fri Dec 22 18:32:59 2017 +0100
+++ b/src/Pure/Thy/present.scala	Fri Dec 22 20:15:16 2017 +0100
@@ -111,8 +111,21 @@
   {
     require(!snapshot.is_outdated)
 
+    def output_document(title: String, body: XML.Body): String =
+      HTML.output_document(
+        List(
+          HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
+          HTML.title(title)),
+        List(HTML.source(body)), css = "")
+
     val name = snapshot.node_name
-    if (name.is_bibtex && !plain_text) {
+    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))
+      Preview(title, content)
+    }
+    else if (name.is_bibtex) {
       val title = "Bibliography " + quote(name.path.base_name)
       val content =
         Isabelle_System.with_tmp_file("bib", "bib") { bib =>
@@ -122,22 +135,16 @@
       Preview(title, content)
     }
     else {
-      val (title, body) =
-        if (name.is_theory && !plain_text)
-          ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
-        else ("File " + quote(name.path.base_name), text_document(snapshot))
-
-      val content =
-        HTML.output_document(
-          List(HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
-            HTML.title(title)), List(HTML.source(body)), css = "")
-
+      val title =
+        if (name.is_theory) "Theory " + quote(name.theory_base_name)
+        else "File " + quote(name.path.base_name)
+      val content = output_document(title, pide_document(snapshot))
       Preview(title, content)
     }
   }
 
 
-  /* theory document */
+  /* PIDE document */
 
   private val document_span_elements =
     Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT
@@ -167,15 +174,6 @@
     make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
 
 
-  /* text document */
-
-  def text_document(snapshot: Document.Snapshot): XML.Body =
-    snapshot.node.source match {
-      case "" => Nil
-      case txt => List(XML.Text(Symbol.decode(txt)))
-    }
-
-
 
   /** build document **/