tuned signature;
authorwenzelm
Sun Nov 12 13:22:00 2017 +0100 (12 months ago)
changeset 67055383b902fe2b9
parent 67054 9498b7522a99
child 67056 e35ae3eeec93
tuned signature;
src/Pure/Thy/thy_document_model.scala
     1.1 --- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:19:00 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:22:00 2017 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Thy/thy_document_model.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Document model for theory files: no edits, no blobs, no overlays.
     1.8 +Document model for theory files: no blobs, no edits, no overlays.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -9,12 +9,12 @@
    1.13  
    1.14  object Thy_Document_Model
    1.15  {
    1.16 -  def read_file(session: Session, path: Path,
    1.17 -    qualifier: String = Sessions.DRAFT,
    1.18 +  def read_file(session: Session,
    1.19 +    node_name: Document.Node.Name,
    1.20      node_visible: Boolean = false,
    1.21      node_required: Boolean = false): Thy_Document_Model =
    1.22    {
    1.23 -    val node_name = session.resources.thy_node_name(qualifier, path.file)
    1.24 +    val path = node_name.path
    1.25      if (!node_name.is_theory) error("Not a theory file: " + path)
    1.26      new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
    1.27    }