theory nodes are never visible: avoid prints, which are not covered by node_consolidated;
--- 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)
}
--- 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