src/Pure/PIDE/markup.scala
author wenzelm
Sun Nov 25 19:49:24 2012 +0100 (2012-11-25)
changeset 50201 c26369c9eda6
parent 49613 2f6986e2ef06
child 50215 97959912840a
permissions -rw-r--r--
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
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@29184
    21
wenzelm@50201
    22
  /* basic markup */
wenzelm@29184
    23
wenzelm@45666
    24
  val Empty = Markup("", Nil)
wenzelm@45666
    25
  val Broken = Markup("broken", Nil)
wenzelm@50201
    26
wenzelm@50201
    27
wenzelm@50201
    28
  /* formal entities */
wenzelm@50201
    29
wenzelm@50201
    30
  val BINDING = "binding"
wenzelm@50201
    31
  val ENTITY = "entity"
wenzelm@50201
    32
  val DEF = "def"
wenzelm@50201
    33
  val REF = "ref"
wenzelm@50201
    34
wenzelm@50201
    35
  object Entity
wenzelm@50201
    36
  {
wenzelm@50201
    37
    def unapply(markup: Markup): Option[(String, String)] =
wenzelm@50201
    38
      markup match {
wenzelm@50201
    39
        case Markup(ENTITY, props @ Kind(kind)) =>
wenzelm@50201
    40
          props match {
wenzelm@50201
    41
            case Name(name) => Some(kind, name)
wenzelm@50201
    42
            case _ => None
wenzelm@50201
    43
          }
wenzelm@50201
    44
        case _ => None
wenzelm@50201
    45
      }
wenzelm@50201
    46
  }
wenzelm@50201
    47
wenzelm@50201
    48
wenzelm@50201
    49
  /* position */
wenzelm@50201
    50
wenzelm@50201
    51
  val LINE = "line"
wenzelm@50201
    52
  val OFFSET = "offset"
wenzelm@50201
    53
  val END_OFFSET = "end_offset"
wenzelm@50201
    54
  val FILE = "file"
wenzelm@50201
    55
  val ID = "id"
wenzelm@50201
    56
wenzelm@50201
    57
  val DEF_LINE = "def_line"
wenzelm@50201
    58
  val DEF_OFFSET = "def_offset"
wenzelm@50201
    59
  val DEF_END_OFFSET = "def_end_offset"
wenzelm@50201
    60
  val DEF_FILE = "def_file"
wenzelm@50201
    61
  val DEF_ID = "def_id"
wenzelm@50201
    62
wenzelm@50201
    63
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
wenzelm@50201
    64
  val POSITION = "position"
wenzelm@50201
    65
wenzelm@50201
    66
wenzelm@50201
    67
  /* path */
wenzelm@50201
    68
wenzelm@50201
    69
  val PATH = "path"
wenzelm@50201
    70
wenzelm@50201
    71
  object Path
wenzelm@50201
    72
  {
wenzelm@50201
    73
    def unapply(markup: Markup): Option[String] =
wenzelm@50201
    74
      markup match {
wenzelm@50201
    75
        case Markup(PATH, Name(name)) => Some(name)
wenzelm@50201
    76
        case _ => None
wenzelm@50201
    77
      }
wenzelm@50201
    78
  }
wenzelm@50201
    79
wenzelm@50201
    80
wenzelm@50201
    81
  /* pretty printing */
wenzelm@50201
    82
wenzelm@50201
    83
  val Indent = new Properties.Int("indent")
wenzelm@50201
    84
  val BLOCK = "block"
wenzelm@50201
    85
  val Width = new Properties.Int("width")
wenzelm@50201
    86
  val BREAK = "break"
wenzelm@50201
    87
wenzelm@50201
    88
  val SEPARATOR = "separator"
wenzelm@50201
    89
wenzelm@50201
    90
wenzelm@50201
    91
  /* hidden text */
wenzelm@50201
    92
wenzelm@50201
    93
  val HIDDEN = "hidden"
wenzelm@50201
    94
wenzelm@50201
    95
wenzelm@50201
    96
  /* logical entities */
wenzelm@50201
    97
wenzelm@50201
    98
  val CLASS = "class"
wenzelm@50201
    99
  val TYPE_NAME = "type_name"
wenzelm@50201
   100
  val FIXED = "fixed"
wenzelm@50201
   101
  val CONSTANT = "constant"
wenzelm@50201
   102
wenzelm@50201
   103
  val DYNAMIC_FACT = "dynamic_fact"
wenzelm@50201
   104
wenzelm@50201
   105
wenzelm@50201
   106
  /* inner syntax */
wenzelm@50201
   107
wenzelm@50201
   108
  val TFREE = "tfree"
wenzelm@50201
   109
  val TVAR = "tvar"
wenzelm@50201
   110
  val FREE = "free"
wenzelm@50201
   111
  val SKOLEM = "skolem"
wenzelm@50201
   112
  val BOUND = "bound"
wenzelm@50201
   113
  val VAR = "var"
wenzelm@50201
   114
  val NUMERAL = "numeral"
wenzelm@50201
   115
  val LITERAL = "literal"
wenzelm@50201
   116
  val DELIMITER = "delimiter"
wenzelm@50201
   117
  val INNER_STRING = "inner_string"
wenzelm@50201
   118
  val INNER_COMMENT = "inner_comment"
wenzelm@50201
   119
wenzelm@50201
   120
  val TOKEN_RANGE = "token_range"
wenzelm@50201
   121
wenzelm@50201
   122
  val SORT = "sort"
wenzelm@50201
   123
  val TYP = "typ"
wenzelm@50201
   124
  val TERM = "term"
wenzelm@50201
   125
  val PROP = "prop"
wenzelm@50201
   126
wenzelm@50201
   127
  val SORTING = "sorting"
wenzelm@50201
   128
  val TYPING = "typing"
wenzelm@50201
   129
wenzelm@50201
   130
  val ATTRIBUTE = "attribute"
wenzelm@50201
   131
  val METHOD = "method"
wenzelm@50201
   132
wenzelm@50201
   133
wenzelm@50201
   134
  /* embedded source text */
wenzelm@50201
   135
wenzelm@50201
   136
  val ML_SOURCE = "ML_source"
wenzelm@50201
   137
  val DOCUMENT_SOURCE = "document_source"
wenzelm@50201
   138
wenzelm@50201
   139
  val ANTIQ = "antiq"
wenzelm@50201
   140
  val ML_ANTIQUOTATION = "ML_antiquotation"
wenzelm@50201
   141
  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
wenzelm@50201
   142
  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
wenzelm@50201
   143
wenzelm@50201
   144
wenzelm@50201
   145
  /* text structure */
wenzelm@50201
   146
wenzelm@50201
   147
  val PARAGRAPH = "paragraph"
wenzelm@50201
   148
wenzelm@50201
   149
wenzelm@50201
   150
  /* ML syntax */
wenzelm@50201
   151
wenzelm@50201
   152
  val ML_KEYWORD = "ML_keyword"
wenzelm@50201
   153
  val ML_DELIMITER = "ML_delimiter"
wenzelm@50201
   154
  val ML_TVAR = "ML_tvar"
wenzelm@50201
   155
  val ML_NUMERAL = "ML_numeral"
wenzelm@50201
   156
  val ML_CHAR = "ML_char"
wenzelm@50201
   157
  val ML_STRING = "ML_string"
wenzelm@50201
   158
  val ML_COMMENT = "ML_comment"
wenzelm@50201
   159
wenzelm@50201
   160
  val ML_DEF = "ML_def"
wenzelm@50201
   161
  val ML_OPEN = "ML_open"
wenzelm@50201
   162
  val ML_STRUCT = "ML_struct"
wenzelm@50201
   163
  val ML_TYPING = "ML_typing"
wenzelm@50201
   164
wenzelm@50201
   165
wenzelm@50201
   166
  /* outer syntax */
wenzelm@50201
   167
wenzelm@50201
   168
  val KEYWORD = "keyword"
wenzelm@50201
   169
  val OPERATOR = "operator"
wenzelm@50201
   170
  val COMMAND = "command"
wenzelm@50201
   171
  val STRING = "string"
wenzelm@50201
   172
  val ALTSTRING = "altstring"
wenzelm@50201
   173
  val VERBATIM = "verbatim"
wenzelm@50201
   174
  val COMMENT = "comment"
wenzelm@50201
   175
  val CONTROL = "control"
wenzelm@50201
   176
wenzelm@50201
   177
  val KEYWORD1 = "keyword1"
wenzelm@50201
   178
  val KEYWORD2 = "keyword2"
wenzelm@50201
   179
wenzelm@50201
   180
wenzelm@50201
   181
  /* timing */
wenzelm@50201
   182
wenzelm@50201
   183
  val TIMING = "timing"
wenzelm@50201
   184
  val ELAPSED = "elapsed"
wenzelm@50201
   185
  val CPU = "cpu"
wenzelm@50201
   186
  val GC = "gc"
wenzelm@50201
   187
wenzelm@50201
   188
  object Timing
wenzelm@50201
   189
  {
wenzelm@50201
   190
    def apply(timing: isabelle.Timing): Markup =
wenzelm@50201
   191
      Markup(TIMING, List(
wenzelm@50201
   192
        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
wenzelm@50201
   193
        (CPU, Properties.Value.Double(timing.cpu.seconds)),
wenzelm@50201
   194
        (GC, Properties.Value.Double(timing.gc.seconds))))
wenzelm@50201
   195
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@50201
   196
      markup match {
wenzelm@50201
   197
        case Markup(TIMING, List(
wenzelm@50201
   198
          (ELAPSED, Properties.Value.Double(elapsed)),
wenzelm@50201
   199
          (CPU, Properties.Value.Double(cpu)),
wenzelm@50201
   200
          (GC, Properties.Value.Double(gc)))) =>
wenzelm@50201
   201
            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@50201
   202
        case _ => None
wenzelm@50201
   203
      }
wenzelm@50201
   204
  }
wenzelm@50201
   205
wenzelm@50201
   206
wenzelm@50201
   207
  /* toplevel */
wenzelm@50201
   208
wenzelm@50201
   209
  val SUBGOALS = "subgoals"
wenzelm@50201
   210
  val PROOF_STATE = "proof_state"
wenzelm@50201
   211
wenzelm@50201
   212
  val STATE = "state"
wenzelm@50201
   213
  val SUBGOAL = "subgoal"
wenzelm@50201
   214
  val SENDBACK = "sendback"
wenzelm@50201
   215
  val INTENSIFY = "intensify"
wenzelm@50201
   216
wenzelm@50201
   217
wenzelm@50201
   218
  /* command status */
wenzelm@50201
   219
wenzelm@50201
   220
  val TASK = "task"
wenzelm@50201
   221
wenzelm@50201
   222
  val ACCEPTED = "accepted"
wenzelm@50201
   223
  val FORKED = "forked"
wenzelm@50201
   224
  val JOINED = "joined"
wenzelm@50201
   225
  val RUNNING = "running"
wenzelm@50201
   226
  val FINISHED = "finished"
wenzelm@50201
   227
  val FAILED = "failed"
wenzelm@50201
   228
wenzelm@50201
   229
wenzelm@50201
   230
  /* interactive documents */
wenzelm@50201
   231
wenzelm@50201
   232
  val VERSION = "version"
wenzelm@50201
   233
  val ASSIGN = "assign"
wenzelm@50201
   234
wenzelm@50201
   235
wenzelm@50201
   236
  /* prover process */
wenzelm@50201
   237
wenzelm@50201
   238
  val PROVER_COMMAND = "prover_command"
wenzelm@50201
   239
  val PROVER_ARG = "prover_arg"
wenzelm@50201
   240
wenzelm@50201
   241
wenzelm@50201
   242
  /* messages */
wenzelm@50201
   243
wenzelm@50201
   244
  val Serial = new Properties.Long("serial")
wenzelm@50201
   245
wenzelm@50201
   246
  val MESSAGE = "message"
wenzelm@50201
   247
wenzelm@50201
   248
  val INIT = "init"
wenzelm@50201
   249
  val STATUS = "status"
wenzelm@50201
   250
  val REPORT = "report"
wenzelm@50201
   251
  val WRITELN = "writeln"
wenzelm@50201
   252
  val TRACING = "tracing"
wenzelm@50201
   253
  val WARNING = "warning"
wenzelm@50201
   254
  val ERROR = "error"
wenzelm@50201
   255
  val PROTOCOL = "protocol"
wenzelm@50201
   256
  val SYSTEM = "system"
wenzelm@50201
   257
  val STDOUT = "stdout"
wenzelm@50201
   258
  val STDERR = "stderr"
wenzelm@50201
   259
  val EXIT = "exit"
wenzelm@50201
   260
wenzelm@50201
   261
  val WRITELN_MESSAGE = "writeln_message"
wenzelm@50201
   262
  val TRACING_MESSAGE = "tracing_message"
wenzelm@50201
   263
  val WARNING_MESSAGE = "warning_message"
wenzelm@50201
   264
  val ERROR_MESSAGE = "error_message"
wenzelm@50201
   265
wenzelm@50201
   266
  val message: String => String =
wenzelm@50201
   267
    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
wenzelm@50201
   268
        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
wenzelm@50201
   269
      .withDefault((name: String) => name + "_message")
wenzelm@50201
   270
wenzelm@50201
   271
  val Return_Code = new Properties.Int("return_code")
wenzelm@50201
   272
wenzelm@50201
   273
  val LEGACY = "legacy"
wenzelm@50201
   274
wenzelm@50201
   275
  val NO_REPORT = "no_report"
wenzelm@50201
   276
wenzelm@50201
   277
  val BAD = "bad"
wenzelm@50201
   278
wenzelm@50201
   279
  val GRAPHVIEW = "graphview"
wenzelm@50201
   280
wenzelm@50201
   281
wenzelm@50201
   282
  /* protocol message functions */
wenzelm@50201
   283
wenzelm@50201
   284
  val FUNCTION = "function"
wenzelm@50201
   285
  val Function = new Properties.String(FUNCTION)
wenzelm@50201
   286
wenzelm@50201
   287
  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
wenzelm@50201
   288
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
wenzelm@50201
   289
wenzelm@50201
   290
  object Invoke_Scala
wenzelm@50201
   291
  {
wenzelm@50201
   292
    def unapply(props: Properties.T): Option[(String, String)] =
wenzelm@50201
   293
      props match {
wenzelm@50201
   294
        case List((FUNCTION, "invoke_scala"), (NAME, name), (ID, id)) => Some((name, id))
wenzelm@50201
   295
        case _ => None
wenzelm@50201
   296
      }
wenzelm@50201
   297
  }
wenzelm@50201
   298
  object Cancel_Scala
wenzelm@50201
   299
  {
wenzelm@50201
   300
    def unapply(props: Properties.T): Option[String] =
wenzelm@50201
   301
      props match {
wenzelm@50201
   302
        case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
wenzelm@50201
   303
        case _ => None
wenzelm@50201
   304
      }
wenzelm@50201
   305
  }
wenzelm@45666
   306
}
wenzelm@43721
   307
wenzelm@43721
   308
wenzelm@45666
   309
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@43748
   310