src/Pure/Tools/print_operation.scala
changeset 72212 53e8858b839f
parent 72155 837b86b214d3
child 72215 8f9cffa78112
equal deleted inserted replaced
72211:a6cbf8ce979e 72212:53e8858b839f
    36       }
    36       }
    37       print_operations.change(_ => ops)
    37       print_operations.change(_ => ops)
    38       true
    38       true
    39     }
    39     }
    40 
    40 
    41     val functions = List(Markup.PRINT_OPERATIONS -> put)
    41     override val functions = List(Markup.PRINT_OPERATIONS -> put)
    42   }
    42   }
    43 }
    43 }