src/Pure/PIDE/markup.scala
author wenzelm
Sun Mar 17 20:03:55 2019 +0100 (3 months ago ago)
changeset 70098 3235ecdcd884
parent 70070 be04e9a053a7
child 70144 82e945d472d5
permissions -rw-r--r--
more meta data from "dcterms" (superset of "dc");
wenzelm@45670
     1
/*  Title:      Pure/PIDE/markup.scala
wenzelm@27958
     2
    Author:     Makarius
wenzelm@27958
     3
wenzelm@56743
     4
Quasi-abstract 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@56743
    12
  /* elements */
wenzelm@56743
    13
wenzelm@56743
    14
  object Elements
wenzelm@56743
    15
  {
wenzelm@56743
    16
    def apply(elems: Set[String]): Elements = new Elements(elems)
wenzelm@56743
    17
    def apply(elems: String*): Elements = apply(Set(elems: _*))
wenzelm@56743
    18
    val empty: Elements = apply()
wenzelm@56743
    19
    val full: Elements =
wenzelm@56743
    20
      new Elements(Set.empty)
wenzelm@56743
    21
      {
wenzelm@56743
    22
        override def apply(elem: String): Boolean = true
wenzelm@56743
    23
        override def toString: String = "Elements.full"
wenzelm@56743
    24
      }
wenzelm@56743
    25
  }
wenzelm@56743
    26
wenzelm@56743
    27
  sealed class Elements private[Markup](private val rep: Set[String])
wenzelm@56743
    28
  {
wenzelm@56743
    29
    def apply(elem: String): Boolean = rep.contains(elem)
wenzelm@56743
    30
    def + (elem: String): Elements = new Elements(rep + elem)
wenzelm@56743
    31
    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
wenzelm@65176
    32
    def - (elem: String): Elements = new Elements(rep - elem)
wenzelm@65176
    33
    def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
wenzelm@56743
    34
    override def toString: String = rep.mkString("Elements(", ",", ")")
wenzelm@56743
    35
  }
wenzelm@56743
    36
wenzelm@56743
    37
wenzelm@45666
    38
  /* properties */
wenzelm@29184
    39
wenzelm@29184
    40
  val NAME = "name"
wenzelm@43780
    41
  val Name = new Properties.String(NAME)
wenzelm@42136
    42
wenzelm@68997
    43
  val XNAME = "xname"
wenzelm@68997
    44
  val XName = new Properties.String(XNAME)
wenzelm@68997
    45
wenzelm@29184
    46
  val KIND = "kind"
wenzelm@43780
    47
  val Kind = new Properties.String(KIND)
wenzelm@29184
    48
wenzelm@65937
    49
  val CONTENT = "content"
wenzelm@65937
    50
  val Content = new Properties.String(CONTENT)
wenzelm@65937
    51
wenzelm@60744
    52
  val SERIAL = "serial"
wenzelm@60744
    53
  val Serial = new Properties.Long(SERIAL)
wenzelm@60744
    54
wenzelm@52854
    55
  val INSTANCE = "instance"
wenzelm@52854
    56
  val Instance = new Properties.String(INSTANCE)
wenzelm@52854
    57
wenzelm@29184
    58
wenzelm@50201
    59
  /* basic markup */
wenzelm@29184
    60
wenzelm@45666
    61
  val Empty = Markup("", Nil)
wenzelm@45666
    62
  val Broken = Markup("broken", Nil)
wenzelm@50201
    63
wenzelm@55553
    64
  class Markup_String(val name: String, prop: String)
wenzelm@55553
    65
  {
wenzelm@55553
    66
    private val Prop = new Properties.String(prop)
wenzelm@55553
    67
wenzelm@55553
    68
    def apply(s: String): Markup = Markup(name, Prop(s))
wenzelm@55553
    69
    def unapply(markup: Markup): Option[String] =
wenzelm@55553
    70
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@55553
    71
  }
wenzelm@55553
    72
wenzelm@55553
    73
  class Markup_Int(val name: String, prop: String)
wenzelm@55553
    74
  {
wenzelm@55553
    75
    private val Prop = new Properties.Int(prop)
wenzelm@55553
    76
wenzelm@55553
    77
    def apply(i: Int): Markup = Markup(name, Prop(i))
wenzelm@55553
    78
    def unapply(markup: Markup): Option[Int] =
wenzelm@55553
    79
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@55553
    80
  }
wenzelm@55553
    81
wenzelm@60744
    82
  class Markup_Long(val name: String, prop: String)
wenzelm@60744
    83
  {
wenzelm@60744
    84
    private val Prop = new Properties.Long(prop)
wenzelm@60744
    85
wenzelm@60744
    86
    def apply(i: Long): Markup = Markup(name, Prop(i))
wenzelm@60744
    87
    def unapply(markup: Markup): Option[Long] =
wenzelm@60744
    88
      if (markup.name == name) Prop.unapply(markup.properties) else None
wenzelm@60744
    89
  }
wenzelm@60744
    90
wenzelm@50201
    91
wenzelm@70070
    92
  /* meta data */
wenzelm@70070
    93
wenzelm@70070
    94
  val META_TITLE = "meta_title"
wenzelm@70070
    95
  val META_CREATOR = "meta_creator"
wenzelm@70070
    96
  val META_CONTRIBUTOR = "meta_contributor"
wenzelm@70070
    97
  val META_DATE = "meta_date"
wenzelm@70070
    98
  val META_DESCRIPTION = "meta_description"
wenzelm@70098
    99
  val META_LICENSE = "meta_license"
wenzelm@70070
   100
wenzelm@70070
   101
wenzelm@50201
   102
  /* formal entities */
wenzelm@50201
   103
wenzelm@50201
   104
  val BINDING = "binding"
wenzelm@50201
   105
  val ENTITY = "entity"
wenzelm@50201
   106
wenzelm@50201
   107
  object Entity
wenzelm@50201
   108
  {
wenzelm@62986
   109
    val Def = new Properties.Long("def")
wenzelm@62986
   110
    val Ref = new Properties.Long("ref")
wenzelm@62986
   111
wenzelm@50201
   112
    def unapply(markup: Markup): Option[(String, String)] =
wenzelm@50201
   113
      markup match {
wenzelm@55553
   114
        case Markup(ENTITY, props) =>
wenzelm@63337
   115
          val kind = Kind.unapply(props).getOrElse("")
wenzelm@63337
   116
          val name = Name.unapply(props).getOrElse("")
wenzelm@63337
   117
          Some((kind, name))
wenzelm@50201
   118
        case _ => None
wenzelm@50201
   119
      }
wenzelm@50201
   120
  }
wenzelm@50201
   121
wenzelm@50201
   122
wenzelm@55672
   123
  /* completion */
wenzelm@55672
   124
wenzelm@55672
   125
  val COMPLETION = "completion"
wenzelm@55914
   126
  val NO_COMPLETION = "no_completion"
wenzelm@55672
   127
wenzelm@69571
   128
  val UPDATE = "update"
wenzelm@69571
   129
wenzelm@55672
   130
wenzelm@50201
   131
  /* position */
wenzelm@50201
   132
wenzelm@50201
   133
  val LINE = "line"
wenzelm@58978
   134
  val END_LINE = "line"
wenzelm@50201
   135
  val OFFSET = "offset"
wenzelm@50201
   136
  val END_OFFSET = "end_offset"
wenzelm@50201
   137
  val FILE = "file"
wenzelm@50201
   138
  val ID = "id"
wenzelm@50201
   139
wenzelm@50201
   140
  val DEF_LINE = "def_line"
wenzelm@50201
   141
  val DEF_OFFSET = "def_offset"
wenzelm@50201
   142
  val DEF_END_OFFSET = "def_end_offset"
wenzelm@50201
   143
  val DEF_FILE = "def_file"
wenzelm@50201
   144
  val DEF_ID = "def_id"
wenzelm@50201
   145
wenzelm@50201
   146
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
wenzelm@50201
   147
  val POSITION = "position"
wenzelm@50201
   148
wenzelm@50201
   149
wenzelm@58464
   150
  /* expression */
wenzelm@58464
   151
wenzelm@58464
   152
  val EXPRESSION = "expression"
wenzelm@62806
   153
  object Expression
wenzelm@62806
   154
  {
wenzelm@62806
   155
    def unapply(markup: Markup): Option[String] =
wenzelm@62806
   156
      markup match {
wenzelm@62806
   157
        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
wenzelm@62806
   158
        case Markup(EXPRESSION, _) => Some("")
wenzelm@62806
   159
        case _ => None
wenzelm@62806
   160
      }
wenzelm@62806
   161
  }
wenzelm@58464
   162
wenzelm@58464
   163
wenzelm@58544
   164
  /* citation */
wenzelm@58544
   165
wenzelm@58544
   166
  val CITATION = "citation"
wenzelm@58545
   167
  val Citation = new Markup_String(CITATION, NAME)
wenzelm@58544
   168
wenzelm@58544
   169
wenzelm@55552
   170
  /* embedded languages */
wenzelm@55552
   171
wenzelm@55666
   172
  val Symbols = new Properties.Boolean("symbols")
wenzelm@55666
   173
  val Antiquotes = new Properties.Boolean("antiquotes")
wenzelm@55828
   174
  val Delimited = new Properties.Boolean("delimited")
wenzelm@55615
   175
wenzelm@55552
   176
  val LANGUAGE = "language"
wenzelm@55615
   177
  object Language
wenzelm@55615
   178
  {
wenzelm@67336
   179
    val DOCUMENT = "document"
wenzelm@55616
   180
    val ML = "ML"
wenzelm@56278
   181
    val SML = "SML"
wenzelm@56843
   182
    val PATH = "path"
wenzelm@55616
   183
    val UNKNOWN = "unknown"
wenzelm@55616
   184
wenzelm@55828
   185
    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
wenzelm@55615
   186
      markup match {
wenzelm@55615
   187
        case Markup(LANGUAGE, props) =>
wenzelm@55828
   188
          (props, props, props, props) match {
wenzelm@55828
   189
            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
wenzelm@55828
   190
              Some((name, symbols, antiquotes, delimited))
wenzelm@55615
   191
            case _ => None
wenzelm@55615
   192
          }
wenzelm@55615
   193
        case _ => None
wenzelm@55615
   194
      }
wenzelm@55615
   195
  }
wenzelm@55552
   196
wenzelm@55552
   197
wenzelm@54702
   198
  /* external resources */
wenzelm@50201
   199
wenzelm@50201
   200
  val PATH = "path"
wenzelm@55553
   201
  val Path = new Markup_String(PATH, NAME)
wenzelm@50201
   202
wenzelm@54702
   203
  val URL = "url"
wenzelm@55553
   204
  val Url = new Markup_String(URL, NAME)
wenzelm@54702
   205
wenzelm@61660
   206
  val DOC = "doc"
wenzelm@61660
   207
  val Doc = new Markup_String(DOC, NAME)
wenzelm@61660
   208
wenzelm@50201
   209
wenzelm@50201
   210
  /* pretty printing */
wenzelm@50201
   211
wenzelm@61866
   212
  val Consistent = new Properties.Boolean("consistent")
wenzelm@61864
   213
  val Indent = new Properties.Int("indent")
wenzelm@61866
   214
  val Width = new Properties.Int("width")
wenzelm@61864
   215
wenzelm@61866
   216
  object Block
wenzelm@61866
   217
  {
wenzelm@61866
   218
    val name = "block"
wenzelm@61866
   219
    def apply(c: Boolean, i: Int): Markup =
wenzelm@61866
   220
      Markup(name,
wenzelm@61866
   221
        (if (c) Consistent(c) else Nil) :::
wenzelm@61866
   222
        (if (i != 0) Indent(i) else Nil))
wenzelm@61866
   223
    def unapply(markup: Markup): Option[(Boolean, Int)] =
wenzelm@61866
   224
      if (markup.name == name) {
wenzelm@61866
   225
        val c = Consistent.unapply(markup.properties).getOrElse(false)
wenzelm@61866
   226
        val i = Indent.unapply(markup.properties).getOrElse(0)
wenzelm@61866
   227
        Some((c, i))
wenzelm@61866
   228
      }
wenzelm@61866
   229
      else None
wenzelm@61866
   230
  }
wenzelm@61866
   231
wenzelm@61864
   232
  object Break
wenzelm@61864
   233
  {
wenzelm@61864
   234
    val name = "break"
wenzelm@61866
   235
    def apply(w: Int, i: Int): Markup =
wenzelm@61866
   236
      Markup(name,
wenzelm@61866
   237
        (if (w != 0) Width(w) else Nil) :::
wenzelm@61866
   238
        (if (i != 0) Indent(i) else Nil))
wenzelm@61864
   239
    def unapply(markup: Markup): Option[(Int, Int)] =
wenzelm@61864
   240
      if (markup.name == name) {
wenzelm@61866
   241
        val w = Width.unapply(markup.properties).getOrElse(0)
wenzelm@61866
   242
        val i = Indent.unapply(markup.properties).getOrElse(0)
wenzelm@61866
   243
        Some((w, i))
wenzelm@61864
   244
      }
wenzelm@61864
   245
      else None
wenzelm@61864
   246
  }
wenzelm@50201
   247
wenzelm@51570
   248
  val ITEM = "item"
wenzelm@51574
   249
  val BULLET = "bullet"
wenzelm@51570
   250
wenzelm@50201
   251
  val SEPARATOR = "separator"
wenzelm@50201
   252
wenzelm@50201
   253
wenzelm@56548
   254
  /* text properties */
wenzelm@56548
   255
wenzelm@56548
   256
  val WORDS = "words"
wenzelm@50201
   257
wenzelm@50201
   258
  val HIDDEN = "hidden"
wenzelm@50201
   259
wenzelm@68298
   260
  val DELETE = "delete"
wenzelm@68298
   261
wenzelm@50201
   262
wenzelm@58048
   263
  /* misc entities */
wenzelm@50201
   264
wenzelm@50201
   265
  val CLASS = "class"
wenzelm@50201
   266
  val TYPE_NAME = "type_name"
wenzelm@50201
   267
  val FIXED = "fixed"
wenzelm@53378
   268
  val CASE = "case"
wenzelm@50201
   269
  val CONSTANT = "constant"
wenzelm@50201
   270
  val DYNAMIC_FACT = "dynamic_fact"
wenzelm@50201
   271
wenzelm@50201
   272
wenzelm@50201
   273
  /* inner syntax */
wenzelm@50201
   274
wenzelm@50201
   275
  val TFREE = "tfree"
wenzelm@50201
   276
  val TVAR = "tvar"
wenzelm@50201
   277
  val FREE = "free"
wenzelm@50201
   278
  val SKOLEM = "skolem"
wenzelm@50201
   279
  val BOUND = "bound"
wenzelm@50201
   280
  val VAR = "var"
wenzelm@50201
   281
  val NUMERAL = "numeral"
wenzelm@50201
   282
  val LITERAL = "literal"
wenzelm@50201
   283
  val DELIMITER = "delimiter"
wenzelm@50201
   284
  val INNER_STRING = "inner_string"
wenzelm@55033
   285
  val INNER_CARTOUCHE = "inner_cartouche"
wenzelm@50201
   286
wenzelm@50201
   287
  val TOKEN_RANGE = "token_range"
wenzelm@50201
   288
wenzelm@50201
   289
  val SORTING = "sorting"
wenzelm@50201
   290
  val TYPING = "typing"
wenzelm@63347
   291
  val CLASS_PARAMETER = "class_parameter"
wenzelm@50201
   292
wenzelm@50201
   293
  val ATTRIBUTE = "attribute"
wenzelm@50201
   294
  val METHOD = "method"
wenzelm@50201
   295
wenzelm@50201
   296
wenzelm@55552
   297
  /* antiquotations */
wenzelm@50201
   298
wenzelm@55526
   299
  val ANTIQUOTED = "antiquoted"
wenzelm@55526
   300
  val ANTIQUOTE = "antiquote"
wenzelm@55526
   301
wenzelm@50201
   302
  val ML_ANTIQUOTATION = "ML_antiquotation"
wenzelm@50201
   303
  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
wenzelm@50201
   304
  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
wenzelm@50201
   305
wenzelm@50201
   306
wenzelm@50201
   307
  /* text structure */
wenzelm@50201
   308
wenzelm@50201
   309
  val PARAGRAPH = "paragraph"
wenzelm@50545
   310
  val TEXT_FOLD = "text_fold"
wenzelm@50201
   311
wenzelm@50201
   312
wenzelm@61449
   313
  /* Markdown document structure */
wenzelm@61449
   314
wenzelm@61449
   315
  val MARKDOWN_PARAGRAPH = "markdown_paragraph"
wenzelm@67323
   316
  val MARKDOWN_ITEM = "markdown_item"
wenzelm@67336
   317
  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
wenzelm@61449
   318
  val Markdown_List = new Markup_String("markdown_list", "kind")
wenzelm@67336
   319
wenzelm@67336
   320
  val ITEMIZE = "itemize"
wenzelm@67336
   321
  val ENUMERATE = "enumerate"
wenzelm@67336
   322
  val DESCRIPTION = "description"
wenzelm@61449
   323
wenzelm@61449
   324
wenzelm@60744
   325
  /* ML */
wenzelm@50201
   326
wenzelm@55505
   327
  val ML_KEYWORD1 = "ML_keyword1"
wenzelm@55505
   328
  val ML_KEYWORD2 = "ML_keyword2"
wenzelm@55505
   329
  val ML_KEYWORD3 = "ML_keyword3"
wenzelm@50201
   330
  val ML_DELIMITER = "ML_delimiter"
wenzelm@50201
   331
  val ML_TVAR = "ML_tvar"
wenzelm@50201
   332
  val ML_NUMERAL = "ML_numeral"
wenzelm@50201
   333
  val ML_CHAR = "ML_char"
wenzelm@50201
   334
  val ML_STRING = "ML_string"
wenzelm@50201
   335
  val ML_COMMENT = "ML_comment"
wenzelm@50201
   336
wenzelm@50201
   337
  val ML_DEF = "ML_def"
wenzelm@50201
   338
  val ML_OPEN = "ML_open"
wenzelm@55837
   339
  val ML_STRUCTURE = "ML_structure"
wenzelm@50201
   340
  val ML_TYPING = "ML_typing"
wenzelm@50201
   341
wenzelm@60744
   342
  val ML_BREAKPOINT = "ML_breakpoint"
wenzelm@60744
   343
wenzelm@50201
   344
wenzelm@50201
   345
  /* outer syntax */
wenzelm@50201
   346
wenzelm@55744
   347
  val COMMAND = "command"
wenzelm@66044
   348
  val KEYWORD = "keyword"
wenzelm@55744
   349
  val KEYWORD1 = "keyword1"
wenzelm@55744
   350
  val KEYWORD2 = "keyword2"
wenzelm@55765
   351
  val KEYWORD3 = "keyword3"
wenzelm@55919
   352
  val QUASI_KEYWORD = "quasi_keyword"
wenzelm@56202
   353
  val IMPROPER = "improper"
wenzelm@50201
   354
  val OPERATOR = "operator"
wenzelm@50201
   355
  val STRING = "string"
wenzelm@59081
   356
  val ALT_STRING = "alt_string"
wenzelm@50201
   357
  val VERBATIM = "verbatim"
wenzelm@55033
   358
  val CARTOUCHE = "cartouche"
wenzelm@50201
   359
  val COMMENT = "comment"
wenzelm@50201
   360
wenzelm@50201
   361
wenzelm@69330
   362
  /* comments */
wenzelm@69330
   363
wenzelm@69330
   364
  val COMMENT1 = "comment1"
wenzelm@69330
   365
  val COMMENT2 = "comment2"
wenzelm@69330
   366
  val COMMENT3 = "comment3"
wenzelm@69330
   367
wenzelm@69330
   368
wenzelm@50201
   369
  /* timing */
wenzelm@50201
   370
wenzelm@50781
   371
  val Elapsed = new Properties.Double("elapsed")
wenzelm@50781
   372
  val CPU = new Properties.Double("cpu")
wenzelm@50781
   373
  val GC = new Properties.Double("gc")
wenzelm@50781
   374
wenzelm@50781
   375
  object Timing_Properties
wenzelm@50781
   376
  {
wenzelm@50781
   377
    def apply(timing: isabelle.Timing): Properties.T =
wenzelm@50781
   378
      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
wenzelm@51662
   379
wenzelm@50781
   380
    def unapply(props: Properties.T): Option[isabelle.Timing] =
wenzelm@50781
   381
      (props, props, props) match {
wenzelm@50781
   382
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
wenzelm@50781
   383
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@50781
   384
        case _ => None
wenzelm@50781
   385
      }
wenzelm@50781
   386
  }
wenzelm@50781
   387
wenzelm@50201
   388
  val TIMING = "timing"
wenzelm@50201
   389
wenzelm@50201
   390
  object Timing
wenzelm@50201
   391
  {
wenzelm@50781
   392
    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
wenzelm@51662
   393
wenzelm@50201
   394
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@50201
   395
      markup match {
wenzelm@50781
   396
        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
wenzelm@50201
   397
        case _ => None
wenzelm@50201
   398
      }
wenzelm@50201
   399
  }
wenzelm@50201
   400
wenzelm@50201
   401
wenzelm@65317
   402
  /* process result */
wenzelm@65317
   403
wenzelm@65317
   404
  val Return_Code = new Properties.Int("return_code")
wenzelm@65317
   405
wenzelm@65317
   406
  object Process_Result
wenzelm@65317
   407
  {
wenzelm@65317
   408
    def apply(result: Process_Result): Properties.T =
wenzelm@65317
   409
      Return_Code(result.rc) :::
wenzelm@65317
   410
        (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
wenzelm@65317
   411
wenzelm@65317
   412
    def unapply(props: Properties.T): Option[Process_Result] =
wenzelm@65317
   413
      props match {
wenzelm@65317
   414
        case Return_Code(rc) =>
wenzelm@65317
   415
          val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
wenzelm@65317
   416
          Some(isabelle.Process_Result(rc, timing = timing))
wenzelm@65317
   417
        case _ => None
wenzelm@65317
   418
      }
wenzelm@65317
   419
  }
wenzelm@65317
   420
wenzelm@65317
   421
wenzelm@63474
   422
  /* command indentation */
wenzelm@63474
   423
wenzelm@63474
   424
  object Command_Indent
wenzelm@63474
   425
  {
wenzelm@63474
   426
    val name = "command_indent"
wenzelm@63474
   427
    def unapply(markup: Markup): Option[Int] =
wenzelm@63474
   428
      if (markup.name == name) Indent.unapply(markup.properties) else None
wenzelm@63474
   429
  }
wenzelm@63474
   430
wenzelm@63474
   431
wenzelm@63474
   432
  /* goals */
wenzelm@50201
   433
wenzelm@50543
   434
  val GOAL = "goal"
wenzelm@50201
   435
  val SUBGOAL = "subgoal"
wenzelm@50215
   436
wenzelm@50450
   437
wenzelm@50201
   438
  /* command status */
wenzelm@50201
   439
wenzelm@50201
   440
  val TASK = "task"
wenzelm@50201
   441
wenzelm@50201
   442
  val ACCEPTED = "accepted"
wenzelm@50201
   443
  val FORKED = "forked"
wenzelm@50201
   444
  val JOINED = "joined"
wenzelm@50201
   445
  val RUNNING = "running"
wenzelm@50201
   446
  val FINISHED = "finished"
wenzelm@50201
   447
  val FAILED = "failed"
wenzelm@68871
   448
  val CANCELED = "canceled"
wenzelm@68324
   449
  val INITIALIZED = "initialized"
wenzelm@68884
   450
  val FINALIZED = "finalized"
wenzelm@66382
   451
  val CONSOLIDATED = "consolidated"
wenzelm@50201
   452
wenzelm@50201
   453
wenzelm@50201
   454
  /* interactive documents */
wenzelm@50201
   455
wenzelm@50201
   456
  val VERSION = "version"
wenzelm@50201
   457
  val ASSIGN = "assign"
wenzelm@50201
   458
wenzelm@50201
   459
wenzelm@50201
   460
  /* prover process */
wenzelm@50201
   461
wenzelm@50201
   462
  val PROVER_COMMAND = "prover_command"
wenzelm@50201
   463
  val PROVER_ARG = "prover_arg"
wenzelm@50201
   464
wenzelm@50201
   465
wenzelm@50201
   466
  /* messages */
wenzelm@50201
   467
wenzelm@50201
   468
  val INIT = "init"
wenzelm@50201
   469
  val STATUS = "status"
wenzelm@50201
   470
  val REPORT = "report"
wenzelm@50500
   471
  val RESULT = "result"
wenzelm@50201
   472
  val WRITELN = "writeln"
wenzelm@59184
   473
  val STATE = "state"
wenzelm@59184
   474
  val INFORMATION = "information"
wenzelm@50201
   475
  val TRACING = "tracing"
wenzelm@50201
   476
  val WARNING = "warning"
wenzelm@59203
   477
  val LEGACY = "legacy"
wenzelm@50201
   478
  val ERROR = "error"
wenzelm@68770
   479
  val NODES_STATUS = "nodes_status"
wenzelm@50201
   480
  val PROTOCOL = "protocol"
wenzelm@50201
   481
  val SYSTEM = "system"
wenzelm@50201
   482
  val STDOUT = "stdout"
wenzelm@50201
   483
  val STDERR = "stderr"
wenzelm@50201
   484
  val EXIT = "exit"
wenzelm@50201
   485
wenzelm@50201
   486
  val WRITELN_MESSAGE = "writeln_message"
wenzelm@59184
   487
  val STATE_MESSAGE = "state_message"
wenzelm@59184
   488
  val INFORMATION_MESSAGE = "information_message"
wenzelm@50201
   489
  val TRACING_MESSAGE = "tracing_message"
wenzelm@50201
   490
  val WARNING_MESSAGE = "warning_message"
wenzelm@59203
   491
  val LEGACY_MESSAGE = "legacy_message"
wenzelm@50201
   492
  val ERROR_MESSAGE = "error_message"
wenzelm@50201
   493
wenzelm@59184
   494
  val messages = Map(
wenzelm@59184
   495
    WRITELN -> WRITELN_MESSAGE,
wenzelm@59184
   496
    STATE -> STATE_MESSAGE,
wenzelm@59184
   497
    INFORMATION -> INFORMATION_MESSAGE,
wenzelm@59184
   498
    TRACING -> TRACING_MESSAGE,
wenzelm@59184
   499
    WARNING -> WARNING_MESSAGE,
wenzelm@59203
   500
    LEGACY -> LEGACY_MESSAGE,
wenzelm@59184
   501
    ERROR -> ERROR_MESSAGE)
wenzelm@59184
   502
wenzelm@52876
   503
  val message: String => String = messages.withDefault((s: String) => s)
wenzelm@50201
   504
wenzelm@50201
   505
  val NO_REPORT = "no_report"
wenzelm@50201
   506
wenzelm@50201
   507
  val BAD = "bad"
wenzelm@50201
   508
wenzelm@50500
   509
  val INTENSIFY = "intensify"
wenzelm@50500
   510
wenzelm@50500
   511
wenzelm@50500
   512
  /* active areas */
wenzelm@50500
   513
wenzelm@50715
   514
  val BROWSER = "browser"
wenzelm@50500
   515
  val GRAPHVIEW = "graphview"
wenzelm@69666
   516
  val THEORY_EXPORTS = "theory_exports"
wenzelm@50500
   517
wenzelm@50500
   518
  val SENDBACK = "sendback"
wenzelm@50500
   519
  val PADDING = "padding"
wenzelm@52697
   520
  val PADDING_LINE = (PADDING, "line")
wenzelm@52697
   521
  val PADDING_COMMAND = (PADDING, "command")
wenzelm@50500
   522
wenzelm@50500
   523
  val DIALOG = "dialog"
wenzelm@50503
   524
  val Result = new Properties.String(RESULT)
wenzelm@50500
   525
wenzelm@63681
   526
  val JEDIT_ACTION = "jedit_action"
wenzelm@63681
   527
wenzelm@50201
   528
wenzelm@50201
   529
  /* protocol message functions */
wenzelm@50201
   530
wenzelm@50201
   531
  val FUNCTION = "function"
wenzelm@50201
   532
  val Function = new Properties.String(FUNCTION)
wenzelm@50201
   533
wenzelm@66942
   534
  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
wenzelm@66942
   535
  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
wenzelm@66942
   536
wenzelm@52563
   537
  val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
wenzelm@50201
   538
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
wenzelm@50201
   539
wenzelm@52111
   540
  object Protocol_Handler
wenzelm@52111
   541
  {
wenzelm@52111
   542
    def unapply(props: Properties.T): Option[(String)] =
wenzelm@52111
   543
      props match {
wenzelm@52111
   544
        case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
wenzelm@52111
   545
        case _ => None
wenzelm@52111
   546
      }
wenzelm@52111
   547
  }
wenzelm@52111
   548
wenzelm@52111
   549
  val INVOKE_SCALA = "invoke_scala"
wenzelm@50201
   550
  object Invoke_Scala
wenzelm@50201
   551
  {
wenzelm@50201
   552
    def unapply(props: Properties.T): Option[(String, String)] =
wenzelm@50201
   553
      props match {
wenzelm@52111
   554
        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
wenzelm@50201
   555
        case _ => None
wenzelm@50201
   556
      }
wenzelm@50201
   557
  }
wenzelm@52111
   558
wenzelm@52111
   559
  val CANCEL_SCALA = "cancel_scala"
wenzelm@50201
   560
  object Cancel_Scala
wenzelm@50201
   561
  {
wenzelm@50201
   562
    def unapply(props: Properties.T): Option[String] =
wenzelm@50201
   563
      props match {
wenzelm@52111
   564
        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
wenzelm@50201
   565
        case _ => None
wenzelm@50201
   566
      }
wenzelm@50201
   567
  }
wenzelm@50255
   568
wenzelm@50255
   569
  object ML_Statistics
wenzelm@50255
   570
  {
wenzelm@50255
   571
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50255
   572
      props match {
wenzelm@66872
   573
        case (FUNCTION, "ML_statistics") :: props => Some(props)
wenzelm@50255
   574
        case _ => None
wenzelm@50255
   575
      }
wenzelm@50255
   576
  }
wenzelm@50975
   577
wenzelm@50975
   578
  object Task_Statistics
wenzelm@50975
   579
  {
wenzelm@50975
   580
    def unapply(props: Properties.T): Option[Properties.T] =
wenzelm@50975
   581
      props match {
wenzelm@66872
   582
        case (FUNCTION, "task_statistics") :: props => Some(props)
wenzelm@50975
   583
        case _ => None
wenzelm@50975
   584
      }
wenzelm@50975
   585
  }
lars@55316
   586
wenzelm@59367
   587
  val LOADING_THEORY = "loading_theory"
wenzelm@56616
   588
  object Loading_Theory
wenzelm@56616
   589
  {
wenzelm@56616
   590
    def unapply(props: Properties.T): Option[String] =
wenzelm@56616
   591
      props match {
wenzelm@59367
   592
        case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
wenzelm@56616
   593
        case _ => None
wenzelm@56616
   594
      }
wenzelm@56616
   595
  }
wenzelm@56616
   596
wenzelm@69967
   597
  val BUILD_SESSION_FINISHED = "build_session_finished"
wenzelm@69967
   598
  val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
wenzelm@69967
   599
wenzelm@69967
   600
  val PRINT_OPERATIONS = "print_operations"
wenzelm@69967
   601
wenzelm@69967
   602
wenzelm@69967
   603
wenzelm@69967
   604
  /* export */
wenzelm@69967
   605
wenzelm@68090
   606
  val EXPORT = "export"
wenzelm@69967
   607
wenzelm@68090
   608
  object Export
wenzelm@68090
   609
  {
wenzelm@68104
   610
    sealed case class Args(
wenzelm@69967
   611
      id: Option[String],
wenzelm@69967
   612
      serial: Long,
wenzelm@69967
   613
      theory_name: String,
wenzelm@69967
   614
      name: String,
wenzelm@69967
   615
      executable: Boolean,
wenzelm@69967
   616
      compress: Boolean)
wenzelm@68090
   617
wenzelm@68090
   618
    val THEORY_NAME = "theory_name"
wenzelm@69967
   619
    val EXECUTABLE = "executable"
wenzelm@68090
   620
    val COMPRESS = "compress"
wenzelm@68090
   621
wenzelm@68148
   622
    def dest_inline(props: Properties.T): Option[(Args, Path)] =
wenzelm@68090
   623
      props match {
wenzelm@68090
   624
        case
wenzelm@68104
   625
          List(
wenzelm@68104
   626
            (SERIAL, Value.Long(serial)),
wenzelm@68104
   627
            (THEORY_NAME, theory_name),
wenzelm@68104
   628
            (NAME, name),
wenzelm@69967
   629
            (EXECUTABLE, Value.Boolean(executable)),
wenzelm@68104
   630
            (COMPRESS, Value.Boolean(compress)),
wenzelm@68148
   631
            (FILE, file)) if isabelle.Path.is_valid(file) =>
wenzelm@69967
   632
          val args = Args(None, serial, theory_name, name, executable, compress)
wenzelm@69967
   633
          Some((args, isabelle.Path.explode(file)))
wenzelm@68090
   634
        case _ => None
wenzelm@68090
   635
      }
wenzelm@68090
   636
wenzelm@68090
   637
    def unapply(props: Properties.T): Option[Args] =
wenzelm@68090
   638
      props match {
wenzelm@68104
   639
        case List(
wenzelm@68104
   640
            (FUNCTION, EXPORT),
wenzelm@68104
   641
            (ID, id),
wenzelm@68104
   642
            (SERIAL, Value.Long(serial)),
wenzelm@68104
   643
            (THEORY_NAME, theory_name),
wenzelm@68104
   644
            (NAME, name),
wenzelm@69967
   645
            (EXECUTABLE, Value.Boolean(executable)),
wenzelm@68104
   646
            (COMPRESS, Value.Boolean(compress))) =>
wenzelm@69967
   647
          Some(Args(proper_string(id), serial, theory_name, name, executable, compress))
wenzelm@68090
   648
        case _ => None
wenzelm@68090
   649
      }
wenzelm@68090
   650
  }
wenzelm@68090
   651
wenzelm@55555
   652
wenzelm@60830
   653
  /* debugger output */
wenzelm@60830
   654
wenzelm@60842
   655
  val DEBUGGER_STATE = "debugger_state"
wenzelm@60842
   656
  object Debugger_State
wenzelm@60842
   657
  {
wenzelm@60842
   658
    def unapply(props: Properties.T): Option[String] =
wenzelm@60842
   659
      props match {
wenzelm@60842
   660
        case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
wenzelm@60842
   661
        case _ => None
wenzelm@60842
   662
      }
wenzelm@60842
   663
  }
wenzelm@60842
   664
wenzelm@60830
   665
  val DEBUGGER_OUTPUT = "debugger_output"
wenzelm@60830
   666
  object Debugger_Output
wenzelm@60830
   667
  {
wenzelm@60834
   668
    def unapply(props: Properties.T): Option[String] =
wenzelm@60830
   669
      props match {
wenzelm@60834
   670
        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
wenzelm@60830
   671
        case _ => None
wenzelm@60830
   672
      }
wenzelm@60830
   673
  }
wenzelm@60830
   674
wenzelm@60830
   675
lars@55316
   676
  /* simplifier trace */
lars@55316
   677
wenzelm@57597
   678
  val SIMP_TRACE_PANEL = "simp_trace_panel"
lars@55316
   679
wenzelm@55555
   680
  val SIMP_TRACE_LOG = "simp_trace_log"
wenzelm@55555
   681
  val SIMP_TRACE_STEP = "simp_trace_step"
wenzelm@55555
   682
  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
wenzelm@55555
   683
  val SIMP_TRACE_HINT = "simp_trace_hint"
wenzelm@55555
   684
  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
lars@55316
   685
wenzelm@55555
   686
  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
wenzelm@55555
   687
  object Simp_Trace_Cancel
lars@55316
   688
  {
lars@55316
   689
    def unapply(props: Properties.T): Option[Long] =
lars@55316
   690
      props match {
wenzelm@55555
   691
        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
lars@55316
   692
        case _ => None
lars@55316
   693
      }
lars@55316
   694
  }
wenzelm@65335
   695
wenzelm@65335
   696
wenzelm@65335
   697
  /* XML data representation */
wenzelm@65335
   698
wenzelm@65335
   699
  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
wenzelm@65335
   700
  {
wenzelm@65335
   701
    import XML.Encode._
wenzelm@65335
   702
    pair(string, properties)((markup.name, markup.properties))
wenzelm@65335
   703
  }
wenzelm@65335
   704
wenzelm@65335
   705
  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
wenzelm@65335
   706
  {
wenzelm@65335
   707
    import XML.Decode._
wenzelm@65335
   708
    val (name, props) = pair(string, properties)(body)
wenzelm@65335
   709
    Markup(name, props)
wenzelm@65335
   710
  }
wenzelm@45666
   711
}
wenzelm@43721
   712
wenzelm@43721
   713
wenzelm@45666
   714
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@59709
   715
{
wenzelm@59709
   716
  def markup(s: String): String =
wenzelm@59709
   717
    YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
wenzelm@64358
   718
wenzelm@64358
   719
  def update_properties(more_props: Properties.T): Markup =
wenzelm@64358
   720
    if (more_props.isEmpty) this
wenzelm@64358
   721
    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
wenzelm@65753
   722
wenzelm@65753
   723
  def + (entry: Properties.Entry): Markup =
wenzelm@65753
   724
    Markup(name, Properties.put(properties, entry))
wenzelm@59709
   725
}