# HG changeset patch
# User wenzelm
# Date 1510502199 -3600
# Node ID 0d8e4e777973a5a90e58fdc6e6b0edee9018595b
# Parent  e35ae3eeec9360ccaaddbce54ed4475bc81636fd
theory nodes are never visible: avoid prints, which are not covered by node_consolidated;

diff -r e35ae3eeec93 -r 0d8e4e777973 src/Pure/Thy/thy_document_model.scala
--- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 16:38:13 2017 +0100
+++ b/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 16:56:39 2017 +0100
@@ -9,21 +9,18 @@
 
 object Thy_Document_Model
 {
-  def read_file(session: Session,
-    node_name: Document.Node.Name,
-    node_visible: Boolean = false): Thy_Document_Model =
+  def read_file(session: Session, node_name: Document.Node.Name): Thy_Document_Model =
   {
     val path = node_name.path
     if (!node_name.is_theory) error("Not a theory file: " + path)
-    new Thy_Document_Model(session, node_name, File.read(path), node_visible)
+    new Thy_Document_Model(session, node_name, File.read(path))
   }
 }
 
 final class Thy_Document_Model private(
   val session: Session,
   val node_name: Document.Node.Name,
-  val text: String,
-  val node_visible: Boolean) extends Document.Model
+  val text: String) extends Document.Model
 {
   /* content */
 
@@ -45,11 +42,8 @@
 
   /* perspective */
 
-  def text_perspective: Text.Perspective =
-    if (node_visible) Text.Perspective.full else Text.Perspective.empty
-
   def node_perspective: Document.Node.Perspective_Text =
-    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
+    Document.Node.Perspective(node_required, Text.Perspective.full, Document.Node.Overlays.empty)
 
 
   /* edits */
@@ -60,7 +54,7 @@
       if (old.isEmpty) Text.Edit.inserts(0, text)
       else Text.Edit.replace(0, old.get.text, text)
 
-    if (text_edits.isEmpty && old.isDefined && old.get.node_perspective == node_perspective) Nil
+    if (text_edits.isEmpty) Nil
     else node_edits(node_header, text_edits, node_perspective)
   }
 
diff -r e35ae3eeec93 -r 0d8e4e777973 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 16:38:13 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 16:56:39 2017 +0100
@@ -29,7 +29,6 @@
   def load_theories(
     session: Session,
     theories: List[(String, Position.T)],
-    visible: Boolean = false,
     qualifier: String = Sessions.DRAFT,
     master_dir: String = ""): List[Document.Node.Name] =
   {
@@ -38,10 +37,7 @@
       yield (import_name(qualifier, master_dir, thy), pos)
 
     val dependencies = resources.dependencies(import_names).check_errors
-
-    val loaded_models =
-      dependencies.names.map(name =>
-        Thy_Document_Model.read_file(session, name, visible && import_names.contains(name)))
+    val loaded_models = dependencies.names.map(Thy_Document_Model.read_file(session, _))
 
     val edits =
       state.change_result(st =>
@@ -56,7 +52,6 @@
         val st1 = st.update_models(model_edits.map(_._1))
         (model_edits.flatMap(_._2), st1)
       })
-
     session.update(Document.Blobs.empty, edits)
 
     dependencies.names