src/Pure/General/markup.scala
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43710 7270ae921cf2
child 43746 a41f618c641d
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;
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"
42136
826168ae0213 added Markup.Name and Markup.Kind convenience;
wenzelm
parents: 41483
diff changeset
    87
  val Name = new Property(NAME)
826168ae0213 added Markup.Name and Markup.Kind convenience;
wenzelm
parents: 41483
diff changeset
    88
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    89
  val KIND = "kind"
42136
826168ae0213 added Markup.Name and Markup.Kind convenience;
wenzelm
parents: 41483
diff changeset
    90
  val Kind = new Property(KIND)
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    91
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    92
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    93
  /* formal entities */
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    94
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
    95
  val BINDING = "binding"
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    96
  val ENTITY = "entity"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    97
  val DEF = "def"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    98
  val REF = "ref"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    99
42202
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   100
  object Entity
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   101
  {
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   102
    def unapply(markup: Markup): Option[(String, String)] =
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   103
      markup match {
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   104
        case Markup(ENTITY, props @ Kind(kind)) =>
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   105
          props match {
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   106
            case Name(name) => Some(kind, name)
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   107
            case _ => None
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   108
          }
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   109
        case _ => None
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   110
      }
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   111
  }
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
   112
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
   113
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   114
  /* position */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   115
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   116
  val LINE = "line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   117
  val OFFSET = "offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   118
  val END_OFFSET = "end_offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   119
  val FILE = "file"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   120
  val ID = "id"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   121
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
   122
  val DEF_LINE = "def_line"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
   123
  val DEF_OFFSET = "def_offset"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
   124
  val DEF_END_OFFSET = "def_end_offset"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
   125
  val DEF_FILE = "def_file"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
   126
  val DEF_ID = "def_id"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
   127
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 43673
diff changeset
   128
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   129
  val POSITION = "position"
29205
7dc7a75033ea added POSITION_PROPERTIES;
wenzelm
parents: 29195
diff changeset
   130
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   131
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   132
  /* path */
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   133
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   134
  val PATH = "path"
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   135
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   136
  object Path
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   137
  {
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   138
    def unapply(markup: Markup): Option[String] =
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   139
      markup match {
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   140
        case Markup(PATH, Name(name)) => Some(name)
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   141
        case _ => None
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   142
      }
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
   143
  }
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   144
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   145
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   146
  /* pretty printing */
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   147
38724
d1feec02cf02 Pretty: tuned markup objects;
wenzelm
parents: 38722
diff changeset
   148
  val Indent = new Int_Property("indent")
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   149
  val BLOCK = "block"
38724
d1feec02cf02 Pretty: tuned markup objects;
wenzelm
parents: 38722
diff changeset
   150
  val Width = new Int_Property("width")
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   151
  val BREAK = "break"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   152
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
   153
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   154
  /* hidden text */
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   155
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   156
  val HIDDEN = "hidden"
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   157
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
   158
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   159
  /* logical entities */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   160
43551
07a9cbf2376f clarified Markup.CLASS vs. HTML.CLASS;
wenzelm
parents: 43432
diff changeset
   161
  val CLASS = "class"
43552
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43551
diff changeset
   162
  val TYPE = "type"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   163
  val FIXED = "fixed"
43552
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43551
diff changeset
   164
  val CONSTANT = "constant"
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43551
diff changeset
   165
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   166
  val DYNAMIC_FACT = "dynamic_fact"
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
  /* inner syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   170
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   171
  val TFREE = "tfree"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   172
  val TVAR = "tvar"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   173
  val FREE = "free"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   174
  val SKOLEM = "skolem"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   175
  val BOUND = "bound"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   176
  val VAR = "var"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   177
  val NUM = "num"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   178
  val FLOAT = "float"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   179
  val XNUM = "xnum"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   180
  val XSTR = "xstr"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   181
  val LITERAL = "literal"
43432
224006e5ac46 inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents: 43386
diff changeset
   182
  val DELIMITER = "delimiter"
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 42492
diff changeset
   183
  val INNER_STRING = "inner_string"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   184
  val INNER_COMMENT = "inner_comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   185
39168
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   186
  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
   187
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   188
  val SORT = "sort"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   189
  val TYP = "typ"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   190
  val TERM = "term"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   191
  val PROP = "prop"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   192
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   193
  val ATTRIBUTE = "attribute"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   194
  val METHOD = "method"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   195
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   196
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   197
  /* embedded source text */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   198
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   199
  val ML_SOURCE = "ML_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   200
  val DOC_SOURCE = "doc_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   201
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   202
  val ANTIQ = "antiq"
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43552
diff changeset
   203
  val ML_ANTIQUOTATION = "ML antiquotation"
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
   204
  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
   205
  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   206
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   207
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   208
  /* ML syntax */
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   209
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   210
  val ML_KEYWORD = "ML_keyword"
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 37194
diff changeset
   211
  val ML_DELIMITER = "ML_delimiter"
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   212
  val ML_IDENT = "ML_ident"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   213
  val ML_TVAR = "ML_tvar"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   214
  val ML_NUMERAL = "ML_numeral"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   215
  val ML_CHAR = "ML_char"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   216
  val ML_STRING = "ML_string"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   217
  val ML_COMMENT = "ML_comment"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   218
  val ML_MALFORMED = "ML_malformed"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   219
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   220
  val ML_DEF = "ML_def"
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   221
  val ML_OPEN = "ML_open"
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   222
  val ML_STRUCT = "ML_struct"
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   223
  val ML_TYPING = "ML_typing"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   224
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   225
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   226
  /* outer syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   227
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   228
  val KEYWORD_DECL = "keyword_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   229
  val COMMAND_DECL = "command_decl"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   230
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   231
  val KEYWORD = "keyword"
37194
825456e5db30 less pschedelic token markup;
wenzelm
parents: 37186
diff changeset
   232
  val OPERATOR = "operator"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   233
  val COMMAND = "command"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   234
  val IDENT = "ident"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   235
  val STRING = "string"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   236
  val ALTSTRING = "altstring"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   237
  val VERBATIM = "verbatim"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   238
  val COMMENT = "comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   239
  val CONTROL = "control"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   240
  val MALFORMED = "malformed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   241
29185
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   242
  val COMMAND_SPAN = "command_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   243
  val IGNORED_SPAN = "ignored_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   244
  val MALFORMED_SPAN = "malformed_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   245
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   246
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
   247
  /* theory loader */
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
   248
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
   249
  val LOADED_THEORY = "loaded_theory"
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
   250
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
   251
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   252
  /* timing */
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   253
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   254
  val TIMING = "timing"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   255
  val ELAPSED = "elapsed"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   256
  val CPU = "cpu"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   257
  val GC = "gc"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   258
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   259
  object Timing
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   260
  {
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   261
    def apply(timing: isabelle.Timing): Markup =
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   262
      Markup(TIMING, List(
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40394
diff changeset
   263
        (ELAPSED, Double(timing.elapsed.seconds)),
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40394
diff changeset
   264
        (CPU, Double(timing.cpu.seconds)),
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40394
diff changeset
   265
        (GC, Double(timing.gc.seconds))))
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   266
    def unapply(markup: Markup): Option[isabelle.Timing] =
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   267
      markup match {
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   268
        case Markup(TIMING, List(
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40394
diff changeset
   269
          (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40394
diff changeset
   270
            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   271
        case _ => None
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   272
      }
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   273
  }
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   274
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
   275
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   276
  /* toplevel */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   277
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   278
  val SUBGOALS = "subgoals"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   279
  val PROOF_STATE = "proof_state"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   280
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   281
  val STATE = "state"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   282
  val SUBGOAL = "subgoal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   283
  val SENDBACK = "sendback"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   284
  val HILITE = "hilite"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   285
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   286
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   287
  /* command status */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   288
29417
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   289
  val TASK = "task"
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   290
37186
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   291
  val FORKED = "forked"
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   292
  val JOINED = "joined"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   293
  val FAILED = "failed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   294
  val FINISHED = "finished"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   295
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   296
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   297
  /* interactive documents */
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   298
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   299
  val VERSION = "version"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   300
  val EXEC = "exec"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   301
  val ASSIGN = "assign"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   302
  val EDIT = "edit"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   303
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   304
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   305
  /* prover process */
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   306
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   307
  val PROVER_COMMAND = "prover_command"
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   308
  val PROVER_ARG = "prover_arg"
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   309
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   310
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   311
  /* messages */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   312
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38871
diff changeset
   313
  val Serial = new Long_Property("serial")
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   314
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   315
  val MESSAGE = "message"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   316
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   317
  val INIT = "init"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   318
  val STATUS = "status"
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39513
diff changeset
   319
  val REPORT = "report"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   320
  val WRITELN = "writeln"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   321
  val TRACING = "tracing"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   322
  val WARNING = "warning"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   323
  val ERROR = "error"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   324
  val SYSTEM = "system"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   325
  val STDOUT = "stdout"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   326
  val EXIT = "exit"
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   327
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39171
diff changeset
   328
  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
   329
39171
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   330
  val BAD = "bad"
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   331
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39585
diff changeset
   332
  val READY = "ready"
31384
ce169bd37fc0 IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents: 30702
diff changeset
   333
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   334
34119
ae92efb48784 markup bad YXML as malformed;
wenzelm
parents: 34046
diff changeset
   335
  /* system data */
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   336
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   337
  val Data = Markup("data", Nil)
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
   338
}
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   339
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   340
sealed case class Markup(name: String, properties: List[(String, String)])