src/Pure/General/markup.scala
author wenzelm
Tue Jul 12 19:36:46 2011 +0200 (2011-07-12 ago)
changeset 43780 2cb2310d68b6
parent 43748 c70bd78ec83c
child 44298 b8f8488704e2
permissions -rw-r--r--
more uniform Properties in ML and Scala;
wenzelm@27958
     1
/*  Title:      Pure/General/markup.scala
wenzelm@27958
     2
    Author:     Makarius
wenzelm@27958
     3
wenzelm@27958
     4
Common markup elements.
wenzelm@27958
     5
*/
wenzelm@27958
     6
wenzelm@27958
     7
package isabelle
wenzelm@27958
     8
wenzelm@27970
     9
wenzelm@32450
    10
object Markup
wenzelm@32450
    11
{
wenzelm@38474
    12
  /* empty */
wenzelm@38474
    13
wenzelm@38474
    14
  val Empty = Markup("", Nil)
wenzelm@38474
    15
wenzelm@38474
    16
wenzelm@38721
    17
  /* misc properties */
wenzelm@29184
    18
wenzelm@29184
    19
  val NAME = "name"
wenzelm@43780
    20
  val Name = new Properties.String(NAME)
wenzelm@42136
    21
wenzelm@29184
    22
  val KIND = "kind"
wenzelm@43780
    23
  val Kind = new Properties.String(KIND)
wenzelm@29184
    24
wenzelm@29184
    25
wenzelm@33088
    26
  /* formal entities */
wenzelm@33088
    27
wenzelm@38887
    28
  val BINDING = "binding"
wenzelm@33088
    29
  val ENTITY = "entity"
wenzelm@33088
    30
  val DEF = "def"
wenzelm@33088
    31
  val REF = "ref"
wenzelm@33088
    32
wenzelm@42202
    33
  object Entity
wenzelm@42202
    34
  {
wenzelm@42202
    35
    def unapply(markup: Markup): Option[(String, String)] =
wenzelm@42202
    36
      markup match {
wenzelm@42202
    37
        case Markup(ENTITY, props @ Kind(kind)) =>
wenzelm@42202
    38
          props match {
wenzelm@42202
    39
            case Name(name) => Some(kind, name)
wenzelm@42202
    40
            case _ => None
wenzelm@42202
    41
          }
wenzelm@42202
    42
        case _ => None
wenzelm@42202
    43
      }
wenzelm@42202
    44
  }
wenzelm@42202
    45
wenzelm@33088
    46
wenzelm@27970
    47
  /* position */
wenzelm@27970
    48
wenzelm@27970
    49
  val LINE = "line"
wenzelm@27970
    50
  val OFFSET = "offset"
wenzelm@27970
    51
  val END_OFFSET = "end_offset"
wenzelm@27970
    52
  val FILE = "file"
wenzelm@27970
    53
  val ID = "id"
wenzelm@27970
    54
wenzelm@42327
    55
  val DEF_LINE = "def_line"
wenzelm@42327
    56
  val DEF_OFFSET = "def_offset"
wenzelm@42327
    57
  val DEF_END_OFFSET = "def_end_offset"
wenzelm@42327
    58
  val DEF_FILE = "def_file"
wenzelm@42327
    59
  val DEF_ID = "def_id"
wenzelm@42327
    60
wenzelm@43710
    61
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
wenzelm@43593
    62
  val POSITION = "position"
wenzelm@29205
    63
wenzelm@43593
    64
wenzelm@43593
    65
  /* path */
wenzelm@43593
    66
wenzelm@43593
    67
  val PATH = "path"
wenzelm@43593
    68
wenzelm@43593
    69
  object Path
wenzelm@43593
    70
  {
wenzelm@43593
    71
    def unapply(markup: Markup): Option[String] =
wenzelm@43593
    72
      markup match {
wenzelm@43593
    73
        case Markup(PATH, Name(name)) => Some(name)
wenzelm@43593
    74
        case _ => None
wenzelm@43593
    75
      }
wenzelm@43593
    76
  }
wenzelm@29184
    77
wenzelm@29184
    78
wenzelm@36683
    79
  /* pretty printing */
wenzelm@36683
    80
wenzelm@43780
    81
  val Indent = new Properties.Int("indent")
wenzelm@36683
    82
  val BLOCK = "block"
wenzelm@43780
    83
  val Width = new Properties.Int("width")
wenzelm@36683
    84
  val BREAK = "break"
wenzelm@36683
    85
wenzelm@36683
    86
wenzelm@33985
    87
  /* hidden text */
wenzelm@33985
    88
wenzelm@33985
    89
  val HIDDEN = "hidden"
wenzelm@33985
    90
wenzelm@33985
    91
wenzelm@29184
    92
  /* logical entities */
wenzelm@29184
    93
wenzelm@43551
    94
  val CLASS = "class"
wenzelm@43552
    95
  val TYPE = "type"
wenzelm@29184
    96
  val FIXED = "fixed"
wenzelm@43552
    97
  val CONSTANT = "constant"
wenzelm@43552
    98
wenzelm@29184
    99
  val DYNAMIC_FACT = "dynamic_fact"
wenzelm@29184
   100
wenzelm@29184
   101
wenzelm@29184
   102
  /* inner syntax */
wenzelm@29184
   103
wenzelm@29184
   104
  val TFREE = "tfree"
wenzelm@29184
   105
  val TVAR = "tvar"
wenzelm@29184
   106
  val FREE = "free"
wenzelm@29184
   107
  val SKOLEM = "skolem"
wenzelm@29184
   108
  val BOUND = "bound"
wenzelm@29184
   109
  val VAR = "var"
wenzelm@29184
   110
  val NUM = "num"
wenzelm@29184
   111
  val FLOAT = "float"
wenzelm@29184
   112
  val XNUM = "xnum"
wenzelm@29184
   113
  val XSTR = "xstr"
wenzelm@29184
   114
  val LITERAL = "literal"
wenzelm@43432
   115
  val DELIMITER = "delimiter"
wenzelm@43386
   116
  val INNER_STRING = "inner_string"
wenzelm@29184
   117
  val INNER_COMMENT = "inner_comment"
wenzelm@29184
   118
wenzelm@39168
   119
  val TOKEN_RANGE = "token_range"
wenzelm@39168
   120
wenzelm@29184
   121
  val SORT = "sort"
wenzelm@29184
   122
  val TYP = "typ"
wenzelm@29184
   123
  val TERM = "term"
wenzelm@29184
   124
  val PROP = "prop"
wenzelm@29184
   125
wenzelm@29184
   126
  val ATTRIBUTE = "attribute"
wenzelm@29184
   127
  val METHOD = "method"
wenzelm@29184
   128
wenzelm@29184
   129
wenzelm@29184
   130
  /* embedded source text */
wenzelm@29184
   131
wenzelm@29184
   132
  val ML_SOURCE = "ML_source"
wenzelm@29184
   133
  val DOC_SOURCE = "doc_source"
wenzelm@29184
   134
wenzelm@29184
   135
  val ANTIQ = "antiq"
wenzelm@43560
   136
  val ML_ANTIQUOTATION = "ML antiquotation"
wenzelm@43564
   137
  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
wenzelm@43564
   138
  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
wenzelm@29184
   139
wenzelm@29184
   140
wenzelm@30615
   141
  /* ML syntax */
wenzelm@30615
   142
wenzelm@30615
   143
  val ML_KEYWORD = "ML_keyword"
wenzelm@37195
   144
  val ML_DELIMITER = "ML_delimiter"
wenzelm@30615
   145
  val ML_IDENT = "ML_ident"
wenzelm@30615
   146
  val ML_TVAR = "ML_tvar"
wenzelm@30615
   147
  val ML_NUMERAL = "ML_numeral"
wenzelm@30615
   148
  val ML_CHAR = "ML_char"
wenzelm@30615
   149
  val ML_STRING = "ML_string"
wenzelm@30615
   150
  val ML_COMMENT = "ML_comment"
wenzelm@30615
   151
  val ML_MALFORMED = "ML_malformed"
wenzelm@30615
   152
wenzelm@30702
   153
  val ML_DEF = "ML_def"
wenzelm@31472
   154
  val ML_OPEN = "ML_open"
wenzelm@31472
   155
  val ML_STRUCT = "ML_struct"
wenzelm@30702
   156
  val ML_TYPING = "ML_typing"
wenzelm@30702
   157
wenzelm@30615
   158
wenzelm@29184
   159
  /* outer syntax */
wenzelm@29184
   160
wenzelm@29184
   161
  val KEYWORD_DECL = "keyword_decl"
wenzelm@29184
   162
  val COMMAND_DECL = "command_decl"
wenzelm@29184
   163
wenzelm@29184
   164
  val KEYWORD = "keyword"
wenzelm@37194
   165
  val OPERATOR = "operator"
wenzelm@29184
   166
  val COMMAND = "command"
wenzelm@29184
   167
  val IDENT = "ident"
wenzelm@29184
   168
  val STRING = "string"
wenzelm@29184
   169
  val ALTSTRING = "altstring"
wenzelm@29184
   170
  val VERBATIM = "verbatim"
wenzelm@29184
   171
  val COMMENT = "comment"
wenzelm@29184
   172
  val CONTROL = "control"
wenzelm@29184
   173
  val MALFORMED = "malformed"
wenzelm@29184
   174
wenzelm@29185
   175
  val COMMAND_SPAN = "command_span"
wenzelm@29185
   176
  val IGNORED_SPAN = "ignored_span"
wenzelm@29185
   177
  val MALFORMED_SPAN = "malformed_span"
wenzelm@29185
   178
wenzelm@29184
   179
wenzelm@43673
   180
  /* theory loader */
wenzelm@43673
   181
wenzelm@43673
   182
  val LOADED_THEORY = "loaded_theory"
wenzelm@43673
   183
wenzelm@43673
   184
wenzelm@40394
   185
  /* timing */
wenzelm@40394
   186
wenzelm@40394
   187
  val TIMING = "timing"
wenzelm@40394
   188
  val ELAPSED = "elapsed"
wenzelm@40394
   189
  val CPU = "cpu"
wenzelm@40394
   190
  val GC = "gc"
wenzelm@40394
   191
wenzelm@40394
   192
  object Timing
wenzelm@40394
   193
  {
wenzelm@40394
   194
    def apply(timing: isabelle.Timing): Markup =
wenzelm@40394
   195
      Markup(TIMING, List(
wenzelm@43780
   196
        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
wenzelm@43780
   197
        (CPU, Properties.Value.Double(timing.cpu.seconds)),
wenzelm@43780
   198
        (GC, Properties.Value.Double(timing.gc.seconds))))
wenzelm@40394
   199
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@40394
   200
      markup match {
wenzelm@40394
   201
        case Markup(TIMING, List(
wenzelm@43780
   202
          (ELAPSED, Properties.Value.Double(elapsed)),
wenzelm@43780
   203
          (CPU, Properties.Value.Double(cpu)),
wenzelm@43780
   204
          (GC, Properties.Value.Double(gc)))) =>
wenzelm@40848
   205
            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@40394
   206
        case _ => None
wenzelm@40394
   207
      }
wenzelm@40394
   208
  }
wenzelm@40394
   209
wenzelm@40394
   210
wenzelm@29184
   211
  /* toplevel */
wenzelm@29184
   212
wenzelm@38721
   213
  val SUBGOALS = "subgoals"
wenzelm@38721
   214
  val PROOF_STATE = "proof_state"
wenzelm@38721
   215
wenzelm@29184
   216
  val STATE = "state"
wenzelm@29184
   217
  val SUBGOAL = "subgoal"
wenzelm@29184
   218
  val SENDBACK = "sendback"
wenzelm@29184
   219
  val HILITE = "hilite"
wenzelm@29184
   220
wenzelm@29184
   221
wenzelm@29184
   222
  /* command status */
wenzelm@29184
   223
wenzelm@29417
   224
  val TASK = "task"
wenzelm@29417
   225
wenzelm@37186
   226
  val FORKED = "forked"
wenzelm@37186
   227
  val JOINED = "joined"
wenzelm@29184
   228
  val FAILED = "failed"
wenzelm@29184
   229
  val FINISHED = "finished"
wenzelm@29488
   230
wenzelm@29488
   231
wenzelm@29488
   232
  /* interactive documents */
wenzelm@29488
   233
wenzelm@38414
   234
  val VERSION = "version"
wenzelm@38414
   235
  val EXEC = "exec"
wenzelm@38414
   236
  val ASSIGN = "assign"
wenzelm@29488
   237
  val EDIT = "edit"
wenzelm@29184
   238
wenzelm@27970
   239
wenzelm@43721
   240
  /* prover process */
wenzelm@43721
   241
wenzelm@43721
   242
  val PROVER_COMMAND = "prover_command"
wenzelm@43721
   243
  val PROVER_ARG = "prover_arg"
wenzelm@43721
   244
wenzelm@43721
   245
wenzelm@27970
   246
  /* messages */
wenzelm@27970
   247
wenzelm@43780
   248
  val Serial = new Properties.Long("serial")
wenzelm@27970
   249
wenzelm@29195
   250
  val MESSAGE = "message"
wenzelm@29522
   251
wenzelm@29522
   252
  val INIT = "init"
wenzelm@29522
   253
  val STATUS = "status"
wenzelm@39525
   254
  val REPORT = "report"
wenzelm@29522
   255
  val WRITELN = "writeln"
wenzelm@29522
   256
  val TRACING = "tracing"
wenzelm@29522
   257
  val WARNING = "warning"
wenzelm@29522
   258
  val ERROR = "error"
wenzelm@43746
   259
  val RAW = "raw"
wenzelm@29522
   260
  val SYSTEM = "system"
wenzelm@29522
   261
  val STDOUT = "stdout"
wenzelm@29522
   262
  val EXIT = "exit"
wenzelm@29195
   263
wenzelm@39439
   264
  val NO_REPORT = "no_report"
wenzelm@39439
   265
wenzelm@39171
   266
  val BAD = "bad"
wenzelm@39171
   267
wenzelm@39591
   268
  val READY = "ready"
wenzelm@31384
   269
wenzelm@27970
   270
wenzelm@43748
   271
  /* raw message functions */
wenzelm@43748
   272
wenzelm@43748
   273
  val FUNCTION = "function"
wenzelm@43780
   274
  val Function = new Properties.String(FUNCTION)
wenzelm@43748
   275
wenzelm@43748
   276
  val INVOKE_SCALA = "invoke_scala"
wenzelm@43748
   277
  object Invoke_Scala
wenzelm@43748
   278
  {
wenzelm@43780
   279
    def unapply(props: Properties.T): Option[(String, String)] =
wenzelm@43748
   280
      props match {
wenzelm@43748
   281
        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
wenzelm@43748
   282
        case _ => None
wenzelm@43748
   283
      }
wenzelm@43748
   284
  }
wenzelm@43748
   285
wenzelm@43748
   286
wenzelm@34119
   287
  /* system data */
wenzelm@27970
   288
wenzelm@38231
   289
  val Data = Markup("data", Nil)
wenzelm@27958
   290
}
wenzelm@38230
   291
wenzelm@43780
   292
sealed case class Markup(name: String, properties: Properties.T)