equal
deleted
inserted
replaced
469 } |
469 } |
470 |
470 |
471 val BUILD_THEORIES_RESULT = "build_theories_result" |
471 val BUILD_THEORIES_RESULT = "build_theories_result" |
472 object Build_Theories_Result |
472 object Build_Theories_Result |
473 { |
473 { |
474 def unapply(props: Properties.T): Option[(String, Boolean)] = |
474 def unapply(props: Properties.T): Option[String] = |
475 props match { |
475 props match { |
476 case List((FUNCTION, BUILD_THEORIES_RESULT), |
476 case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id) |
477 ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok)) |
|
478 case _ => None |
477 case _ => None |
479 } |
478 } |
480 } |
479 } |
481 |
480 |
482 val PRINT_OPERATIONS = "print_operations" |
481 val PRINT_OPERATIONS = "print_operations" |