src/Pure/General/markup.scala
author wenzelm
Wed, 25 Aug 2010 22:37:53 +0200
changeset 38722 ba31936497c2
parent 38721 ca8b14fa0d0d
child 38724 d1feec02cf02
permissions -rw-r--r--
organized markup properties via apply/unapply patterns;
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
{
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    12
  /* plain values */
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    13
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    14
  object Int {
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    15
    def apply(i: scala.Int): String = i.toString
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    16
    def unapply(s: String): Option[scala.Int] =
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    17
      try { Some(Integer.parseInt(s)) }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    18
      catch { case _: NumberFormatException => None }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    19
  }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    20
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    21
  object Long {
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    22
    def apply(i: scala.Long): String = i.toString
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    23
    def unapply(s: String): Option[scala.Long] =
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    24
      try { Some(java.lang.Long.parseLong(s)) }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    25
      catch { case _: NumberFormatException => None }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    26
  }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    27
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    28
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    29
  /* named properties */
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    30
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    31
  class Property(val name: String)
38355
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38259
diff changeset
    32
  {
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    33
    def apply(value: String): List[(String, String)] = List((name, value))
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    34
    def unapply(props: List[(String, String)]): Option[String] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    35
      props.find(_._1 == name).map(_._2)
38355
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38259
diff changeset
    36
  }
8cb265fb12fe represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents: 38259
diff changeset
    37
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    38
  class Int_Property(name: String)
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    39
  {
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    40
    def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    41
    def unapply(props: List[(String, String)]): Option[Int] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    42
      props.find(_._1 == name) match {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    43
        case None => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    44
        case Some((_, value)) => Int.unapply(value)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    45
      }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    46
  }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    47
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    48
  class Long_Property(name: String)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    49
  {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    50
    def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    51
    def unapply(props: List[(String, String)]): Option[Long] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    52
      props.find(_._1 == name) match {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    53
        case None => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    54
        case Some((_, value)) => Long.unapply(value)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    55
      }
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    56
  }
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    57
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    58
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    59
  /* empty */
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    60
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    61
  val Empty = Markup("", Nil)
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    62
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    63
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
    64
  /* misc properties */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    65
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    66
  val NAME = "name"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    67
  val KIND = "kind"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    68
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    69
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    70
  /* formal entities */
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    71
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    72
  val ENTITY = "entity"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    73
  val DEF = "def"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    74
  val REF = "ref"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    75
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    76
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    77
  /* position */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    78
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    79
  val LINE = "line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    80
  val COLUMN = "column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    81
  val OFFSET = "offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    82
  val END_LINE = "end_line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    83
  val END_COLUMN = "end_column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    84
  val END_OFFSET = "end_offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    85
  val FILE = "file"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    86
  val ID = "id"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    87
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    88
  val POSITION_PROPERTIES =
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    89
    Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
29205
7dc7a75033ea added POSITION_PROPERTIES;
wenzelm
parents: 29195
diff changeset
    90
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    91
  val POSITION = "position"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    92
  val LOCATION = "location"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    93
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    94
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    95
  /* pretty printing */
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    96
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    97
  val INDENT = "indent"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    98
  val BLOCK = "block"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    99
  val WIDTH = "width"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   100
  val BREAK = "break"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   101
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   102
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   103
  /* hidden text */
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   104
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   105
  val HIDDEN = "hidden"
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   106
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   107
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   108
  /* logical entities */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   109
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   110
  val TCLASS = "tclass"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   111
  val TYCON = "tycon"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   112
  val FIXED_DECL = "fixed_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   113
  val FIXED = "fixed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   114
  val CONST_DECL = "const_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   115
  val CONST = "const"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   116
  val FACT_DECL = "fact_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   117
  val FACT = "fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   118
  val DYNAMIC_FACT = "dynamic_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   119
  val LOCAL_FACT_DECL = "local_fact_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   120
  val LOCAL_FACT = "local_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   121
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   122
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   123
  /* inner syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   124
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   125
  val TFREE = "tfree"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   126
  val TVAR = "tvar"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   127
  val FREE = "free"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   128
  val SKOLEM = "skolem"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   129
  val BOUND = "bound"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   130
  val VAR = "var"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   131
  val NUM = "num"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   132
  val FLOAT = "float"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   133
  val XNUM = "xnum"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   134
  val XSTR = "xstr"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   135
  val LITERAL = "literal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   136
  val INNER_COMMENT = "inner_comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   137
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   138
  val SORT = "sort"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   139
  val TYP = "typ"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   140
  val TERM = "term"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   141
  val PROP = "prop"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   142
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   143
  val ATTRIBUTE = "attribute"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   144
  val METHOD = "method"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   145
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   146
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   147
  /* embedded source text */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   148
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   149
  val ML_SOURCE = "ML_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   150
  val DOC_SOURCE = "doc_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   151
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   152
  val ANTIQ = "antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   153
  val ML_ANTIQ = "ML_antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   154
  val DOC_ANTIQ = "doc_antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   155
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   156
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   157
  /* ML syntax */
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   158
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   159
  val ML_KEYWORD = "ML_keyword"
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 37194
diff changeset
   160
  val ML_DELIMITER = "ML_delimiter"
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   161
  val ML_IDENT = "ML_ident"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   162
  val ML_TVAR = "ML_tvar"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   163
  val ML_NUMERAL = "ML_numeral"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   164
  val ML_CHAR = "ML_char"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   165
  val ML_STRING = "ML_string"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   166
  val ML_COMMENT = "ML_comment"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   167
  val ML_MALFORMED = "ML_malformed"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   168
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   169
  val ML_DEF = "ML_def"
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   170
  val ML_OPEN = "ML_open"
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   171
  val ML_STRUCT = "ML_struct"
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   172
  val ML_REF = "ML_ref"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   173
  val ML_TYPING = "ML_typing"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   174
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   175
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   176
  /* outer syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   177
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   178
  val KEYWORD_DECL = "keyword_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   179
  val COMMAND_DECL = "command_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   180
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   181
  val KEYWORD = "keyword"
37194
825456e5db30 less pschedelic token markup;
wenzelm
parents: 37186
diff changeset
   182
  val OPERATOR = "operator"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   183
  val COMMAND = "command"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   184
  val IDENT = "ident"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   185
  val STRING = "string"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   186
  val ALTSTRING = "altstring"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   187
  val VERBATIM = "verbatim"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   188
  val COMMENT = "comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   189
  val CONTROL = "control"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   190
  val MALFORMED = "malformed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   191
29185
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   192
  val COMMAND_SPAN = "command_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   193
  val IGNORED_SPAN = "ignored_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   194
  val MALFORMED_SPAN = "malformed_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   195
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   196
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   197
  /* toplevel */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   198
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   199
  val SUBGOALS = "subgoals"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   200
  val PROOF_STATE = "proof_state"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   201
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   202
  val STATE = "state"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   203
  val SUBGOAL = "subgoal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   204
  val SENDBACK = "sendback"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   205
  val HILITE = "hilite"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   206
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   207
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   208
  /* command status */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   209
29417
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   210
  val TASK = "task"
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   211
37186
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   212
  val FORKED = "forked"
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   213
  val JOINED = "joined"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   214
  val FAILED = "failed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   215
  val FINISHED = "finished"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   216
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   217
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   218
  /* interactive documents */
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   219
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   220
  val VERSION = "version"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   221
  val EXEC = "exec"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   222
  val ASSIGN = "assign"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   223
  val EDIT = "edit"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   224
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   225
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   226
  /* messages */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   227
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   228
  val PID = "pid"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   229
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   230
  val MESSAGE = "message"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   231
  val CLASS = "class"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   232
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   233
  val INIT = "init"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   234
  val STATUS = "status"
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
   235
  val REPORT = "report"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   236
  val WRITELN = "writeln"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   237
  val TRACING = "tracing"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   238
  val WARNING = "warning"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   239
  val ERROR = "error"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   240
  val DEBUG = "debug"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   241
  val SYSTEM = "system"
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38236
diff changeset
   242
  val INPUT = "input"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   243
  val STDIN = "stdin"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   244
  val STDOUT = "stdout"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   245
  val SIGNAL = "signal"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   246
  val EXIT = "exit"
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   247
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   248
  val Ready = Markup("ready", Nil)
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   249
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   250
34119
ae92efb48784 markup bad YXML as malformed;
wenzelm
parents: 34046
diff changeset
   251
  /* system data */
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   252
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   253
  val Data = Markup("data", Nil)
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
   254
}
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   255
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   256
sealed case class Markup(name: String, properties: List[(String, String)])