src/Pure/General/markup.scala
author wenzelm
Thu, 06 May 2010 16:27:47 +0200
changeset 36683 41a1210519fd
parent 34242 5ccdc8bf3849
child 36689 379f5b1e7f91
permissions -rw-r--r--
basic support for symbolic pretty printing; tuned;
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
    Author:     Makarius
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     3
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     4
Common markup elements.
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     5
*/
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     6
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     7
package isabelle
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     8
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
     9
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    10
object Markup
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    11
{
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    12
  /* property values */
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    13
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    14
  def get_string(name: String, props: List[(String, String)]): Option[String] =
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    15
    props.find(p => p._1 == name).map(_._2)
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    16
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    17
  def parse_int(s: String): Option[Int] =
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    18
    try { Some(Integer.parseInt(s)) }
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    19
    catch { case _: NumberFormatException => None }
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    20
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    21
  def get_int(name: String, props: List[(String, String)]): Option[Int] =
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    22
  {
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    23
    get_string(name, props) match {
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    24
      case None => None
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    25
      case Some(value) => parse_int(value)
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    26
    }
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    27
  }
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    28
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    29
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    30
  /* name */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    31
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    32
  val NAME = "name"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    33
  val KIND = "kind"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    34
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    35
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    36
  /* formal entities */
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    37
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    38
  val ENTITY = "entity"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    39
  val DEF = "def"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    40
  val REF = "ref"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    41
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    42
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    43
  /* position */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    44
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    45
  val LINE = "line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    46
  val COLUMN = "column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    47
  val OFFSET = "offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    48
  val END_LINE = "end_line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    49
  val END_COLUMN = "end_column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    50
  val END_OFFSET = "end_offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    51
  val FILE = "file"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    52
  val ID = "id"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    53
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    54
  val POSITION_PROPERTIES =
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    55
    Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
29205
7dc7a75033ea added POSITION_PROPERTIES;
wenzelm
parents: 29195
diff changeset
    56
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    57
  val POSITION = "position"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    58
  val LOCATION = "location"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    59
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    60
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    61
  /* pretty printing */
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    62
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    63
  val INDENT = "indent"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    64
  val BLOCK = "block"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    65
  val WIDTH = "width"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    66
  val BREAK = "break"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    67
  val FBREAK = "fbreak"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    68
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    69
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    70
  /* hidden text */
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    71
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    72
  val HIDDEN = "hidden"
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    73
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    74
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    75
  /* logical entities */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    76
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    77
  val TCLASS = "tclass"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    78
  val TYCON = "tycon"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    79
  val FIXED_DECL = "fixed_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    80
  val FIXED = "fixed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    81
  val CONST_DECL = "const_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    82
  val CONST = "const"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    83
  val FACT_DECL = "fact_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    84
  val FACT = "fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    85
  val DYNAMIC_FACT = "dynamic_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    86
  val LOCAL_FACT_DECL = "local_fact_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    87
  val LOCAL_FACT = "local_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    88
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    89
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    90
  /* inner syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    91
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    92
  val TFREE = "tfree"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    93
  val TVAR = "tvar"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    94
  val FREE = "free"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    95
  val SKOLEM = "skolem"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    96
  val BOUND = "bound"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    97
  val VAR = "var"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    98
  val NUM = "num"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    99
  val FLOAT = "float"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   100
  val XNUM = "xnum"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   101
  val XSTR = "xstr"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   102
  val LITERAL = "literal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   103
  val INNER_COMMENT = "inner_comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   104
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   105
  val SORT = "sort"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   106
  val TYP = "typ"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   107
  val TERM = "term"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   108
  val PROP = "prop"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   109
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   110
  val ATTRIBUTE = "attribute"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   111
  val METHOD = "method"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   112
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   113
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   114
  /* embedded source text */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   115
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   116
  val ML_SOURCE = "ML_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   117
  val DOC_SOURCE = "doc_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   118
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   119
  val ANTIQ = "antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   120
  val ML_ANTIQ = "ML_antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   121
  val DOC_ANTIQ = "doc_antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   122
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   123
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   124
  /* ML syntax */
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   125
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   126
  val ML_KEYWORD = "ML_keyword"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   127
  val ML_IDENT = "ML_ident"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   128
  val ML_TVAR = "ML_tvar"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   129
  val ML_NUMERAL = "ML_numeral"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   130
  val ML_CHAR = "ML_char"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   131
  val ML_STRING = "ML_string"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   132
  val ML_COMMENT = "ML_comment"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   133
  val ML_MALFORMED = "ML_malformed"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   134
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   135
  val ML_DEF = "ML_def"
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   136
  val ML_OPEN = "ML_open"
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   137
  val ML_STRUCT = "ML_struct"
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   138
  val ML_REF = "ML_ref"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   139
  val ML_TYPING = "ML_typing"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   140
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   141
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   142
  /* outer syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   143
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   144
  val KEYWORD_DECL = "keyword_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   145
  val COMMAND_DECL = "command_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   146
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   147
  val KEYWORD = "keyword"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   148
  val COMMAND = "command"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   149
  val IDENT = "ident"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   150
  val STRING = "string"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   151
  val ALTSTRING = "altstring"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   152
  val VERBATIM = "verbatim"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   153
  val COMMENT = "comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   154
  val CONTROL = "control"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   155
  val MALFORMED = "malformed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   156
29185
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   157
  val COMMAND_SPAN = "command_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   158
  val IGNORED_SPAN = "ignored_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   159
  val MALFORMED_SPAN = "malformed_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   160
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   161
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   162
  /* toplevel */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   163
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   164
  val STATE = "state"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   165
  val SUBGOAL = "subgoal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   166
  val SENDBACK = "sendback"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   167
  val HILITE = "hilite"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   168
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   169
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   170
  /* command status */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   171
29417
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   172
  val TASK = "task"
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   173
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   174
  val UNPROCESSED = "unprocessed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   175
  val RUNNING = "running"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   176
  val FAILED = "failed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   177
  val FINISHED = "finished"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   178
  val DISPOSED = "disposed"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   179
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   180
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   181
  /* interactive documents */
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   182
34242
5ccdc8bf3849 explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
wenzelm
parents: 34214
diff changeset
   183
  val ASSIGN = "assign"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   184
  val EDIT = "edit"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   185
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   186
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   187
  /* messages */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   188
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   189
  val PID = "pid"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   190
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   191
  val MESSAGE = "message"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   192
  val CLASS = "class"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   193
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   194
  val INIT = "init"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   195
  val STATUS = "status"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   196
  val WRITELN = "writeln"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   197
  val PRIORITY = "priority"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   198
  val TRACING = "tracing"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   199
  val WARNING = "warning"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   200
  val ERROR = "error"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   201
  val DEBUG = "debug"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   202
  val SYSTEM = "system"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   203
  val STDIN = "stdin"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   204
  val STDOUT = "stdout"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   205
  val SIGNAL = "signal"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   206
  val EXIT = "exit"
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   207
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   208
  val READY = "ready"
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   209
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   210
34119
ae92efb48784 markup bad YXML as malformed;
wenzelm
parents: 34046
diff changeset
   211
  /* system data */
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   212
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 33985
diff changeset
   213
  val DATA = "data"
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
   214
}