src/Pure/General/markup.scala
author wenzelm
Sat, 06 Nov 2010 18:10:35 +0100
changeset 40394 6dcb6cbf0719
parent 40392 6f47c49fed84
child 40848 8662b9b1f123
permissions -rw-r--r--
somewhat more uniform timing markup in ML vs. Scala;
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
40392
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    14
  object Int
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    15
  {
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    16
    def apply(x: scala.Int): String = x.toString
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    17
    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
    18
      try { Some(Integer.parseInt(s)) }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    19
      catch { case _: NumberFormatException => None }
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
40392
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    22
  object Long
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    23
  {
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    24
    def apply(x: scala.Long): String = x.toString
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    25
    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
    26
      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
    27
      catch { case _: NumberFormatException => None }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    28
  }
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    29
40392
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    30
  object Double
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    31
  {
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    32
    def apply(x: scala.Double): String = x.toString
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    33
    def unapply(s: String): Option[scala.Double] =
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    34
      try { Some(java.lang.Double.parseDouble(s)) }
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    35
      catch { case _: NumberFormatException => None }
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    36
  }
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    37
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
    38
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    39
  /* named properties */
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    40
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    41
  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
    42
  {
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    43
    def apply(value: String): List[(String, String)] = List((name, value))
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    44
    def unapply(props: List[(String, String)]): Option[String] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    45
      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
    46
  }
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
    47
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    48
  class Int_Property(name: String)
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    49
  {
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    50
    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
    51
    def unapply(props: List[(String, String)]): Option[Int] =
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)) => Int.unapply(value)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    55
      }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    56
  }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    57
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    58
  class Long_Property(name: String)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    59
  {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    60
    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
    61
    def unapply(props: List[(String, String)]): Option[Long] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    62
      props.find(_._1 == name) match {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    63
        case None => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    64
        case Some((_, value)) => Long.unapply(value)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38721
diff changeset
    65
      }
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    66
  }
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    67
40392
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    68
  class Double_Property(name: String)
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    69
  {
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    70
    def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    71
    def unapply(props: List[(String, String)]): Option[Double] =
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    72
      props.find(_._1 == name) match {
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    73
        case None => None
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    74
        case Some((_, value)) => Double.unapply(value)
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    75
      }
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    76
  }
6f47c49fed84 added Markup.Double, Markup.Double_Property;
wenzelm
parents: 39591
diff changeset
    77
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    78
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    79
  /* empty */
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    80
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    81
  val Empty = Markup("", Nil)
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    82
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38429
diff changeset
    83
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
    84
  /* misc properties */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    85
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    86
  val NAME = "name"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    87
  val KIND = "kind"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    88
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    89
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    90
  /* formal entities */
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    91
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    92
  val BINDING = "binding"
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    93
  val ENTITY = "entity"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    94
  val DEF = "def"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    95
  val REF = "ref"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    96
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    97
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    98
  /* position */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    99
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   100
  val LINE = "line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   101
  val COLUMN = "column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   102
  val OFFSET = "offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   103
  val END_LINE = "end_line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   104
  val END_COLUMN = "end_column"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   105
  val END_OFFSET = "end_offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   106
  val FILE = "file"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   107
  val ID = "id"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   108
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
   109
  val POSITION_PROPERTIES =
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
   110
    Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
29205
7dc7a75033ea added POSITION_PROPERTIES;
wenzelm
parents: 29195
diff changeset
   111
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   112
  val POSITION = "position"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   113
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   114
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   115
  /* pretty printing */
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   116
38724
d1feec02cf02 Pretty: tuned markup objects;
wenzelm
parents: 38722
diff changeset
   117
  val Indent = new Int_Property("indent")
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   118
  val BLOCK = "block"
38724
d1feec02cf02 Pretty: tuned markup objects;
wenzelm
parents: 38722
diff changeset
   119
  val Width = new Int_Property("width")
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   120
  val BREAK = "break"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   121
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   122
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   123
  /* hidden text */
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   124
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   125
  val HIDDEN = "hidden"
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   126
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   127
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   128
  /* logical entities */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   129
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   130
  val TCLASS = "tclass"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   131
  val TYCON = "tycon"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   132
  val FIXED_DECL = "fixed_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   133
  val FIXED = "fixed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   134
  val CONST_DECL = "const_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   135
  val CONST = "const"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   136
  val FACT_DECL = "fact_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   137
  val FACT = "fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   138
  val DYNAMIC_FACT = "dynamic_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   139
  val LOCAL_FACT_DECL = "local_fact_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   140
  val LOCAL_FACT = "local_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   141
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   142
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   143
  /* inner syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   144
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   145
  val TFREE = "tfree"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   146
  val TVAR = "tvar"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   147
  val FREE = "free"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   148
  val SKOLEM = "skolem"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   149
  val BOUND = "bound"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   150
  val VAR = "var"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   151
  val NUM = "num"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   152
  val FLOAT = "float"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   153
  val XNUM = "xnum"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   154
  val XSTR = "xstr"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   155
  val LITERAL = "literal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   156
  val INNER_COMMENT = "inner_comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   157
39168
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   158
  val TOKEN_RANGE = "token_range"
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   159
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   160
  val SORT = "sort"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   161
  val TYP = "typ"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   162
  val TERM = "term"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   163
  val PROP = "prop"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   164
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   165
  val ATTRIBUTE = "attribute"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   166
  val METHOD = "method"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   167
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   168
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   169
  /* embedded source text */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   170
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   171
  val ML_SOURCE = "ML_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   172
  val DOC_SOURCE = "doc_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   173
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   174
  val ANTIQ = "antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   175
  val ML_ANTIQ = "ML_antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   176
  val DOC_ANTIQ = "doc_antiq"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   177
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   178
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   179
  /* ML syntax */
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   180
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   181
  val ML_KEYWORD = "ML_keyword"
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 37194
diff changeset
   182
  val ML_DELIMITER = "ML_delimiter"
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   183
  val ML_IDENT = "ML_ident"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   184
  val ML_TVAR = "ML_tvar"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   185
  val ML_NUMERAL = "ML_numeral"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   186
  val ML_CHAR = "ML_char"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   187
  val ML_STRING = "ML_string"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   188
  val ML_COMMENT = "ML_comment"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   189
  val ML_MALFORMED = "ML_malformed"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   190
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   191
  val ML_DEF = "ML_def"
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   192
  val ML_OPEN = "ML_open"
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   193
  val ML_STRUCT = "ML_struct"
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   194
  val ML_REF = "ML_ref"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   195
  val ML_TYPING = "ML_typing"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   196
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   197
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   198
  /* outer syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   199
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   200
  val KEYWORD_DECL = "keyword_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   201
  val COMMAND_DECL = "command_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   202
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   203
  val KEYWORD = "keyword"
37194
825456e5db30 less pschedelic token markup;
wenzelm
parents: 37186
diff changeset
   204
  val OPERATOR = "operator"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   205
  val COMMAND = "command"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   206
  val IDENT = "ident"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   207
  val STRING = "string"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   208
  val ALTSTRING = "altstring"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   209
  val VERBATIM = "verbatim"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   210
  val COMMENT = "comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   211
  val CONTROL = "control"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   212
  val MALFORMED = "malformed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   213
29185
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   214
  val COMMAND_SPAN = "command_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   215
  val IGNORED_SPAN = "ignored_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   216
  val MALFORMED_SPAN = "malformed_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   217
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   218
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   219
  /* timing */
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   220
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   221
  val TIMING = "timing"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   222
  val ELAPSED = "elapsed"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   223
  val CPU = "cpu"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   224
  val GC = "gc"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   225
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   226
  object Timing
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   227
  {
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   228
    def apply(timing: isabelle.Timing): Markup =
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   229
      Markup(TIMING, List(
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   230
        (ELAPSED, Double(timing.elapsed)),
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   231
        (CPU, Double(timing.cpu)),
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   232
        (GC, Double(timing.gc))))
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   233
    def unapply(markup: Markup): Option[isabelle.Timing] =
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   234
      markup match {
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   235
        case Markup(TIMING, List(
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   236
          (ELAPSED, Double(elapsed)),
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   237
          (CPU, Double(cpu)),
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   238
          (GC, Double(gc)))) => Some(isabelle.Timing(elapsed, cpu, gc))
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   239
        case _ => None
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   240
      }
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   241
  }
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   242
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   243
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   244
  /* toplevel */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   245
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   246
  val SUBGOALS = "subgoals"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   247
  val PROOF_STATE = "proof_state"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   248
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   249
  val STATE = "state"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   250
  val SUBGOAL = "subgoal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   251
  val SENDBACK = "sendback"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   252
  val HILITE = "hilite"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   253
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   254
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   255
  /* command status */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   256
29417
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   257
  val TASK = "task"
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   258
37186
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   259
  val FORKED = "forked"
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   260
  val JOINED = "joined"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   261
  val FAILED = "failed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   262
  val FINISHED = "finished"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   263
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   264
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   265
  /* interactive documents */
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   266
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   267
  val VERSION = "version"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   268
  val EXEC = "exec"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   269
  val ASSIGN = "assign"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   270
  val EDIT = "edit"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   271
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   272
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   273
  /* messages */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   274
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38871
diff changeset
   275
  val Serial = new Long_Property("serial")
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   276
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   277
  val MESSAGE = "message"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   278
  val CLASS = "class"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   279
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   280
  val INIT = "init"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   281
  val STATUS = "status"
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39513
diff changeset
   282
  val REPORT = "report"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   283
  val WRITELN = "writeln"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   284
  val TRACING = "tracing"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   285
  val WARNING = "warning"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   286
  val ERROR = "error"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   287
  val SYSTEM = "system"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   288
  val STDOUT = "stdout"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   289
  val EXIT = "exit"
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   290
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39171
diff changeset
   291
  val NO_REPORT = "no_report"
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39171
diff changeset
   292
39171
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   293
  val BAD = "bad"
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   294
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39585
diff changeset
   295
  val READY = "ready"
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   296
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   297
34119
ae92efb48784 markup bad YXML as malformed;
wenzelm
parents: 34046
diff changeset
   298
  /* system data */
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   299
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   300
  val Data = Markup("data", Nil)
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
   301
}
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   302
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   303
sealed case class Markup(name: String, properties: List[(String, String)])