src/Tools/jEdit/src/document_model.scala
changeset 64680 7f87c1aa0ffa
parent 64673 b5965890e54d
child 64799 c0c648911f1a
equal deleted inserted replaced
64679:b2bf280b7e13 64680:7f87c1aa0ffa
    67 }
    67 }
    68 
    68 
    69 
    69 
    70 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
    70 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
    71 {
    71 {
       
    72   override def toString: String = node_name.toString
       
    73 
       
    74 
    72   /* header */
    75   /* header */
    73 
    76 
    74   def is_theory: Boolean = node_name.is_theory
    77   def is_theory: Boolean = node_name.is_theory
    75 
    78 
    76   def node_header(): Document.Node.Header =
    79   def node_header(): Document.Node.Header =