clarified modules;
authorwenzelm
Fri, 22 Dec 2017 14:27:59 +0100
changeset 67253 93b4333f33bb
parent 67252 c7f859868b7c
child 67254 31dd98471e88
clarified modules;
src/Pure/Thy/present.scala
src/Tools/VSCode/src/preview_panel.scala
src/Tools/jEdit/src/document_model.scala
--- a/src/Pure/Thy/present.scala	Fri Dec 22 13:51:20 2017 +0100
+++ b/src/Pure/Thy/present.scala	Fri Dec 22 14:27:59 2017 +0100
@@ -101,6 +101,28 @@
   }
 
 
+  /** preview **/
+
+  def preview(fonts_dir: String, snapshot: Document.Snapshot, plain: Boolean = false): String =
+  {
+    require(!snapshot.is_outdated)
+
+    val name = snapshot.node_name
+    if (name.is_bibtex && !plain) Bibtex.present(snapshot)
+    else {
+      val (heading, body) =
+        if (name.is_theory && !plain)
+          ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
+        else ("File " + quote(name.path.base_name), text_document(snapshot))
+
+      HTML.output_document(
+        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
+          HTML.title(heading)),
+          List(HTML.chapter(heading), HTML.source(body)))
+    }
+  }
+
+
   /* theory document */
 
   private val document_span_elements =
@@ -127,7 +149,7 @@
         XML.Text(Symbol.decode(text))
     }
 
-  def theory_document(snapshot: Document.Snapshot): XML.Body =
+  def pide_document(snapshot: Document.Snapshot): XML.Body =
     make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
 
 
--- a/src/Tools/VSCode/src/preview_panel.scala	Fri Dec 22 13:51:20 2017 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Dec 22 14:27:59 2017 +0100
@@ -47,7 +47,7 @@
     val content =
       HTML.output_document(
         List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)),
-        List(HTML.source(Present.theory_document(snapshot))),
+        List(HTML.source(Present.pide_document(snapshot))),
         css = "")
     (label, content)
   }
--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 13:51:20 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 14:27:59 2017 +0100
@@ -313,7 +313,10 @@
               { case (name, model)
                 if url_name == (if (name.is_theory) name.theory else name.node) => model })
         }
-        yield HTTP.Response.html(model.preview(fonts_root)))
+        yield {
+          val snapshot = model.await_stable_snapshot()
+          HTTP.Response.html(Present.preview(fonts_root, snapshot))
+        })
 
     List(HTTP.fonts(fonts_root), preview)
   }
@@ -321,29 +324,6 @@
 
 sealed abstract class Document_Model extends Document.Model
 {
-  /* content */
-
-  def bibtex_entries: List[Text.Info[String]]
-
-  def preview(fonts_dir: String): String =
-  {
-    val snapshot = await_stable_snapshot()
-
-    if (is_bibtex) Bibtex.present(snapshot)
-    else {
-      val (heading, body) =
-        if (is_theory)
-          ("Theory " + quote(node_name.theory_base_name), Present.theory_document(snapshot))
-        else ("File " + quote(node_name.path.base_name), Present.text_document(snapshot))
-
-      HTML.output_document(
-        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
-          HTML.title(heading)),
-          List(HTML.chapter(heading), HTML.source(body)))
-    }
-  }
-
-
   /* perspective */
 
   def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil