src/Pure/General/markup.scala
author wenzelm
Sun, 07 Sep 2008 17:48:50 +0200
changeset 28154 3c3663e24ba7
parent 27970 3dd5fbdf61c4
child 29140 e7ac5bb20aed
permissions -rw-r--r--
Default (mostly dummy) implementation of thread structures. formerly in multithreading.ML; create mutexes / condition variables without failure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/markup.scala
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     4
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     5
Common markup elements.
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     6
*/
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     7
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     8
package isabelle
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     9
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
    10
object Markup {
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    11
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    12
  /* position */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    13
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    14
  val LINE = "line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    15
  val COLUMN = "column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    16
  val OFFSET = "offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    17
  val END_LINE = "end_line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    18
  val END_COLUMN = "end_column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    19
  val END_OFFSET = "end_offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    20
  val FILE = "file"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    21
  val ID = "id"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    22
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    23
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    24
  /* messages */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    25
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    26
  val PID = "pid"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    27
  val SESSION = "session"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    28
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    29
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    30
  /* content */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    31
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
    32
  val ROOT = "root"
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
    33
  val RAW = "raw"
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    34
  val BAD = "bad"
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
    35
}