src/Pure/General/markup.scala
author wenzelm
Sat Aug 23 23:07:39 2008 +0200 (2008-08-23 ago)
changeset 27970 3dd5fbdf61c4
parent 27958 292d78c906b1
child 29140 e7ac5bb20aed
permissions -rw-r--r--
added position, messages;
renamed messages to content, malformed to bad;
wenzelm@27958
     1
/*  Title:      Pure/General/markup.scala
wenzelm@27958
     2
    ID:         $Id$
wenzelm@27958
     3
    Author:     Makarius
wenzelm@27958
     4
wenzelm@27958
     5
Common markup elements.
wenzelm@27958
     6
*/
wenzelm@27958
     7
wenzelm@27958
     8
package isabelle
wenzelm@27958
     9
wenzelm@27958
    10
object Markup {
wenzelm@27970
    11
wenzelm@27970
    12
  /* position */
wenzelm@27970
    13
wenzelm@27970
    14
  val LINE = "line"
wenzelm@27970
    15
  val COLUMN = "column"
wenzelm@27970
    16
  val OFFSET = "offset"
wenzelm@27970
    17
  val END_LINE = "end_line"
wenzelm@27970
    18
  val END_COLUMN = "end_column"
wenzelm@27970
    19
  val END_OFFSET = "end_offset"
wenzelm@27970
    20
  val FILE = "file"
wenzelm@27970
    21
  val ID = "id"
wenzelm@27970
    22
wenzelm@27970
    23
wenzelm@27970
    24
  /* messages */
wenzelm@27970
    25
wenzelm@27970
    26
  val PID = "pid"
wenzelm@27970
    27
  val SESSION = "session"
wenzelm@27970
    28
wenzelm@27970
    29
wenzelm@27970
    30
  /* content */
wenzelm@27970
    31
wenzelm@27958
    32
  val ROOT = "root"
wenzelm@27958
    33
  val RAW = "raw"
wenzelm@27970
    34
  val BAD = "bad"
wenzelm@27958
    35
}