src/Pure/PIDE/markup.scala
author wenzelm
Tue Nov 11 18:16:25 2014 +0100 (2014-11-11 ago)
changeset 58978 e42da880c61e
parent 58853 f8715e7c1be6
child 59081 2ceb05ee0331
permissions -rw-r--r--
more position information, e.g. relevant for errors in generated ML source;
wenzelm@45670
     1
/*  Title:      Pure/PIDE/markup.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@27958
     3
    Author:     Makarius
wenzelm@27958
     4
wenzelm@56743
     5
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@56743
    13
  /* elements */
wenzelm@56743
    14
wenzelm@56743
    15
  object Elements
wenzelm@56743
    16
  {
wenzelm@56743
    17
    def apply(elems: Set[String]): Elements = new Elements(elems)
wenzelm@56743
    18
    def apply(elems: String*): Elements = apply(Set(elems: _*))
wenzelm@56743
    19
    val empty: Elements = apply()
wenzelm@56743
    20
    val full: Elements =
wenzelm@56743
    21
      new Elements(Set.empty)
wenzelm@56743
    22
      {
wenzelm@56743
    23
        override def apply(elem: String): Boolean = true
wenzelm@56743
    24
        override def toString: String = "Elements.full"
wenzelm@56743
    25
      }
wenzelm@56743
    26
  }
wenzelm@56743
    27
wenzelm@56743
    28
  sealed class Elements private[Markup](private val rep: Set[String])
wenzelm@56743
    29
  {
wenzelm@56743
    30
    def apply(elem: String): Boolean = rep.contains(elem)
wenzelm@56743
    31
    def + (elem: String): Elements = new Elements(rep + elem)
wenzelm@56743
    32
    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
wenzelm@56743
    33
    override def toString: String = rep.mkString("Elements(", ",", ")")
wenzelm@56743
    34
  }
wenzelm@56743
    35
wenzelm@56743
    36
wenzelm@45666
    37
  /* properties */
wenzelm@29184
    38
wenzelm@29184
    39
  val NAME = "name"
wenzelm@43780
    40
  val Name = new Properties.String(NAME)
wenzelm@42136
    41
wenzelm@29184
    42
  val KIND = "kind"
wenzelm@43780
    43
  val Kind = new Properties.String(KIND)
wenzelm@29184
    44
wenzelm@52854
    45
  val INSTANCE = "instance"
wenzelm@52854
    46
  val Instance = new Properties.String(INSTANCE)
wenzelm@52854
    47
wenzelm@29184
    48
wenzelm@50201
    49
  /* basic markup */
wenzelm@29184
    50
wenzelm@45666
    51
  val Empty = Markup("", Nil)
wenzelm@45666
    52
  val Broken = Markup("broken", Nil)
wenzelm@50201
    53
wenzelm@55553
    54
  class Markup_String(val name: String, prop: String)
wenzelm@55553
    55
  {
wenzelm@55553
    56
    private val Prop = new Properties.String(prop)
wenzelm@55553
    57
wenzelm@55553
    58
    def apply(s: String): Markup = Markup(name, Prop(s))
wenzelm@55553
    59
    def unapply(markup: Markup): Option[String] =
wenzelm@55553
    60
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@55553
    61
  }
wenzelm@55553
    62
wenzelm@55553
    63
  class Markup_Int(val name: String, prop: String)
wenzelm@55553
    64
  {
wenzelm@55553
    65
    private val Prop = new Properties.Int(prop)
wenzelm@55553
    66
wenzelm@55553
    67
    def apply(i: Int): Markup = Markup(name, Prop(i))
wenzelm@55553
    68
    def unapply(markup: Markup): Option[Int] =
wenzelm@55553
    69
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@55553
    70
  }
wenzelm@55553
    71
wenzelm@50201
    72
wenzelm@50201
    73
  /* formal entities */
wenzelm@50201
    74
wenzelm@50201
    75
  val BINDING = "binding"
wenzelm@50201
    76
  val ENTITY = "entity"
wenzelm@50201
    77
  val DEF = "def"
wenzelm@50201
    78
  val REF = "ref"
wenzelm@50201
    79
wenzelm@50201
    80
  object Entity
wenzelm@50201
    81
  {
wenzelm@50201
    82
    def unapply(markup: Markup): Option[(String, String)] =
wenzelm@50201
    83
      markup match {
wenzelm@55553
    84
        case Markup(ENTITY, props) =>
wenzelm@55553
    85
          (props, props) match {
wenzelm@55615
    86
            case (Kind(kind), Name(name)) => Some((kind, name))
wenzelm@50201
    87
            case _ => None
wenzelm@50201
    88
          }
wenzelm@50201
    89
        case _ => None
wenzelm@50201
    90
      }
wenzelm@50201
    91
  }
wenzelm@50201
    92
wenzelm@50201
    93
wenzelm@55672
    94
  /* completion */
wenzelm@55672
    95
wenzelm@55672
    96
  val COMPLETION = "completion"
wenzelm@55914
    97
  val NO_COMPLETION = "no_completion"
wenzelm@55672
    98
wenzelm@55672
    99
wenzelm@50201
   100
  /* position */
wenzelm@50201
   101
wenzelm@50201
   102
  val LINE = "line"
wenzelm@58978
   103
  val END_LINE = "line"
wenzelm@50201
   104
  val OFFSET = "offset"
wenzelm@50201
   105
  val END_OFFSET = "end_offset"
wenzelm@50201
   106
  val FILE = "file"
wenzelm@50201
   107
  val ID = "id"
wenzelm@50201
   108
wenzelm@50201
   109
  val DEF_LINE = "def_line"
wenzelm@50201
   110
  val DEF_OFFSET = "def_offset"
wenzelm@50201
   111
  val DEF_END_OFFSET = "def_end_offset"
wenzelm@50201
   112
  val DEF_FILE = "def_file"
wenzelm@50201
   113
  val DEF_ID = "def_id"
wenzelm@50201
   114
wenzelm@50201
   115
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
wenzelm@50201
   116
  val POSITION = "position"
wenzelm@50201
   117
wenzelm@50201
   118
wenzelm@58464
   119
  /* expression */
wenzelm@58464
   120
wenzelm@58464
   121
  val EXPRESSION = "expression"
wenzelm@58464
   122
wenzelm@58464
   123
wenzelm@58544
   124
  /* citation */
wenzelm@58544
   125
wenzelm@58544
   126
  val CITATION = "citation"
wenzelm@58545
   127
  val Citation = new Markup_String(CITATION, NAME)
wenzelm@58544
   128
wenzelm@58544
   129
wenzelm@55552
   130
  /* embedded languages */
wenzelm@55552
   131
wenzelm@55666
   132
  val Symbols = new Properties.Boolean("symbols")
wenzelm@55666
   133
  val Antiquotes = new Properties.Boolean("antiquotes")
wenzelm@55828
   134
  val Delimited = new Properties.Boolean("delimited")
wenzelm@55615
   135
wenzelm@55552
   136
  val LANGUAGE = "language"
wenzelm@55615
   137
  object Language
wenzelm@55615
   138
  {
wenzelm@55616
   139
    val ML = "ML"
wenzelm@56278
   140
    val SML = "SML"
wenzelm@56843
   141
    val PATH = "path"
wenzelm@55616
   142
    val UNKNOWN = "unknown"
wenzelm@55616
   143
wenzelm@55828
   144
    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
wenzelm@55615
   145
      markup match {
wenzelm@55615
   146
        case Markup(LANGUAGE, props) =>
wenzelm@55828
   147
          (props, props, props, props) match {
wenzelm@55828
   148
            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
wenzelm@55828
   149
              Some((name, symbols, antiquotes, delimited))
wenzelm@55615
   150
            case _ => None
wenzelm@55615
   151
          }
wenzelm@55615
   152
        case _ => None
wenzelm@55615
   153
      }
wenzelm@55615
   154
  }
wenzelm@55552
   155
wenzelm@55552
   156
wenzelm@54702
   157
  /* external resources */
wenzelm@50201
   158
wenzelm@50201
   159
  val PATH = "path"
wenzelm@55553
   160
  val Path = new Markup_String(PATH, NAME)
wenzelm@50201
   161
wenzelm@54702
   162
  val URL = "url"
wenzelm@55553
   163
  val Url = new Markup_String(URL, NAME)
wenzelm@54702
   164
wenzelm@50201
   165
wenzelm@50201
   166
  /* pretty printing */
wenzelm@50201
   167
wenzelm@55553
   168
  val Block = new Markup_Int("block", "indent")
wenzelm@55553
   169
  val Break = new Markup_Int("break", "width")
wenzelm@50201
   170
wenzelm@51570
   171
  val ITEM = "item"
wenzelm@51574
   172
  val BULLET = "bullet"
wenzelm@51570
   173
wenzelm@50201
   174
  val SEPARATOR = "separator"
wenzelm@50201
   175
wenzelm@50201
   176
wenzelm@56548
   177
  /* text properties */
wenzelm@56548
   178
wenzelm@56548
   179
  val WORDS = "words"
wenzelm@50201
   180
wenzelm@50201
   181
  val HIDDEN = "hidden"
wenzelm@50201
   182
wenzelm@50201
   183
wenzelm@58048
   184
  /* misc entities */
wenzelm@50201
   185
wenzelm@50201
   186
  val CLASS = "class"
wenzelm@50201
   187
  val TYPE_NAME = "type_name"
wenzelm@50201
   188
  val FIXED = "fixed"
wenzelm@53378
   189
  val CASE = "case"
wenzelm@50201
   190
  val CONSTANT = "constant"
wenzelm@50201
   191
  val DYNAMIC_FACT = "dynamic_fact"
wenzelm@50201
   192
wenzelm@50201
   193
wenzelm@50201
   194
  /* inner syntax */
wenzelm@50201
   195
wenzelm@50201
   196
  val TFREE = "tfree"
wenzelm@50201
   197
  val TVAR = "tvar"
wenzelm@50201
   198
  val FREE = "free"
wenzelm@50201
   199
  val SKOLEM = "skolem"
wenzelm@50201
   200
  val BOUND = "bound"
wenzelm@50201
   201
  val VAR = "var"
wenzelm@50201
   202
  val NUMERAL = "numeral"
wenzelm@50201
   203
  val LITERAL = "literal"
wenzelm@50201
   204
  val DELIMITER = "delimiter"
wenzelm@50201
   205
  val INNER_STRING = "inner_string"
wenzelm@55033
   206
  val INNER_CARTOUCHE = "inner_cartouche"
wenzelm@50201
   207
  val INNER_COMMENT = "inner_comment"
wenzelm@50201
   208
wenzelm@50201
   209
  val TOKEN_RANGE = "token_range"
wenzelm@50201
   210
wenzelm@50201
   211
  val SORTING = "sorting"
wenzelm@50201
   212
  val TYPING = "typing"
wenzelm@50201
   213
wenzelm@50201
   214
  val ATTRIBUTE = "attribute"
wenzelm@50201
   215
  val METHOD = "method"
wenzelm@50201
   216
wenzelm@50201
   217
wenzelm@55552
   218
  /* antiquotations */
wenzelm@50201
   219
wenzelm@55526
   220
  val ANTIQUOTED = "antiquoted"
wenzelm@55526
   221
  val ANTIQUOTE = "antiquote"
wenzelm@55526
   222
wenzelm@50201
   223
  val ML_ANTIQUOTATION = "ML_antiquotation"
wenzelm@50201
   224
  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
wenzelm@50201
   225
  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
wenzelm@50201
   226
wenzelm@50201
   227
wenzelm@50201
   228
  /* text structure */
wenzelm@50201
   229
wenzelm@50201
   230
  val PARAGRAPH = "paragraph"
wenzelm@50545
   231
  val TEXT_FOLD = "text_fold"
wenzelm@50201
   232
wenzelm@50201
   233
wenzelm@50201
   234
  /* ML syntax */
wenzelm@50201
   235
wenzelm@55505
   236
  val ML_KEYWORD1 = "ML_keyword1"
wenzelm@55505
   237
  val ML_KEYWORD2 = "ML_keyword2"
wenzelm@55505
   238
  val ML_KEYWORD3 = "ML_keyword3"
wenzelm@50201
   239
  val ML_DELIMITER = "ML_delimiter"
wenzelm@50201
   240
  val ML_TVAR = "ML_tvar"
wenzelm@50201
   241
  val ML_NUMERAL = "ML_numeral"
wenzelm@50201
   242
  val ML_CHAR = "ML_char"
wenzelm@50201
   243
  val ML_STRING = "ML_string"
wenzelm@50201
   244
  val ML_COMMENT = "ML_comment"
wenzelm@56278
   245
  val SML_STRING = "SML_string"
wenzelm@56278
   246
  val SML_COMMENT = "SML_comment"
wenzelm@50201
   247
wenzelm@50201
   248
  val ML_DEF = "ML_def"
wenzelm@50201
   249
  val ML_OPEN = "ML_open"
wenzelm@55837
   250
  val ML_STRUCTURE = "ML_structure"
wenzelm@50201
   251
  val ML_TYPING = "ML_typing"
wenzelm@50201
   252
wenzelm@50201
   253
wenzelm@50201
   254
  /* outer syntax */
wenzelm@50201
   255
wenzelm@55744
   256
  val COMMAND = "command"
wenzelm@55744
   257
  val KEYWORD1 = "keyword1"
wenzelm@55744
   258
  val KEYWORD2 = "keyword2"
wenzelm@55765
   259
  val KEYWORD3 = "keyword3"
wenzelm@55919
   260
  val QUASI_KEYWORD = "quasi_keyword"
wenzelm@56202
   261
  val IMPROPER = "improper"
wenzelm@50201
   262
  val OPERATOR = "operator"
wenzelm@50201
   263
  val STRING = "string"
wenzelm@50201
   264
  val ALTSTRING = "altstring"
wenzelm@50201
   265
  val VERBATIM = "verbatim"
wenzelm@55033
   266
  val CARTOUCHE = "cartouche"
wenzelm@50201
   267
  val COMMENT = "comment"
wenzelm@50201
   268
wenzelm@50201
   269
wenzelm@50201
   270
  /* timing */
wenzelm@50201
   271
wenzelm@50781
   272
  val Elapsed = new Properties.Double("elapsed")
wenzelm@50781
   273
  val CPU = new Properties.Double("cpu")
wenzelm@50781
   274
  val GC = new Properties.Double("gc")
wenzelm@50781
   275
wenzelm@50781
   276
  object Timing_Properties
wenzelm@50781
   277
  {
wenzelm@50781
   278
    def apply(timing: isabelle.Timing): Properties.T =
wenzelm@50781
   279
      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
wenzelm@51662
   280
wenzelm@50781
   281
    def unapply(props: Properties.T): Option[isabelle.Timing] =
wenzelm@50781
   282
      (props, props, props) match {
wenzelm@50781
   283
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
wenzelm@50781
   284
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@50781
   285
        case _ => None
wenzelm@50781
   286
      }
wenzelm@50781
   287
  }
wenzelm@50781
   288
wenzelm@50201
   289
  val TIMING = "timing"
wenzelm@50201
   290
wenzelm@50201
   291
  object Timing
wenzelm@50201
   292
  {
wenzelm@50781
   293
    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
wenzelm@51662
   294
wenzelm@50201
   295
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@50201
   296
      markup match {
wenzelm@50781
   297
        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
wenzelm@50201
   298
        case _ => None
wenzelm@50201
   299
      }
wenzelm@50201
   300
  }
wenzelm@50201
   301
wenzelm@50201
   302
wenzelm@51662
   303
  /* command timing */
wenzelm@51662
   304
wenzelm@51818
   305
  val COMMAND_TIMING = "command_timing"
wenzelm@51662
   306
wenzelm@51662
   307
wenzelm@50201
   308
  /* toplevel */
wenzelm@50201
   309
wenzelm@50201
   310
  val SUBGOALS = "subgoals"
wenzelm@50201
   311
  val PROOF_STATE = "proof_state"
wenzelm@50201
   312
wenzelm@50201
   313
  val STATE = "state"
wenzelm@50543
   314
  val GOAL = "goal"
wenzelm@50201
   315
  val SUBGOAL = "subgoal"
wenzelm@50215
   316
wenzelm@50450
   317
wenzelm@50201
   318
  /* command status */
wenzelm@50201
   319
wenzelm@50201
   320
  val TASK = "task"
wenzelm@50201
   321
wenzelm@50201
   322
  val ACCEPTED = "accepted"
wenzelm@50201
   323
  val FORKED = "forked"
wenzelm@50201
   324
  val JOINED = "joined"
wenzelm@50201
   325
  val RUNNING = "running"
wenzelm@50201
   326
  val FINISHED = "finished"
wenzelm@50201
   327
  val FAILED = "failed"
wenzelm@50201
   328
wenzelm@50201
   329
wenzelm@50201
   330
  /* interactive documents */
wenzelm@50201
   331
wenzelm@50201
   332
  val VERSION = "version"
wenzelm@50201
   333
  val ASSIGN = "assign"
wenzelm@50201
   334
wenzelm@50201
   335
wenzelm@50201
   336
  /* prover process */
wenzelm@50201
   337
wenzelm@50201
   338
  val PROVER_COMMAND = "prover_command"
wenzelm@50201
   339
  val PROVER_ARG = "prover_arg"
wenzelm@50201
   340
wenzelm@50201
   341
wenzelm@50201
   342
  /* messages */
wenzelm@50201
   343
lars@55316
   344
  val SERIAL = "serial"
lars@55316
   345
  val Serial = new Properties.Long(SERIAL)
wenzelm@50201
   346
wenzelm@50201
   347
  val MESSAGE = "message"
wenzelm@50201
   348
wenzelm@50201
   349
  val INIT = "init"
wenzelm@50201
   350
  val STATUS = "status"
wenzelm@50201
   351
  val REPORT = "report"
wenzelm@50500
   352
  val RESULT = "result"
wenzelm@50201
   353
  val WRITELN = "writeln"
wenzelm@50201
   354
  val TRACING = "tracing"
wenzelm@50201
   355
  val WARNING = "warning"
wenzelm@50201
   356
  val ERROR = "error"
wenzelm@50201
   357
  val PROTOCOL = "protocol"
wenzelm@50201
   358
  val SYSTEM = "system"
wenzelm@50201
   359
  val STDOUT = "stdout"
wenzelm@50201
   360
  val STDERR = "stderr"
wenzelm@50201
   361
  val EXIT = "exit"
wenzelm@50201
   362
wenzelm@50201
   363
  val WRITELN_MESSAGE = "writeln_message"
wenzelm@50201
   364
  val TRACING_MESSAGE = "tracing_message"
wenzelm@50201
   365
  val WARNING_MESSAGE = "warning_message"
wenzelm@50201
   366
  val ERROR_MESSAGE = "error_message"
wenzelm@50201
   367
wenzelm@52876
   368
  val messages =
wenzelm@50201
   369
    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
wenzelm@52876
   370
        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
wenzelm@52876
   371
  val message: String => String = messages.withDefault((s: String) => s)
wenzelm@50201
   372
wenzelm@50201
   373
  val Return_Code = new Properties.Int("return_code")
wenzelm@50201
   374
wenzelm@50201
   375
  val LEGACY = "legacy"
wenzelm@50201
   376
wenzelm@50201
   377
  val NO_REPORT = "no_report"
wenzelm@50201
   378
wenzelm@50201
   379
  val BAD = "bad"
wenzelm@50201
   380
wenzelm@50500
   381
  val INTENSIFY = "intensify"
wenzelm@52643
   382
  val INFORMATION = "information"
wenzelm@50500
   383
wenzelm@50500
   384
wenzelm@50500
   385
  /* active areas */
wenzelm@50500
   386
wenzelm@50715
   387
  val BROWSER = "browser"
wenzelm@50500
   388
  val GRAPHVIEW = "graphview"
wenzelm@50500
   389
wenzelm@50500
   390
  val SENDBACK = "sendback"
wenzelm@50500
   391
  val PADDING = "padding"
wenzelm@52697
   392
  val PADDING_LINE = (PADDING, "line")
wenzelm@52697
   393
  val PADDING_COMMAND = (PADDING, "command")
wenzelm@50500
   394
wenzelm@50500
   395
  val DIALOG = "dialog"
wenzelm@50503
   396
  val Result = new Properties.String(RESULT)
wenzelm@50500
   397
wenzelm@50201
   398
wenzelm@50201
   399
  /* protocol message functions */
wenzelm@50201
   400
wenzelm@50201
   401
  val FUNCTION = "function"
wenzelm@50201
   402
  val Function = new Properties.String(FUNCTION)
wenzelm@50201
   403
wenzelm@52563
   404
  val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
wenzelm@50201
   405
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
wenzelm@50201
   406
wenzelm@52111
   407
  object Protocol_Handler
wenzelm@52111
   408
  {
wenzelm@52111
   409
    def unapply(props: Properties.T): Option[(String)] =
wenzelm@52111
   410
      props match {
wenzelm@52111
   411
        case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
wenzelm@52111
   412
        case _ => None
wenzelm@52111
   413
      }
wenzelm@52111
   414
  }
wenzelm@52111
   415
wenzelm@52111
   416
  val INVOKE_SCALA = "invoke_scala"
wenzelm@50201
   417
  object Invoke_Scala
wenzelm@50201
   418
  {
wenzelm@50201
   419
    def unapply(props: Properties.T): Option[(String, String)] =
wenzelm@50201
   420
      props match {
wenzelm@52111
   421
        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
wenzelm@50201
   422
        case _ => None
wenzelm@50201
   423
      }
wenzelm@50201
   424
  }
wenzelm@52111
   425
wenzelm@52111
   426
  val CANCEL_SCALA = "cancel_scala"
wenzelm@50201
   427
  object Cancel_Scala
wenzelm@50201
   428
  {
wenzelm@50201
   429
    def unapply(props: Properties.T): Option[String] =
wenzelm@50201
   430
      props match {
wenzelm@52111
   431
        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
wenzelm@50201
   432
        case _ => None
wenzelm@50201
   433
      }
wenzelm@50201
   434
  }
wenzelm@50255
   435
wenzelm@50255
   436
  object ML_Statistics
wenzelm@50255
   437
  {
wenzelm@50255
   438
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50255
   439
      props match {
wenzelm@50255
   440
        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
wenzelm@50255
   441
        case _ => None
wenzelm@50255
   442
      }
wenzelm@50255
   443
  }
wenzelm@50975
   444
wenzelm@50975
   445
  object Task_Statistics
wenzelm@50975
   446
  {
wenzelm@50975
   447
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50975
   448
      props match {
wenzelm@50975
   449
        case (FUNCTION, "task_statistics") :: stats => Some(stats)
wenzelm@50975
   450
        case _ => None
wenzelm@50975
   451
      }
wenzelm@50975
   452
  }
lars@55316
   453
wenzelm@56616
   454
  object Loading_Theory
wenzelm@56616
   455
  {
wenzelm@56616
   456
    def unapply(props: Properties.T): Option[String] =
wenzelm@56616
   457
      props match {
wenzelm@56616
   458
        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
wenzelm@56616
   459
        case _ => None
wenzelm@56616
   460
      }
wenzelm@56616
   461
  }
wenzelm@56616
   462
wenzelm@56616
   463
  object Use_Theories_Result
wenzelm@56616
   464
  {
wenzelm@56616
   465
    def unapply(props: Properties.T): Option[(String, Boolean)] =
wenzelm@56616
   466
      props match {
wenzelm@56616
   467
        case List((FUNCTION, "use_theories_result"),
wenzelm@56616
   468
          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
wenzelm@56616
   469
        case _ => None
wenzelm@56616
   470
      }
wenzelm@56616
   471
  }
wenzelm@56616
   472
wenzelm@56864
   473
  val PRINT_OPERATIONS = "print_operations"
wenzelm@56864
   474
wenzelm@55555
   475
lars@55316
   476
  /* simplifier trace */
lars@55316
   477
wenzelm@57597
   478
  val SIMP_TRACE_PANEL = "simp_trace_panel"
lars@55316
   479
wenzelm@55555
   480
  val SIMP_TRACE_LOG = "simp_trace_log"
wenzelm@55555
   481
  val SIMP_TRACE_STEP = "simp_trace_step"
wenzelm@55555
   482
  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
wenzelm@55555
   483
  val SIMP_TRACE_HINT = "simp_trace_hint"
wenzelm@55555
   484
  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
lars@55316
   485
wenzelm@55555
   486
  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
wenzelm@55555
   487
  object Simp_Trace_Cancel
lars@55316
   488
  {
lars@55316
   489
    def unapply(props: Properties.T): Option[Long] =
lars@55316
   490
      props match {
wenzelm@55555
   491
        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
lars@55316
   492
        case _ => None
lars@55316
   493
      }
lars@55316
   494
  }
wenzelm@45666
   495
}
wenzelm@43721
   496
wenzelm@43721
   497
wenzelm@45666
   498
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@43748
   499