src/Pure/name.scala
author wenzelm
Sun, 06 Oct 2024 18:34:35 +0200
changeset 81121 7cacedbddba7
parent 80272 9f89b3c41460
permissions -rw-r--r--
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup; effectively revert 2cb4a2970941 and unify pretty-printing in Scala and ML, following Scala before that change; build error messages are properly formatted again (amending 320bcbf34849): "no_report" markup does not affect its enclosed line break anymore;

/*  Title:      Pure/name.scala
    Author:     Makarius

Items with formal name.
*/

package isabelle


object Name {
  trait T { def name: String }

  type Data[A] = Map[String, A]
}