src/Pure/Tools/print_operation.scala
changeset 71601 97ccf48c2f0c
parent 65344 b99283eed13c
child 72155 837b86b214d3
equal deleted inserted replaced
71600:64aad1e46f98 71601:97ccf48c2f0c
    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     val functions = List(Markup.PRINT_OPERATIONS -> put)
    42   }
    42   }
    43 }
    43 }