# 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) }