1 /* Title: Pure/Thy/thy_document_model.scala |
1 /* Title: Pure/Thy/thy_document_model.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Document model for theory files: no edits, no blobs, no overlays. |
4 Document model for theory files: no blobs, no edits, no overlays. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Thy_Document_Model |
10 object Thy_Document_Model |
11 { |
11 { |
12 def read_file(session: Session, path: Path, |
12 def read_file(session: Session, |
13 qualifier: String = Sessions.DRAFT, |
13 node_name: Document.Node.Name, |
14 node_visible: Boolean = false, |
14 node_visible: Boolean = false, |
15 node_required: Boolean = false): Thy_Document_Model = |
15 node_required: Boolean = false): Thy_Document_Model = |
16 { |
16 { |
17 val node_name = session.resources.thy_node_name(qualifier, path.file) |
17 val path = node_name.path |
18 if (!node_name.is_theory) error("Not a theory file: " + path) |
18 if (!node_name.is_theory) error("Not a theory file: " + path) |
19 new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required) |
19 new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required) |
20 } |
20 } |
21 } |
21 } |
22 |
22 |