equal
deleted
inserted
replaced
128 |
128 |
129 |
129 |
130 /** document model **/ |
130 /** document model **/ |
131 |
131 |
132 def check_name(name: String): Boolean = name.endsWith(".bib") |
132 def check_name(name: String): Boolean = name.endsWith(".bib") |
133 def check_name(name: Document.Node.Name): Boolean = check_name(name.node) |
|
134 |
133 |
135 def entries(text: String): List[Text.Info[String]] = |
134 def entries(text: String): List[Text.Info[String]] = |
136 { |
135 { |
137 val result = new mutable.ListBuffer[Text.Info[String]] |
136 val result = new mutable.ListBuffer[Text.Info[String]] |
138 var offset = 0 |
137 var offset = 0 |