src/Pure/PIDE/markup.scala
author wenzelm
Sat Dec 19 14:47:52 2015 +0100 (2015-12-19)
changeset 61864 3a5992c3410c
parent 61862 e2a9e46ac0fb
child 62806 de9bf8171626
permissions -rw-r--r--
support for blocks with consistent breaks;
tuned;
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@60744
    45
  val SERIAL = "serial"
wenzelm@60744
    46
  val Serial = new Properties.Long(SERIAL)
wenzelm@60744
    47
wenzelm@52854
    48
  val INSTANCE = "instance"
wenzelm@52854
    49
  val Instance = new Properties.String(INSTANCE)
wenzelm@52854
    50
wenzelm@29184
    51
wenzelm@50201
    52
  /* basic markup */
wenzelm@29184
    53
wenzelm@45666
    54
  val Empty = Markup("", Nil)
wenzelm@45666
    55
  val Broken = Markup("broken", Nil)
wenzelm@50201
    56
wenzelm@55551
    57
  class Markup_String(val name: String, prop: String)
wenzelm@55551
    58
  {
wenzelm@55551
    59
    private val Prop = new Properties.String(prop)
wenzelm@55551
    60
wenzelm@55551
    61
    def apply(s: String): Markup = Markup(name, Prop(s))
wenzelm@55551
    62
    def unapply(markup: Markup): Option[String] =
wenzelm@55551
    63
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@55551
    64
  }
wenzelm@55551
    65
wenzelm@55551
    66
  class Markup_Int(val name: String, prop: String)
wenzelm@55551
    67
  {
wenzelm@55551
    68
    private val Prop = new Properties.Int(prop)
wenzelm@55551
    69
wenzelm@55551
    70
    def apply(i: Int): Markup = Markup(name, Prop(i))
wenzelm@55551
    71
    def unapply(markup: Markup): Option[Int] =
wenzelm@55551
    72
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@55551
    73
  }
wenzelm@55551
    74
wenzelm@60744
    75
  class Markup_Long(val name: String, prop: String)
wenzelm@60744
    76
  {
wenzelm@60744
    77
    private val Prop = new Properties.Long(prop)
wenzelm@60744
    78
wenzelm@60744
    79
    def apply(i: Long): Markup = Markup(name, Prop(i))
wenzelm@60744
    80
    def unapply(markup: Markup): Option[Long] =
wenzelm@60744
    81
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@60744
    82
  }
wenzelm@60744
    83
wenzelm@50201
    84
wenzelm@50201
    85
  /* formal entities */
wenzelm@50201
    86
wenzelm@50201
    87
  val BINDING = "binding"
wenzelm@50201
    88
  val ENTITY = "entity"
wenzelm@50201
    89
  val DEF = "def"
wenzelm@50201
    90
  val REF = "ref"
wenzelm@50201
    91
wenzelm@50201
    92
  object Entity
wenzelm@50201
    93
  {
wenzelm@50201
    94
    def unapply(markup: Markup): Option[(String, String)] =
wenzelm@50201
    95
      markup match {
wenzelm@55551
    96
        case Markup(ENTITY, props) =>
wenzelm@55551
    97
          (props, props) match {
wenzelm@55615
    98
            case (Kind(kind), Name(name)) => Some((kind, name))
wenzelm@50201
    99
            case _ => None
wenzelm@50201
   100
          }
wenzelm@50201
   101
        case _ => None
wenzelm@50201
   102
      }
wenzelm@50201
   103
  }
wenzelm@50201
   104
wenzelm@50201
   105
wenzelm@55672
   106
  /* completion */
wenzelm@55672
   107
wenzelm@55672
   108
  val COMPLETION = "completion"
wenzelm@55914
   109
  val NO_COMPLETION = "no_completion"
wenzelm@55672
   110
wenzelm@55672
   111
wenzelm@50201
   112
  /* position */
wenzelm@50201
   113
wenzelm@50201
   114
  val LINE = "line"
wenzelm@58978
   115
  val END_LINE = "line"
wenzelm@50201
   116
  val OFFSET = "offset"
wenzelm@50201
   117
  val END_OFFSET = "end_offset"
wenzelm@50201
   118
  val FILE = "file"
wenzelm@50201
   119
  val ID = "id"
wenzelm@50201
   120
wenzelm@50201
   121
  val DEF_LINE = "def_line"
wenzelm@50201
   122
  val DEF_OFFSET = "def_offset"
wenzelm@50201
   123
  val DEF_END_OFFSET = "def_end_offset"
wenzelm@50201
   124
  val DEF_FILE = "def_file"
wenzelm@50201
   125
  val DEF_ID = "def_id"
wenzelm@50201
   126
wenzelm@50201
   127
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
wenzelm@50201
   128
  val POSITION = "position"
wenzelm@50201
   129
wenzelm@50201
   130
wenzelm@58464
   131
  /* expression */
wenzelm@58464
   132
wenzelm@58464
   133
  val EXPRESSION = "expression"
wenzelm@58464
   134
wenzelm@58464
   135
wenzelm@58544
   136
  /* citation */
wenzelm@58544
   137
wenzelm@58544
   138
  val CITATION = "citation"
wenzelm@58545
   139
  val Citation = new Markup_String(CITATION, NAME)
wenzelm@58544
   140
wenzelm@58544
   141
wenzelm@55550
   142
  /* embedded languages */
wenzelm@55550
   143
wenzelm@55666
   144
  val Symbols = new Properties.Boolean("symbols")
wenzelm@55666
   145
  val Antiquotes = new Properties.Boolean("antiquotes")
wenzelm@55828
   146
  val Delimited = new Properties.Boolean("delimited")
wenzelm@55615
   147
wenzelm@55550
   148
  val LANGUAGE = "language"
wenzelm@55615
   149
  object Language
wenzelm@55615
   150
  {
wenzelm@55616
   151
    val ML = "ML"
wenzelm@56278
   152
    val SML = "SML"
wenzelm@56843
   153
    val PATH = "path"
wenzelm@55616
   154
    val UNKNOWN = "unknown"
wenzelm@55616
   155
wenzelm@55828
   156
    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
wenzelm@55615
   157
      markup match {
wenzelm@55615
   158
        case Markup(LANGUAGE, props) =>
wenzelm@55828
   159
          (props, props, props, props) match {
wenzelm@55828
   160
            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
wenzelm@55828
   161
              Some((name, symbols, antiquotes, delimited))
wenzelm@55615
   162
            case _ => None
wenzelm@55615
   163
          }
wenzelm@55615
   164
        case _ => None
wenzelm@55615
   165
      }
wenzelm@55615
   166
  }
wenzelm@55550
   167
wenzelm@55550
   168
wenzelm@54702
   169
  /* external resources */
wenzelm@50201
   170
wenzelm@50201
   171
  val PATH = "path"
wenzelm@55551
   172
  val Path = new Markup_String(PATH, NAME)
wenzelm@50201
   173
wenzelm@54702
   174
  val URL = "url"
wenzelm@55551
   175
  val Url = new Markup_String(URL, NAME)
wenzelm@54702
   176
wenzelm@61660
   177
  val DOC = "doc"
wenzelm@61660
   178
  val Doc = new Markup_String(DOC, NAME)
wenzelm@61660
   179
wenzelm@50201
   180
wenzelm@50201
   181
  /* pretty printing */
wenzelm@50201
   182
wenzelm@61864
   183
  val Consistent = new Properties.Boolean("consistent")
wenzelm@61862
   184
  val Indent = new Properties.Int("indent")
wenzelm@61864
   185
  val Width = new Properties.Int("width")
wenzelm@61862
   186
wenzelm@61864
   187
  object Block
wenzelm@61864
   188
  {
wenzelm@61864
   189
    val name = "block"
wenzelm@61864
   190
    def apply(c: Boolean, i: Int): Markup =
wenzelm@61864
   191
      Markup(name,
wenzelm@61864
   192
        (if (c) Consistent(c) else Nil) :::
wenzelm@61864
   193
        (if (i != 0) Indent(i) else Nil))
wenzelm@61864
   194
    def unapply(markup: Markup): Option[(Boolean, Int)] =
wenzelm@61864
   195
      if (markup.name == name) {
wenzelm@61864
   196
        val c = Consistent.unapply(markup.properties).getOrElse(false)
wenzelm@61864
   197
        val i = Indent.unapply(markup.properties).getOrElse(0)
wenzelm@61864
   198
        Some((c, i))
wenzelm@61864
   199
      }
wenzelm@61864
   200
      else None
wenzelm@61864
   201
  }
wenzelm@61864
   202
wenzelm@61862
   203
  object Break
wenzelm@61862
   204
  {
wenzelm@61862
   205
    val name = "break"
wenzelm@61864
   206
    def apply(w: Int, i: Int): Markup =
wenzelm@61864
   207
      Markup(name,
wenzelm@61864
   208
        (if (w != 0) Width(w) else Nil) :::
wenzelm@61864
   209
        (if (i != 0) Indent(i) else Nil))
wenzelm@61862
   210
    def unapply(markup: Markup): Option[(Int, Int)] =
wenzelm@61862
   211
      if (markup.name == name) {
wenzelm@61864
   212
        val w = Width.unapply(markup.properties).getOrElse(0)
wenzelm@61864
   213
        val i = Indent.unapply(markup.properties).getOrElse(0)
wenzelm@61864
   214
        Some((w, i))
wenzelm@61862
   215
      }
wenzelm@61862
   216
      else None
wenzelm@61862
   217
  }
wenzelm@50201
   218
wenzelm@51570
   219
  val ITEM = "item"
wenzelm@51574
   220
  val BULLET = "bullet"
wenzelm@51570
   221
wenzelm@50201
   222
  val SEPARATOR = "separator"
wenzelm@50201
   223
wenzelm@50201
   224
wenzelm@56548
   225
  /* text properties */
wenzelm@56548
   226
wenzelm@56548
   227
  val WORDS = "words"
wenzelm@50201
   228
wenzelm@50201
   229
  val HIDDEN = "hidden"
wenzelm@50201
   230
wenzelm@50201
   231
wenzelm@58048
   232
  /* misc entities */
wenzelm@50201
   233
wenzelm@50201
   234
  val CLASS = "class"
wenzelm@50201
   235
  val TYPE_NAME = "type_name"
wenzelm@50201
   236
  val FIXED = "fixed"
wenzelm@53378
   237
  val CASE = "case"
wenzelm@50201
   238
  val CONSTANT = "constant"
wenzelm@50201
   239
  val DYNAMIC_FACT = "dynamic_fact"
wenzelm@50201
   240
wenzelm@50201
   241
wenzelm@50201
   242
  /* inner syntax */
wenzelm@50201
   243
wenzelm@50201
   244
  val TFREE = "tfree"
wenzelm@50201
   245
  val TVAR = "tvar"
wenzelm@50201
   246
  val FREE = "free"
wenzelm@50201
   247
  val SKOLEM = "skolem"
wenzelm@50201
   248
  val BOUND = "bound"
wenzelm@50201
   249
  val VAR = "var"
wenzelm@50201
   250
  val NUMERAL = "numeral"
wenzelm@50201
   251
  val LITERAL = "literal"
wenzelm@50201
   252
  val DELIMITER = "delimiter"
wenzelm@50201
   253
  val INNER_STRING = "inner_string"
wenzelm@55033
   254
  val INNER_CARTOUCHE = "inner_cartouche"
wenzelm@50201
   255
  val INNER_COMMENT = "inner_comment"
wenzelm@50201
   256
wenzelm@50201
   257
  val TOKEN_RANGE = "token_range"
wenzelm@50201
   258
wenzelm@50201
   259
  val SORTING = "sorting"
wenzelm@50201
   260
  val TYPING = "typing"
wenzelm@50201
   261
wenzelm@50201
   262
  val ATTRIBUTE = "attribute"
wenzelm@50201
   263
  val METHOD = "method"
wenzelm@50201
   264
wenzelm@50201
   265
wenzelm@55550
   266
  /* antiquotations */
wenzelm@50201
   267
wenzelm@55526
   268
  val ANTIQUOTED = "antiquoted"
wenzelm@55526
   269
  val ANTIQUOTE = "antiquote"
wenzelm@55526
   270
wenzelm@50201
   271
  val ML_ANTIQUOTATION = "ML_antiquotation"
wenzelm@50201
   272
  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
wenzelm@50201
   273
  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
wenzelm@50201
   274
wenzelm@50201
   275
wenzelm@50201
   276
  /* text structure */
wenzelm@50201
   277
wenzelm@50201
   278
  val PARAGRAPH = "paragraph"
wenzelm@50545
   279
  val TEXT_FOLD = "text_fold"
wenzelm@50201
   280
wenzelm@50201
   281
wenzelm@61449
   282
  /* Markdown document structure */
wenzelm@61449
   283
wenzelm@61449
   284
  val MARKDOWN_PARAGRAPH = "markdown_paragraph"
wenzelm@61449
   285
  val Markdown_List = new Markup_String("markdown_list", "kind")
wenzelm@61449
   286
  val Markdown_Item = new Markup_Int("markdown_item", "depth")
wenzelm@61449
   287
wenzelm@61449
   288
wenzelm@60744
   289
  /* ML */
wenzelm@50201
   290
wenzelm@55505
   291
  val ML_KEYWORD1 = "ML_keyword1"
wenzelm@55505
   292
  val ML_KEYWORD2 = "ML_keyword2"
wenzelm@55505
   293
  val ML_KEYWORD3 = "ML_keyword3"
wenzelm@50201
   294
  val ML_DELIMITER = "ML_delimiter"
wenzelm@50201
   295
  val ML_TVAR = "ML_tvar"
wenzelm@50201
   296
  val ML_NUMERAL = "ML_numeral"
wenzelm@50201
   297
  val ML_CHAR = "ML_char"
wenzelm@50201
   298
  val ML_STRING = "ML_string"
wenzelm@50201
   299
  val ML_COMMENT = "ML_comment"
wenzelm@56278
   300
  val SML_STRING = "SML_string"
wenzelm@56278
   301
  val SML_COMMENT = "SML_comment"
wenzelm@50201
   302
wenzelm@50201
   303
  val ML_DEF = "ML_def"
wenzelm@50201
   304
  val ML_OPEN = "ML_open"
wenzelm@55837
   305
  val ML_STRUCTURE = "ML_structure"
wenzelm@50201
   306
  val ML_TYPING = "ML_typing"
wenzelm@50201
   307
wenzelm@60744
   308
  val ML_BREAKPOINT = "ML_breakpoint"
wenzelm@60744
   309
wenzelm@50201
   310
wenzelm@50201
   311
  /* outer syntax */
wenzelm@50201
   312
wenzelm@55744
   313
  val COMMAND = "command"
wenzelm@55744
   314
  val KEYWORD1 = "keyword1"
wenzelm@55744
   315
  val KEYWORD2 = "keyword2"
wenzelm@55765
   316
  val KEYWORD3 = "keyword3"
wenzelm@55919
   317
  val QUASI_KEYWORD = "quasi_keyword"
wenzelm@56202
   318
  val IMPROPER = "improper"
wenzelm@50201
   319
  val OPERATOR = "operator"
wenzelm@50201
   320
  val STRING = "string"
wenzelm@59081
   321
  val ALT_STRING = "alt_string"
wenzelm@50201
   322
  val VERBATIM = "verbatim"
wenzelm@55033
   323
  val CARTOUCHE = "cartouche"
wenzelm@50201
   324
  val COMMENT = "comment"
wenzelm@50201
   325
wenzelm@50201
   326
wenzelm@50201
   327
  /* timing */
wenzelm@50201
   328
wenzelm@50781
   329
  val Elapsed = new Properties.Double("elapsed")
wenzelm@50781
   330
  val CPU = new Properties.Double("cpu")
wenzelm@50781
   331
  val GC = new Properties.Double("gc")
wenzelm@50781
   332
wenzelm@50781
   333
  object Timing_Properties
wenzelm@50781
   334
  {
wenzelm@50781
   335
    def apply(timing: isabelle.Timing): Properties.T =
wenzelm@50781
   336
      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
wenzelm@51662
   337
wenzelm@50781
   338
    def unapply(props: Properties.T): Option[isabelle.Timing] =
wenzelm@50781
   339
      (props, props, props) match {
wenzelm@50781
   340
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
wenzelm@50781
   341
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@50781
   342
        case _ => None
wenzelm@50781
   343
      }
wenzelm@50781
   344
  }
wenzelm@50781
   345
wenzelm@50201
   346
  val TIMING = "timing"
wenzelm@50201
   347
wenzelm@50201
   348
  object Timing
wenzelm@50201
   349
  {
wenzelm@50781
   350
    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
wenzelm@51662
   351
wenzelm@50201
   352
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@50201
   353
      markup match {
wenzelm@50781
   354
        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
wenzelm@50201
   355
        case _ => None
wenzelm@50201
   356
      }
wenzelm@50201
   357
  }
wenzelm@50201
   358
wenzelm@50201
   359
wenzelm@51662
   360
  /* command timing */
wenzelm@51662
   361
wenzelm@51818
   362
  val COMMAND_TIMING = "command_timing"
wenzelm@51662
   363
wenzelm@51662
   364
wenzelm@50201
   365
  /* toplevel */
wenzelm@50201
   366
wenzelm@50201
   367
  val SUBGOALS = "subgoals"
wenzelm@50201
   368
  val PROOF_STATE = "proof_state"
wenzelm@50201
   369
wenzelm@50543
   370
  val GOAL = "goal"
wenzelm@50201
   371
  val SUBGOAL = "subgoal"
wenzelm@50215
   372
wenzelm@50450
   373
wenzelm@50201
   374
  /* command status */
wenzelm@50201
   375
wenzelm@50201
   376
  val TASK = "task"
wenzelm@50201
   377
wenzelm@50201
   378
  val ACCEPTED = "accepted"
wenzelm@50201
   379
  val FORKED = "forked"
wenzelm@50201
   380
  val JOINED = "joined"
wenzelm@50201
   381
  val RUNNING = "running"
wenzelm@50201
   382
  val FINISHED = "finished"
wenzelm@50201
   383
  val FAILED = "failed"
wenzelm@50201
   384
wenzelm@50201
   385
wenzelm@50201
   386
  /* interactive documents */
wenzelm@50201
   387
wenzelm@50201
   388
  val VERSION = "version"
wenzelm@50201
   389
  val ASSIGN = "assign"
wenzelm@50201
   390
wenzelm@50201
   391
wenzelm@50201
   392
  /* prover process */
wenzelm@50201
   393
wenzelm@50201
   394
  val PROVER_COMMAND = "prover_command"
wenzelm@50201
   395
  val PROVER_ARG = "prover_arg"
wenzelm@50201
   396
wenzelm@50201
   397
wenzelm@50201
   398
  /* messages */
wenzelm@50201
   399
wenzelm@50201
   400
  val INIT = "init"
wenzelm@50201
   401
  val STATUS = "status"
wenzelm@50201
   402
  val REPORT = "report"
wenzelm@50500
   403
  val RESULT = "result"
wenzelm@50201
   404
  val WRITELN = "writeln"
wenzelm@59184
   405
  val STATE = "state"
wenzelm@59184
   406
  val INFORMATION = "information"
wenzelm@50201
   407
  val TRACING = "tracing"
wenzelm@50201
   408
  val WARNING = "warning"
wenzelm@59203
   409
  val LEGACY = "legacy"
wenzelm@50201
   410
  val ERROR = "error"
wenzelm@50201
   411
  val PROTOCOL = "protocol"
wenzelm@50201
   412
  val SYSTEM = "system"
wenzelm@50201
   413
  val STDOUT = "stdout"
wenzelm@50201
   414
  val STDERR = "stderr"
wenzelm@50201
   415
  val EXIT = "exit"
wenzelm@50201
   416
wenzelm@50201
   417
  val WRITELN_MESSAGE = "writeln_message"
wenzelm@59184
   418
  val STATE_MESSAGE = "state_message"
wenzelm@59184
   419
  val INFORMATION_MESSAGE = "information_message"
wenzelm@50201
   420
  val TRACING_MESSAGE = "tracing_message"
wenzelm@50201
   421
  val WARNING_MESSAGE = "warning_message"
wenzelm@59203
   422
  val LEGACY_MESSAGE = "legacy_message"
wenzelm@50201
   423
  val ERROR_MESSAGE = "error_message"
wenzelm@50201
   424
wenzelm@59184
   425
  val messages = Map(
wenzelm@59184
   426
    WRITELN -> WRITELN_MESSAGE,
wenzelm@59184
   427
    STATE -> STATE_MESSAGE,
wenzelm@59184
   428
    INFORMATION -> INFORMATION_MESSAGE,
wenzelm@59184
   429
    TRACING -> TRACING_MESSAGE,
wenzelm@59184
   430
    WARNING -> WARNING_MESSAGE,
wenzelm@59203
   431
    LEGACY -> LEGACY_MESSAGE,
wenzelm@59184
   432
    ERROR -> ERROR_MESSAGE)
wenzelm@59184
   433
wenzelm@52876
   434
  val message: String => String = messages.withDefault((s: String) => s)
wenzelm@50201
   435
wenzelm@50201
   436
  val Return_Code = new Properties.Int("return_code")
wenzelm@50201
   437
wenzelm@50201
   438
  val NO_REPORT = "no_report"
wenzelm@50201
   439
wenzelm@50201
   440
  val BAD = "bad"
wenzelm@50201
   441
wenzelm@50500
   442
  val INTENSIFY = "intensify"
wenzelm@50500
   443
wenzelm@50500
   444
wenzelm@50500
   445
  /* active areas */
wenzelm@50500
   446
wenzelm@50715
   447
  val BROWSER = "browser"
wenzelm@50500
   448
  val GRAPHVIEW = "graphview"
wenzelm@50500
   449
wenzelm@50500
   450
  val SENDBACK = "sendback"
wenzelm@50500
   451
  val PADDING = "padding"
wenzelm@52697
   452
  val PADDING_LINE = (PADDING, "line")
wenzelm@52697
   453
  val PADDING_COMMAND = (PADDING, "command")
wenzelm@50500
   454
wenzelm@50500
   455
  val DIALOG = "dialog"
wenzelm@50503
   456
  val Result = new Properties.String(RESULT)
wenzelm@50500
   457
wenzelm@50201
   458
wenzelm@50201
   459
  /* protocol message functions */
wenzelm@50201
   460
wenzelm@50201
   461
  val FUNCTION = "function"
wenzelm@50201
   462
  val Function = new Properties.String(FUNCTION)
wenzelm@50201
   463
wenzelm@52563
   464
  val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
wenzelm@50201
   465
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
wenzelm@50201
   466
wenzelm@52111
   467
  object Protocol_Handler
wenzelm@52111
   468
  {
wenzelm@52111
   469
    def unapply(props: Properties.T): Option[(String)] =
wenzelm@52111
   470
      props match {
wenzelm@52111
   471
        case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
wenzelm@52111
   472
        case _ => None
wenzelm@52111
   473
      }
wenzelm@52111
   474
  }
wenzelm@52111
   475
wenzelm@52111
   476
  val INVOKE_SCALA = "invoke_scala"
wenzelm@50201
   477
  object Invoke_Scala
wenzelm@50201
   478
  {
wenzelm@50201
   479
    def unapply(props: Properties.T): Option[(String, String)] =
wenzelm@50201
   480
      props match {
wenzelm@52111
   481
        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
wenzelm@50201
   482
        case _ => None
wenzelm@50201
   483
      }
wenzelm@50201
   484
  }
wenzelm@52111
   485
wenzelm@52111
   486
  val CANCEL_SCALA = "cancel_scala"
wenzelm@50201
   487
  object Cancel_Scala
wenzelm@50201
   488
  {
wenzelm@50201
   489
    def unapply(props: Properties.T): Option[String] =
wenzelm@50201
   490
      props match {
wenzelm@52111
   491
        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
wenzelm@50201
   492
        case _ => None
wenzelm@50201
   493
      }
wenzelm@50201
   494
  }
wenzelm@50255
   495
wenzelm@50255
   496
  object ML_Statistics
wenzelm@50255
   497
  {
wenzelm@50255
   498
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50255
   499
      props match {
wenzelm@50255
   500
        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
wenzelm@50255
   501
        case _ => None
wenzelm@50255
   502
      }
wenzelm@50255
   503
  }
wenzelm@50975
   504
wenzelm@50975
   505
  object Task_Statistics
wenzelm@50975
   506
  {
wenzelm@50975
   507
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50975
   508
      props match {
wenzelm@50975
   509
        case (FUNCTION, "task_statistics") :: stats => Some(stats)
wenzelm@50975
   510
        case _ => None
wenzelm@50975
   511
      }
wenzelm@50975
   512
  }
lars@55316
   513
wenzelm@59367
   514
  val LOADING_THEORY = "loading_theory"
wenzelm@56616
   515
  object Loading_Theory
wenzelm@56616
   516
  {
wenzelm@56616
   517
    def unapply(props: Properties.T): Option[String] =
wenzelm@56616
   518
      props match {
wenzelm@59367
   519
        case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
wenzelm@56616
   520
        case _ => None
wenzelm@56616
   521
      }
wenzelm@56616
   522
  }
wenzelm@56616
   523
wenzelm@59366
   524
  val BUILD_THEORIES_RESULT = "build_theories_result"
wenzelm@59364
   525
  object Build_Theories_Result
wenzelm@56616
   526
  {
wenzelm@59369
   527
    def unapply(props: Properties.T): Option[String] =
wenzelm@56616
   528
      props match {
wenzelm@60831
   529
        case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id)
wenzelm@56616
   530
        case _ => None
wenzelm@56616
   531
      }
wenzelm@56616
   532
  }
wenzelm@56616
   533
wenzelm@56864
   534
  val PRINT_OPERATIONS = "print_operations"
wenzelm@56864
   535
wenzelm@55553
   536
wenzelm@60830
   537
  /* debugger output */
wenzelm@60830
   538
wenzelm@60842
   539
  val DEBUGGER_STATE = "debugger_state"
wenzelm@60842
   540
  object Debugger_State
wenzelm@60842
   541
  {
wenzelm@60842
   542
    def unapply(props: Properties.T): Option[String] =
wenzelm@60842
   543
      props match {
wenzelm@60842
   544
        case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
wenzelm@60842
   545
        case _ => None
wenzelm@60842
   546
      }
wenzelm@60842
   547
  }
wenzelm@60842
   548
wenzelm@60830
   549
  val DEBUGGER_OUTPUT = "debugger_output"
wenzelm@60830
   550
  object Debugger_Output
wenzelm@60830
   551
  {
wenzelm@60834
   552
    def unapply(props: Properties.T): Option[String] =
wenzelm@60830
   553
      props match {
wenzelm@60834
   554
        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
wenzelm@60830
   555
        case _ => None
wenzelm@60830
   556
      }
wenzelm@60830
   557
  }
wenzelm@60830
   558
wenzelm@60830
   559
lars@55316
   560
  /* simplifier trace */
lars@55316
   561
wenzelm@57594
   562
  val SIMP_TRACE_PANEL = "simp_trace_panel"
lars@55316
   563
wenzelm@55553
   564
  val SIMP_TRACE_LOG = "simp_trace_log"
wenzelm@55553
   565
  val SIMP_TRACE_STEP = "simp_trace_step"
wenzelm@55553
   566
  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
wenzelm@55553
   567
  val SIMP_TRACE_HINT = "simp_trace_hint"
wenzelm@55553
   568
  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
lars@55316
   569
wenzelm@55553
   570
  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
wenzelm@55553
   571
  object Simp_Trace_Cancel
lars@55316
   572
  {
lars@55316
   573
    def unapply(props: Properties.T): Option[Long] =
lars@55316
   574
      props match {
wenzelm@55553
   575
        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
lars@55316
   576
        case _ => None
lars@55316
   577
      }
lars@55316
   578
  }
wenzelm@45666
   579
}
wenzelm@43721
   580
wenzelm@43721
   581
wenzelm@45666
   582
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@59707
   583
{
wenzelm@59707
   584
  def markup(s: String): String =
wenzelm@59707
   585
    YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
wenzelm@59707
   586
}