49 |
49 |
50 sealed case class Theory( |
50 sealed case class Theory( |
51 theory: String, |
51 theory: String, |
52 session: String = "", |
52 session: String = "", |
53 percentage: Option[Int] = None, |
53 percentage: Option[Int] = None, |
54 total_time: Time = Time.zero, |
54 cumulated_time: Time = Time.zero, |
55 override val verbose: Boolean = true, |
55 override val verbose: Boolean = true, |
56 override val status: Boolean = false |
56 override val status: Boolean = false |
57 ) extends Msg { |
57 ) extends Msg { |
58 override def message: Message = |
58 override def message: Message = |
59 Message(Kind.writeln, print_session + print_theory + print_percentage + print_total_time, |
59 Message(Kind.writeln, print_session + print_theory + print_percentage + print_cumulated_time, |
60 verbose = verbose, status = status) |
60 verbose = verbose, status = status) |
61 |
61 |
62 def print_session: String = if_proper(session, session + ": ") |
62 def print_session: String = if_proper(session, session + ": ") |
63 def print_theory: String = "theory " + theory |
63 def print_theory: String = "theory " + theory |
64 def print_percentage: String = |
64 def print_percentage: String = |
65 percentage match { case None => "" case Some(p) => " " + p + "%" } |
65 percentage match { case None => "" case Some(p) => " " + p + "%" } |
66 def print_total_time: String = |
66 def print_cumulated_time: String = |
67 if (total_time.is_relevant) " (" + total_time.message + " elapsed time)" else "" |
67 if (cumulated_time.is_relevant) " (" + cumulated_time.message + " cumulated time)" else "" |
68 } |
68 } |
69 |
69 |
70 sealed case class Nodes_Status( |
70 sealed case class Nodes_Status( |
71 domain: List[Document.Node.Name], |
71 domain: List[Document.Node.Name], |
72 document_status: Document_Status.Nodes_Status, |
72 document_status: Document_Status.Nodes_Status, |
78 |
78 |
79 def theory(name: Document.Node.Name): Theory = { |
79 def theory(name: Document.Node.Name): Theory = { |
80 val node_status = apply(name) |
80 val node_status = apply(name) |
81 Theory(theory = name.theory, session = session, |
81 Theory(theory = name.theory, session = session, |
82 percentage = Some(node_status.percentage), |
82 percentage = Some(node_status.percentage), |
83 total_time = node_status.total_timing.elapsed) |
83 cumulated_time = node_status.cumulated_time) |
84 } |
84 } |
85 |
85 |
86 def theory_progress(name: Document.Node.Name, check: (Int, Int) => Boolean): Option[Theory] = { |
86 def theory_progress(name: Document.Node.Name, check: (Int, Int) => Boolean): Option[Theory] = { |
87 val thy = theory(name) |
87 val thy = theory(name) |
88 val thy_percentage = thy.percentage.getOrElse(0) |
88 val thy_percentage = thy.percentage.getOrElse(0) |