src/Pure/PIDE/markup.scala
author wenzelm
Sat Feb 15 18:28:18 2014 +0100 (2014-02-15 ago)
changeset 55505 2a1ca7f6607b
parent 55390 36550a4eac5e
child 55526 39708e59f4b0
permissions -rw-r--r--
more uniform ML keyword markup;
tuned;
wenzelm@45670
     1
/*  Title:      Pure/PIDE/markup.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@27958
     3
    Author:     Makarius
wenzelm@27958
     4
wenzelm@50201
     5
Isabelle-specific implementation of quasi-abstract markup elements.
wenzelm@27958
     6
*/
wenzelm@27958
     7
wenzelm@27958
     8
package isabelle
wenzelm@27958
     9
wenzelm@27970
    10
wenzelm@32450
    11
object Markup
wenzelm@32450
    12
{
wenzelm@45666
    13
  /* properties */
wenzelm@29184
    14
wenzelm@29184
    15
  val NAME = "name"
wenzelm@43780
    16
  val Name = new Properties.String(NAME)
wenzelm@42136
    17
wenzelm@29184
    18
  val KIND = "kind"
wenzelm@43780
    19
  val Kind = new Properties.String(KIND)
wenzelm@29184
    20
wenzelm@52854
    21
  val INSTANCE = "instance"
wenzelm@52854
    22
  val Instance = new Properties.String(INSTANCE)
wenzelm@52854
    23
wenzelm@29184
    24
wenzelm@50201
    25
  /* basic markup */
wenzelm@29184
    26
wenzelm@45666
    27
  val Empty = Markup("", Nil)
wenzelm@45666
    28
  val Broken = Markup("broken", Nil)
wenzelm@50201
    29
wenzelm@50201
    30
wenzelm@50201
    31
  /* formal entities */
wenzelm@50201
    32
wenzelm@50201
    33
  val BINDING = "binding"
wenzelm@50201
    34
  val ENTITY = "entity"
wenzelm@50201
    35
  val DEF = "def"
wenzelm@50201
    36
  val REF = "ref"
wenzelm@50201
    37
wenzelm@50201
    38
  object Entity
wenzelm@50201
    39
  {
wenzelm@50201
    40
    def unapply(markup: Markup): Option[(String, String)] =
wenzelm@50201
    41
      markup match {
wenzelm@50201
    42
        case Markup(ENTITY, props @ Kind(kind)) =>
wenzelm@50201
    43
          props match {
wenzelm@50201
    44
            case Name(name) => Some(kind, name)
wenzelm@50201
    45
            case _ => None
wenzelm@50201
    46
          }
wenzelm@50201
    47
        case _ => None
wenzelm@50201
    48
      }
wenzelm@50201
    49
  }
wenzelm@50201
    50
wenzelm@50201
    51
wenzelm@50201
    52
  /* position */
wenzelm@50201
    53
wenzelm@50201
    54
  val LINE = "line"
wenzelm@50201
    55
  val OFFSET = "offset"
wenzelm@50201
    56
  val END_OFFSET = "end_offset"
wenzelm@50201
    57
  val FILE = "file"
wenzelm@50201
    58
  val ID = "id"
wenzelm@50201
    59
wenzelm@50201
    60
  val DEF_LINE = "def_line"
wenzelm@50201
    61
  val DEF_OFFSET = "def_offset"
wenzelm@50201
    62
  val DEF_END_OFFSET = "def_end_offset"
wenzelm@50201
    63
  val DEF_FILE = "def_file"
wenzelm@50201
    64
  val DEF_ID = "def_id"
wenzelm@50201
    65
wenzelm@50201
    66
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
wenzelm@50201
    67
  val POSITION = "position"
wenzelm@50201
    68
wenzelm@50201
    69
wenzelm@54702
    70
  /* external resources */
wenzelm@50201
    71
wenzelm@50201
    72
  val PATH = "path"
wenzelm@50201
    73
wenzelm@50201
    74
  object Path
wenzelm@50201
    75
  {
wenzelm@50201
    76
    def unapply(markup: Markup): Option[String] =
wenzelm@50201
    77
      markup match {
wenzelm@50201
    78
        case Markup(PATH, Name(name)) => Some(name)
wenzelm@50201
    79
        case _ => None
wenzelm@50201
    80
      }
wenzelm@50201
    81
  }
wenzelm@50201
    82
wenzelm@54702
    83
  val URL = "url"
wenzelm@54702
    84
wenzelm@54702
    85
  object Url
wenzelm@54702
    86
  {
wenzelm@54702
    87
    def unapply(markup: Markup): Option[String] =
wenzelm@54702
    88
      markup match {
wenzelm@54702
    89
        case Markup(URL, Name(name)) => Some(name)
wenzelm@54702
    90
        case _ => None
wenzelm@54702
    91
      }
wenzelm@54702
    92
  }
wenzelm@54702
    93
wenzelm@50201
    94
wenzelm@50201
    95
  /* pretty printing */
wenzelm@50201
    96
wenzelm@50201
    97
  val Indent = new Properties.Int("indent")
wenzelm@50201
    98
  val BLOCK = "block"
wenzelm@51570
    99
wenzelm@50201
   100
  val Width = new Properties.Int("width")
wenzelm@50201
   101
  val BREAK = "break"
wenzelm@50201
   102
wenzelm@51570
   103
  val ITEM = "item"
wenzelm@51574
   104
  val BULLET = "bullet"
wenzelm@51570
   105
wenzelm@50201
   106
  val SEPARATOR = "separator"
wenzelm@50201
   107
wenzelm@50201
   108
wenzelm@50201
   109
  /* hidden text */
wenzelm@50201
   110
wenzelm@50201
   111
  val HIDDEN = "hidden"
wenzelm@50201
   112
wenzelm@50201
   113
wenzelm@50201
   114
  /* logical entities */
wenzelm@50201
   115
wenzelm@50201
   116
  val CLASS = "class"
wenzelm@50201
   117
  val TYPE_NAME = "type_name"
wenzelm@50201
   118
  val FIXED = "fixed"
wenzelm@53378
   119
  val CASE = "case"
wenzelm@50201
   120
  val CONSTANT = "constant"
wenzelm@50201
   121
  val DYNAMIC_FACT = "dynamic_fact"
wenzelm@50201
   122
wenzelm@50201
   123
wenzelm@50201
   124
  /* inner syntax */
wenzelm@50201
   125
wenzelm@50201
   126
  val TFREE = "tfree"
wenzelm@50201
   127
  val TVAR = "tvar"
wenzelm@50201
   128
  val FREE = "free"
wenzelm@50201
   129
  val SKOLEM = "skolem"
wenzelm@50201
   130
  val BOUND = "bound"
wenzelm@50201
   131
  val VAR = "var"
wenzelm@50201
   132
  val NUMERAL = "numeral"
wenzelm@50201
   133
  val LITERAL = "literal"
wenzelm@50201
   134
  val DELIMITER = "delimiter"
wenzelm@50201
   135
  val INNER_STRING = "inner_string"
wenzelm@55033
   136
  val INNER_CARTOUCHE = "inner_cartouche"
wenzelm@50201
   137
  val INNER_COMMENT = "inner_comment"
wenzelm@50201
   138
wenzelm@50201
   139
  val TOKEN_RANGE = "token_range"
wenzelm@50201
   140
wenzelm@50201
   141
  val SORT = "sort"
wenzelm@50201
   142
  val TYP = "typ"
wenzelm@50201
   143
  val TERM = "term"
wenzelm@50201
   144
  val PROP = "prop"
wenzelm@50201
   145
wenzelm@50201
   146
  val SORTING = "sorting"
wenzelm@50201
   147
  val TYPING = "typing"
wenzelm@50201
   148
wenzelm@50201
   149
  val ATTRIBUTE = "attribute"
wenzelm@50201
   150
  val METHOD = "method"
wenzelm@50201
   151
wenzelm@50201
   152
wenzelm@50201
   153
  /* embedded source text */
wenzelm@50201
   154
wenzelm@50201
   155
  val ML_SOURCE = "ML_source"
wenzelm@50201
   156
  val DOCUMENT_SOURCE = "document_source"
wenzelm@50201
   157
wenzelm@50201
   158
  val ANTIQ = "antiq"
wenzelm@50201
   159
  val ML_ANTIQUOTATION = "ML_antiquotation"
wenzelm@50201
   160
  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
wenzelm@50201
   161
  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
wenzelm@50201
   162
wenzelm@50201
   163
wenzelm@50201
   164
  /* text structure */
wenzelm@50201
   165
wenzelm@50201
   166
  val PARAGRAPH = "paragraph"
wenzelm@50545
   167
  val TEXT_FOLD = "text_fold"
wenzelm@50201
   168
wenzelm@50201
   169
wenzelm@50201
   170
  /* ML syntax */
wenzelm@50201
   171
wenzelm@55505
   172
  val ML_KEYWORD1 = "ML_keyword1"
wenzelm@55505
   173
  val ML_KEYWORD2 = "ML_keyword2"
wenzelm@55505
   174
  val ML_KEYWORD3 = "ML_keyword3"
wenzelm@50201
   175
  val ML_DELIMITER = "ML_delimiter"
wenzelm@50201
   176
  val ML_TVAR = "ML_tvar"
wenzelm@50201
   177
  val ML_NUMERAL = "ML_numeral"
wenzelm@50201
   178
  val ML_CHAR = "ML_char"
wenzelm@50201
   179
  val ML_STRING = "ML_string"
wenzelm@50201
   180
  val ML_COMMENT = "ML_comment"
wenzelm@50201
   181
wenzelm@50201
   182
  val ML_DEF = "ML_def"
wenzelm@50201
   183
  val ML_OPEN = "ML_open"
wenzelm@50201
   184
  val ML_STRUCT = "ML_struct"
wenzelm@50201
   185
  val ML_TYPING = "ML_typing"
wenzelm@50201
   186
wenzelm@50201
   187
wenzelm@50201
   188
  /* outer syntax */
wenzelm@50201
   189
wenzelm@50201
   190
  val KEYWORD = "keyword"
wenzelm@50201
   191
  val OPERATOR = "operator"
wenzelm@50201
   192
  val COMMAND = "command"
wenzelm@50201
   193
  val STRING = "string"
wenzelm@50201
   194
  val ALTSTRING = "altstring"
wenzelm@50201
   195
  val VERBATIM = "verbatim"
wenzelm@55033
   196
  val CARTOUCHE = "cartouche"
wenzelm@50201
   197
  val COMMENT = "comment"
wenzelm@50201
   198
  val CONTROL = "control"
wenzelm@50201
   199
wenzelm@50201
   200
  val KEYWORD1 = "keyword1"
wenzelm@50201
   201
  val KEYWORD2 = "keyword2"
wenzelm@50201
   202
wenzelm@50201
   203
wenzelm@50201
   204
  /* timing */
wenzelm@50201
   205
wenzelm@50781
   206
  val Elapsed = new Properties.Double("elapsed")
wenzelm@50781
   207
  val CPU = new Properties.Double("cpu")
wenzelm@50781
   208
  val GC = new Properties.Double("gc")
wenzelm@50781
   209
wenzelm@50781
   210
  object Timing_Properties
wenzelm@50781
   211
  {
wenzelm@50781
   212
    def apply(timing: isabelle.Timing): Properties.T =
wenzelm@50781
   213
      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
wenzelm@51662
   214
wenzelm@50781
   215
    def unapply(props: Properties.T): Option[isabelle.Timing] =
wenzelm@50781
   216
      (props, props, props) match {
wenzelm@50781
   217
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
wenzelm@50781
   218
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@50781
   219
        case _ => None
wenzelm@50781
   220
      }
wenzelm@50781
   221
  }
wenzelm@50781
   222
wenzelm@50201
   223
  val TIMING = "timing"
wenzelm@50201
   224
wenzelm@50201
   225
  object Timing
wenzelm@50201
   226
  {
wenzelm@50781
   227
    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
wenzelm@51662
   228
wenzelm@50201
   229
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@50201
   230
      markup match {
wenzelm@50781
   231
        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
wenzelm@50201
   232
        case _ => None
wenzelm@50201
   233
      }
wenzelm@50201
   234
  }
wenzelm@50201
   235
wenzelm@50201
   236
wenzelm@51662
   237
  /* command timing */
wenzelm@51662
   238
wenzelm@51818
   239
  val COMMAND_TIMING = "command_timing"
wenzelm@51662
   240
wenzelm@51662
   241
wenzelm@50201
   242
  /* toplevel */
wenzelm@50201
   243
wenzelm@50201
   244
  val SUBGOALS = "subgoals"
wenzelm@50201
   245
  val PROOF_STATE = "proof_state"
wenzelm@50201
   246
wenzelm@50201
   247
  val STATE = "state"
wenzelm@50543
   248
  val GOAL = "goal"
wenzelm@50201
   249
  val SUBGOAL = "subgoal"
wenzelm@50215
   250
wenzelm@50450
   251
wenzelm@50201
   252
  /* command status */
wenzelm@50201
   253
wenzelm@50201
   254
  val TASK = "task"
wenzelm@50201
   255
wenzelm@50201
   256
  val ACCEPTED = "accepted"
wenzelm@50201
   257
  val FORKED = "forked"
wenzelm@50201
   258
  val JOINED = "joined"
wenzelm@50201
   259
  val RUNNING = "running"
wenzelm@50201
   260
  val FINISHED = "finished"
wenzelm@50201
   261
  val FAILED = "failed"
wenzelm@50201
   262
wenzelm@50201
   263
wenzelm@50201
   264
  /* interactive documents */
wenzelm@50201
   265
wenzelm@50201
   266
  val VERSION = "version"
wenzelm@50201
   267
  val ASSIGN = "assign"
wenzelm@50201
   268
wenzelm@50201
   269
wenzelm@50201
   270
  /* prover process */
wenzelm@50201
   271
wenzelm@50201
   272
  val PROVER_COMMAND = "prover_command"
wenzelm@50201
   273
  val PROVER_ARG = "prover_arg"
wenzelm@50201
   274
wenzelm@50201
   275
wenzelm@50201
   276
  /* messages */
wenzelm@50201
   277
lars@55316
   278
  val SERIAL = "serial"
lars@55316
   279
  val Serial = new Properties.Long(SERIAL)
wenzelm@50201
   280
wenzelm@50201
   281
  val MESSAGE = "message"
wenzelm@50201
   282
wenzelm@50201
   283
  val INIT = "init"
wenzelm@50201
   284
  val STATUS = "status"
wenzelm@50201
   285
  val REPORT = "report"
wenzelm@50500
   286
  val RESULT = "result"
wenzelm@50201
   287
  val WRITELN = "writeln"
wenzelm@50201
   288
  val TRACING = "tracing"
wenzelm@50201
   289
  val WARNING = "warning"
wenzelm@50201
   290
  val ERROR = "error"
wenzelm@50201
   291
  val PROTOCOL = "protocol"
wenzelm@50201
   292
  val SYSTEM = "system"
wenzelm@50201
   293
  val STDOUT = "stdout"
wenzelm@50201
   294
  val STDERR = "stderr"
wenzelm@50201
   295
  val EXIT = "exit"
wenzelm@50201
   296
wenzelm@50201
   297
  val WRITELN_MESSAGE = "writeln_message"
wenzelm@50201
   298
  val TRACING_MESSAGE = "tracing_message"
wenzelm@50201
   299
  val WARNING_MESSAGE = "warning_message"
wenzelm@50201
   300
  val ERROR_MESSAGE = "error_message"
wenzelm@50201
   301
wenzelm@52876
   302
  val messages =
wenzelm@50201
   303
    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
wenzelm@52876
   304
        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
wenzelm@52876
   305
  val message: String => String = messages.withDefault((s: String) => s)
wenzelm@50201
   306
wenzelm@50201
   307
  val Return_Code = new Properties.Int("return_code")
wenzelm@50201
   308
wenzelm@50201
   309
  val LEGACY = "legacy"
wenzelm@50201
   310
wenzelm@50201
   311
  val NO_REPORT = "no_report"
wenzelm@50201
   312
wenzelm@50201
   313
  val BAD = "bad"
wenzelm@50201
   314
wenzelm@50500
   315
  val INTENSIFY = "intensify"
wenzelm@52643
   316
  val INFORMATION = "information"
wenzelm@50500
   317
wenzelm@50500
   318
wenzelm@50500
   319
  /* active areas */
wenzelm@50500
   320
wenzelm@50715
   321
  val BROWSER = "browser"
wenzelm@50500
   322
  val GRAPHVIEW = "graphview"
wenzelm@50500
   323
wenzelm@50500
   324
  val SENDBACK = "sendback"
wenzelm@50500
   325
  val PADDING = "padding"
wenzelm@52697
   326
  val PADDING_LINE = (PADDING, "line")
wenzelm@52697
   327
  val PADDING_COMMAND = (PADDING, "command")
wenzelm@50500
   328
wenzelm@50500
   329
  val DIALOG = "dialog"
wenzelm@50503
   330
  val Result = new Properties.String(RESULT)
wenzelm@50500
   331
wenzelm@50201
   332
wenzelm@50201
   333
  /* protocol message functions */
wenzelm@50201
   334
wenzelm@50201
   335
  val FUNCTION = "function"
wenzelm@50201
   336
  val Function = new Properties.String(FUNCTION)
wenzelm@50201
   337
wenzelm@52800
   338
  val Flush: Properties.T = List((FUNCTION, "flush"))
wenzelm@52800
   339
wenzelm@52563
   340
  val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
wenzelm@50201
   341
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
wenzelm@50201
   342
wenzelm@52111
   343
  object Protocol_Handler
wenzelm@52111
   344
  {
wenzelm@52111
   345
    def unapply(props: Properties.T): Option[(String)] =
wenzelm@52111
   346
      props match {
wenzelm@52111
   347
        case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
wenzelm@52111
   348
        case _ => None
wenzelm@52111
   349
      }
wenzelm@52111
   350
  }
wenzelm@52111
   351
wenzelm@52111
   352
  val INVOKE_SCALA = "invoke_scala"
wenzelm@50201
   353
  object Invoke_Scala
wenzelm@50201
   354
  {
wenzelm@50201
   355
    def unapply(props: Properties.T): Option[(String, String)] =
wenzelm@50201
   356
      props match {
wenzelm@52111
   357
        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
wenzelm@50201
   358
        case _ => None
wenzelm@50201
   359
      }
wenzelm@50201
   360
  }
wenzelm@52111
   361
wenzelm@52111
   362
  val CANCEL_SCALA = "cancel_scala"
wenzelm@50201
   363
  object Cancel_Scala
wenzelm@50201
   364
  {
wenzelm@50201
   365
    def unapply(props: Properties.T): Option[String] =
wenzelm@50201
   366
      props match {
wenzelm@52111
   367
        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
wenzelm@50201
   368
        case _ => None
wenzelm@50201
   369
      }
wenzelm@50201
   370
  }
wenzelm@50255
   371
wenzelm@53055
   372
  val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
wenzelm@53055
   373
  val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
wenzelm@53055
   374
wenzelm@50255
   375
  object ML_Statistics
wenzelm@50255
   376
  {
wenzelm@50255
   377
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50255
   378
      props match {
wenzelm@50255
   379
        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
wenzelm@50255
   380
        case _ => None
wenzelm@50255
   381
      }
wenzelm@50255
   382
  }
wenzelm@50975
   383
wenzelm@50975
   384
  object Task_Statistics
wenzelm@50975
   385
  {
wenzelm@50975
   386
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50975
   387
      props match {
wenzelm@50975
   388
        case (FUNCTION, "task_statistics") :: stats => Some(stats)
wenzelm@50975
   389
        case _ => None
wenzelm@50975
   390
      }
wenzelm@50975
   391
  }
lars@55316
   392
lars@55316
   393
  /* simplifier trace */
lars@55316
   394
lars@55316
   395
  val TEXT = "text"
lars@55316
   396
  val Text = new Properties.String(TEXT)
lars@55316
   397
lars@55316
   398
  val PARENT = "parent"
lars@55316
   399
  val Parent = new Properties.Long(PARENT)
lars@55316
   400
lars@55316
   401
  val SUCCESS = "success"
lars@55316
   402
  val Success = new Properties.Boolean(SUCCESS)
lars@55316
   403
lars@55390
   404
  val MEMORY = "memory"
lars@55390
   405
  val Memory = new Properties.Boolean(MEMORY)
lars@55390
   406
lars@55316
   407
  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
lars@55316
   408
  object Cancel_Simp_Trace
lars@55316
   409
  {
lars@55316
   410
    def unapply(props: Properties.T): Option[Long] =
lars@55316
   411
      props match {
lars@55316
   412
        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
lars@55316
   413
        case _ => None
lars@55316
   414
      }
lars@55316
   415
  }
lars@55316
   416
lars@55316
   417
  val SIMP_TRACE = "simp_trace"
lars@55316
   418
  object Simp_Trace
lars@55316
   419
  {
lars@55316
   420
    def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
lars@55316
   421
      tree match {
lars@55316
   422
        case XML.Elem(Markup(SIMP_TRACE, props), _) =>
lars@55316
   423
          (props, props) match {
lars@55316
   424
            case (Serial(serial), Name(name)) =>
lars@55316
   425
              Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
lars@55316
   426
            case _ =>
lars@55316
   427
              None
lars@55316
   428
          }
lars@55316
   429
        case _ =>
lars@55316
   430
          None
lars@55316
   431
      }
lars@55316
   432
  }
lars@55316
   433
lars@55316
   434
  /* trace items from the prover */
lars@55316
   435
lars@55316
   436
  object Simp_Trace_Item
lars@55316
   437
  {
lars@55316
   438
lars@55316
   439
    def unapply(tree: XML.Tree): Option[(String, Data)] =
lars@55316
   440
      tree match {
lars@55316
   441
        case XML.Elem(Markup(RESULT, Serial(serial)), List(
lars@55316
   442
          XML.Elem(Markup(markup, props), content)
lars@55316
   443
        )) if markup.startsWith("simp_trace_") =>
lars@55316
   444
          (props, props) match {
lars@55316
   445
            case (Text(text), Parent(parent)) =>
lars@55316
   446
              Some((markup, Data(serial, markup, text, parent, props, content)))
lars@55316
   447
            case _ =>
lars@55316
   448
              None
lars@55316
   449
          }
lars@55316
   450
        case _ =>
lars@55316
   451
          None
lars@55316
   452
      }
lars@55316
   453
lars@55316
   454
    val LOG = "simp_trace_log"
lars@55316
   455
    val STEP = "simp_trace_step"
lars@55316
   456
    val RECURSE = "simp_trace_recurse"
lars@55316
   457
    val HINT = "simp_trace_hint"
lars@55316
   458
    val IGNORE = "simp_trace_ignore"
lars@55316
   459
lars@55316
   460
    case class Data(serial: Long, markup: String, text: String,
lars@55316
   461
                    parent: Long, props: Properties.T, content: XML.Body)
lars@55390
   462
    {
lars@55390
   463
      def memory: Boolean =
lars@55390
   464
        Memory.unapply(props) getOrElse true
lars@55390
   465
    }
lars@55316
   466
lars@55316
   467
  }
lars@55316
   468
wenzelm@45666
   469
}
wenzelm@43721
   470
wenzelm@43721
   471
wenzelm@45666
   472
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@43748
   473