5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Line_Structure |
10 object Line_Structure { |
11 { |
|
12 val init: Line_Structure = Line_Structure() |
11 val init: Line_Structure = Line_Structure() |
13 } |
12 } |
14 |
13 |
15 sealed case class Line_Structure( |
14 sealed case class Line_Structure( |
16 improper: Boolean = true, |
15 improper: Boolean = true, |
17 blank: Boolean = true, |
16 blank: Boolean = true, |
18 command: Boolean = false, |
17 command: Boolean = false, |
19 depth: Int = 0, |
18 depth: Int = 0, |
20 span_depth: Int = 0, |
19 span_depth: Int = 0, |
21 after_span_depth: Int = 0, |
20 after_span_depth: Int = 0, |
22 element_depth: Int = 0) |
21 element_depth: Int = 0 |
23 { |
22 ) { |
24 def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure = |
23 def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure = { |
25 { |
|
26 val improper1 = tokens.forall(tok => !tok.is_proper) |
24 val improper1 = tokens.forall(tok => !tok.is_proper) |
27 val blank1 = tokens.forall(_.is_space) |
25 val blank1 = tokens.forall(_.is_space) |
28 val command1 = tokens.exists(_.is_begin_or_command) |
26 val command1 = tokens.exists(_.is_begin_or_command) |
29 |
27 |
30 val command_depth = |
28 val command_depth = |