equal
deleted
inserted
replaced
491 } |
491 } |
492 |
492 |
493 val PRINT_OPERATIONS = "print_operations" |
493 val PRINT_OPERATIONS = "print_operations" |
494 |
494 |
495 |
495 |
|
496 /* debugger output */ |
|
497 |
|
498 val DEBUGGER_OUTPUT = "debugger_output" |
|
499 object Debugger_Output |
|
500 { |
|
501 def unapply(props: Properties.T): Option[(String, Long)] = |
|
502 props match { |
|
503 case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) => |
|
504 Some((name, i)) |
|
505 case _ => None |
|
506 } |
|
507 } |
|
508 |
|
509 |
496 /* simplifier trace */ |
510 /* simplifier trace */ |
497 |
511 |
498 val SIMP_TRACE_PANEL = "simp_trace_panel" |
512 val SIMP_TRACE_PANEL = "simp_trace_panel" |
499 |
513 |
500 val SIMP_TRACE_LOG = "simp_trace_log" |
514 val SIMP_TRACE_LOG = "simp_trace_log" |