author | wenzelm |
Sat, 23 Aug 2008 23:07:39 +0200 | |
changeset 27970 | 3dd5fbdf61c4 |
parent 27958 | 292d78c906b1 |
child 29140 | e7ac5bb20aed |
permissions | -rw-r--r-- |
/* Title: Pure/General/markup.scala ID: $Id$ Author: Makarius Common markup elements. */ package isabelle object Markup { /* position */ val LINE = "line" val COLUMN = "column" val OFFSET = "offset" val END_LINE = "end_line" val END_COLUMN = "end_column" val END_OFFSET = "end_offset" val FILE = "file" val ID = "id" /* messages */ val PID = "pid" val SESSION = "session" /* content */ val ROOT = "root" val RAW = "raw" val BAD = "bad" }