equal
deleted
inserted
replaced
21 after_span_depth: Int = 0, |
21 after_span_depth: Int = 0, |
22 element_depth: Int = 0) |
22 element_depth: Int = 0) |
23 { |
23 { |
24 def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure = |
24 def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure = |
25 { |
25 { |
26 val improper1 = tokens.forall(_.is_improper) |
26 val improper1 = tokens.forall(tok => !tok.is_proper) |
27 val blank1 = tokens.forall(_.is_space) |
27 val blank1 = tokens.forall(_.is_space) |
28 val command1 = tokens.exists(_.is_begin_or_command) |
28 val command1 = tokens.exists(_.is_begin_or_command) |
29 |
29 |
30 val command_depth = |
30 val command_depth = |
31 tokens.iterator.filter(_.is_proper).toStream.headOption match { |
31 tokens.iterator.filter(_.is_proper).toStream.headOption match { |