equal
deleted
inserted
replaced
58 }).toList |
58 }).toList |
59 } |
59 } |
60 |
60 |
61 def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = |
61 def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = |
62 Document_Model(session, editor, node_name, Content.empty, |
62 Document_Model(session, editor, node_name, Content.empty, |
63 node_required = session.resources.file_formats.is_theory(node_name)) |
63 node_required = File_Format.registry.is_theory(node_name)) |
64 } |
64 } |
65 |
65 |
66 sealed case class Document_Model( |
66 sealed case class Document_Model( |
67 session: Session, |
67 session: Session, |
68 editor: Server.Editor, |
68 editor: Server.Editor, |