# HG changeset patch
# User wenzelm
# Date 1510489320 -3600
# Node ID 383b902fe2b9a7b8e19472d943eac3ba947a12ba
# Parent  9498b7522a99b58284ed9a761a20eb7449d8c596
tuned signature;

diff -r 9498b7522a99 -r 383b902fe2b9 src/Pure/Thy/thy_document_model.scala
--- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:19:00 2017 +0100
+++ b/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:22:00 2017 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/thy_document_model.scala
     Author:     Makarius
 
-Document model for theory files: no edits, no blobs, no overlays.
+Document model for theory files: no blobs, no edits, no overlays.
 */
 
 package isabelle
@@ -9,12 +9,12 @@
 
 object Thy_Document_Model
 {
-  def read_file(session: Session, path: Path,
-    qualifier: String = Sessions.DRAFT,
+  def read_file(session: Session,
+    node_name: Document.Node.Name,
     node_visible: Boolean = false,
     node_required: Boolean = false): Thy_Document_Model =
   {
-    val node_name = session.resources.thy_node_name(qualifier, path.file)
+    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, node_required)
   }