equal
deleted
inserted
replaced
80 case _ => status |
80 case _ => status |
81 } |
81 } |
82 |
82 |
83 def command_status(markups: List[Markup]): Status = |
83 def command_status(markups: List[Markup]): Status = |
84 (Status.init /: markups)(command_status(_, _)) |
84 (Status.init /: markups)(command_status(_, _)) |
|
85 |
|
86 |
|
87 /* command timing */ |
|
88 |
|
89 object Command_Timing |
|
90 { |
|
91 def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] = |
|
92 props match { |
|
93 case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args => |
|
94 (args, args) match { |
|
95 case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing)) |
|
96 case _ => None |
|
97 } |
|
98 case _ => None |
|
99 } |
|
100 } |
85 |
101 |
86 |
102 |
87 /* node status */ |
103 /* node status */ |
88 |
104 |
89 sealed case class Node_Status( |
105 sealed case class Node_Status( |