src/Pure/PIDE/isabelle_markup.scala
author wenzelm
Wed, 04 Apr 2012 14:19:47 +0200
changeset 47336 bed4b2738d8a
parent 46910 3e068ef04b42
child 47395 e6261a493f04
permissions -rw-r--r--
separate module for prover command execution;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45670
b84170538043 rearranged files;
wenzelm
parents: 45666
diff changeset
     1
/*  Title:      Pure/PIDE/isabelle_markup.scala
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     3
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
     4
Isabelle markup elements.
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     5
*/
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     6
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     7
package isabelle
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     8
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
     9
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    10
object Isabelle_Markup
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    11
{
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    12
  /* formal entities */
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    13
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    14
  val BINDING = "binding"
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    15
  val ENTITY = "entity"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    16
  val DEF = "def"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    17
  val REF = "ref"
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    18
42202
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    19
  object Entity
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    20
  {
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    21
    def unapply(markup: Markup): Option[(String, String)] =
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    22
      markup match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    23
        case Markup(ENTITY, props @ Markup.Kind(kind)) =>
42202
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    24
          props match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    25
            case Markup.Name(name) => Some(kind, name)
42202
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    26
            case _ => None
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    27
          }
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    28
        case _ => None
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    29
      }
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    30
  }
f6483ed40529 show tooltip/sub-expression for entity markup;
wenzelm
parents: 42136
diff changeset
    31
33088
757d7787b10c markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents: 32450
diff changeset
    32
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    33
  /* position */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    34
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    35
  val LINE = "line"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    36
  val OFFSET = "offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    37
  val END_OFFSET = "end_offset"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    38
  val FILE = "file"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    39
  val ID = "id"
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    40
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
    41
  val DEF_LINE = "def_line"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
    42
  val DEF_OFFSET = "def_offset"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
    43
  val DEF_END_OFFSET = "def_end_offset"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
    44
  val DEF_FILE = "def_file"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
    45
  val DEF_ID = "def_id"
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42202
diff changeset
    46
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 43673
diff changeset
    47
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    48
  val POSITION = "position"
29205
7dc7a75033ea added POSITION_PROPERTIES;
wenzelm
parents: 29195
diff changeset
    49
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    50
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    51
  /* path */
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    52
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    53
  val PATH = "path"
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    54
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    55
  object Path
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    56
  {
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    57
    def unapply(markup: Markup): Option[String] =
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    58
      markup match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    59
        case Markup(PATH, Markup.Name(name)) => Some(name)
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    60
        case _ => None
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    61
      }
11140987d415 print Path.T with some markup;
wenzelm
parents: 43564
diff changeset
    62
  }
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    63
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    64
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    65
  /* pretty printing */
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    66
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    67
  val Indent = new Properties.Int("indent")
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    68
  val BLOCK = "block"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    69
  val Width = new Properties.Int("width")
36683
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    70
  val BREAK = "break"
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    71
41a1210519fd basic support for symbolic pretty printing;
wenzelm
parents: 34242
diff changeset
    72
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    73
  /* hidden text */
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    74
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    75
  val HIDDEN = "hidden"
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    76
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33088
diff changeset
    77
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    78
  /* logical entities */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    79
43551
07a9cbf2376f clarified Markup.CLASS vs. HTML.CLASS;
wenzelm
parents: 43432
diff changeset
    80
  val CLASS = "class"
46649
bb185c45037e clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
wenzelm
parents: 46123
diff changeset
    81
  val TYPE_NAME = "type name"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    82
  val FIXED = "fixed"
43552
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43551
diff changeset
    83
  val CONSTANT = "constant"
156c822f181a entity markup for "type", "constant";
wenzelm
parents: 43551
diff changeset
    84
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    85
  val DYNAMIC_FACT = "dynamic_fact"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    86
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    87
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    88
  /* inner syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    89
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    90
  val TFREE = "tfree"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    91
  val TVAR = "tvar"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    92
  val FREE = "free"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    93
  val SKOLEM = "skolem"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    94
  val BOUND = "bound"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    95
  val VAR = "var"
45702
7df60d1aa988 updated markup conforming to ML side;
wenzelm
parents: 45674
diff changeset
    96
  val NUMERAL = "numeral"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    97
  val LITERAL = "literal"
43432
224006e5ac46 inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents: 43386
diff changeset
    98
  val DELIMITER = "delimiter"
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 42492
diff changeset
    99
  val INNER_STRING = "inner_string"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   100
  val INNER_COMMENT = "inner_comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   101
39168
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   102
  val TOKEN_RANGE = "token_range"
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38887
diff changeset
   103
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   104
  val SORT = "sort"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   105
  val TYP = "typ"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   106
  val TERM = "term"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   107
  val PROP = "prop"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   108
45445
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44706
diff changeset
   109
  val TYPING = "typing"
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44706
diff changeset
   110
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   111
  val ATTRIBUTE = "attribute"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   112
  val METHOD = "method"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   113
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   114
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   115
  /* embedded source text */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   116
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   117
  val ML_SOURCE = "ML_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   118
  val DOC_SOURCE = "doc_source"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   119
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   120
  val ANTIQ = "antiq"
43560
d1650e3720fd ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43552
diff changeset
   121
  val ML_ANTIQUOTATION = "ML antiquotation"
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
   122
  val DOCUMENT_ANTIQUOTATION = "document antiquotation"
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 43560
diff changeset
   123
  val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   124
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   125
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   126
  /* ML syntax */
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   127
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   128
  val ML_KEYWORD = "ML_keyword"
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 37194
diff changeset
   129
  val ML_DELIMITER = "ML_delimiter"
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   130
  val ML_TVAR = "ML_tvar"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   131
  val ML_NUMERAL = "ML_numeral"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   132
  val ML_CHAR = "ML_char"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   133
  val ML_STRING = "ML_string"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   134
  val ML_COMMENT = "ML_comment"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   135
  val ML_MALFORMED = "ML_malformed"
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   136
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   137
  val ML_DEF = "ML_def"
31472
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   138
  val ML_OPEN = "ML_open"
d7929d74acb4 added markup ML_open, ML_struct;
wenzelm
parents: 31384
diff changeset
   139
  val ML_STRUCT = "ML_struct"
30702
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   140
  val ML_TYPING = "ML_typing"
274626e2b2dd more markup elements for ML programs;
wenzelm
parents: 30615
diff changeset
   141
30615
f1275196df16 added ML syntax markup;
wenzelm
parents: 29522
diff changeset
   142
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   143
  /* outer syntax */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   144
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   145
  val KEYWORD = "keyword"
37194
825456e5db30 less pschedelic token markup;
wenzelm
parents: 37186
diff changeset
   146
  val OPERATOR = "operator"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   147
  val COMMAND = "command"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   148
  val STRING = "string"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   149
  val ALTSTRING = "altstring"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   150
  val VERBATIM = "verbatim"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   151
  val COMMENT = "comment"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   152
  val CONTROL = "control"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   153
  val MALFORMED = "malformed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   154
29185
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   155
  val COMMAND_SPAN = "command_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   156
  val IGNORED_SPAN = "ignored_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   157
  val MALFORMED_SPAN = "malformed_span"
26fcfca1db9d more markup elements;
wenzelm
parents: 29184
diff changeset
   158
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   159
45674
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   160
  /* timing */
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   161
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   162
  val TIMING = "timing"
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   163
  val ELAPSED = "elapsed"
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   164
  val CPU = "cpu"
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   165
  val GC = "gc"
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   166
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   167
  object Timing
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   168
  {
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   169
    def apply(timing: isabelle.Timing): Markup =
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   170
      Markup(TIMING, List(
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   171
        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   172
        (CPU, Properties.Value.Double(timing.cpu.seconds)),
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   173
        (GC, Properties.Value.Double(timing.gc.seconds))))
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   174
    def unapply(markup: Markup): Option[isabelle.Timing] =
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   175
      markup match {
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   176
        case Markup(TIMING, List(
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   177
          (ELAPSED, Properties.Value.Double(elapsed)),
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   178
          (CPU, Properties.Value.Double(cpu)),
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   179
          (GC, Properties.Value.Double(gc)))) =>
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   180
            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   181
        case _ => None
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   182
      }
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   183
  }
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   184
eb65c9d17e2f clarified Time vs. Timing;
wenzelm
parents: 45670
diff changeset
   185
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   186
  /* toplevel */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   187
38721
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   188
  val SUBGOALS = "subgoals"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   189
  val PROOF_STATE = "proof_state"
ca8b14fa0d0d added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents: 38474
diff changeset
   190
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   191
  val STATE = "state"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   192
  val SUBGOAL = "subgoal"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   193
  val SENDBACK = "sendback"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   194
  val HILITE = "hilite"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   195
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   196
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   197
  /* command status */
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   198
29417
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   199
  val TASK = "task"
779ff1187327 added running task markup;
wenzelm
parents: 29205
diff changeset
   200
46910
3e068ef04b42 clarified command state -- markup within proper_range, excluding trailing whitespace;
wenzelm
parents: 46774
diff changeset
   201
  val PARSED = "parsed"
37186
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   202
  val FORKED = "forked"
349e9223c685 explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents: 37121
diff changeset
   203
  val JOINED = "joined"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   204
  val FAILED = "failed"
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   205
  val FINISHED = "finished"
29488
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   206
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   207
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   208
  /* interactive documents */
8fc3aeece219 replaced command_state by edits/edit;
wenzelm
parents: 29482
diff changeset
   209
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   210
  val VERSION = "version"
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38355
diff changeset
   211
  val ASSIGN = "assign"
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
   212
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   213
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   214
  /* prover process */
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   215
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   216
  val PROVER_COMMAND = "prover_command"
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   217
  val PROVER_ARG = "prover_arg"
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   218
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   219
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   220
  /* messages */
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   221
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
   222
  val Serial = new Properties.Long("serial")
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   223
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   224
  val MESSAGE = "message"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   225
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   226
  val INIT = "init"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   227
  val STATUS = "status"
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39513
diff changeset
   228
  val REPORT = "report"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   229
  val WRITELN = "writeln"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   230
  val TRACING = "tracing"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   231
  val WARNING = "warning"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   232
  val ERROR = "error"
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46649
diff changeset
   233
  val PROTOCOL = "protocol"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   234
  val SYSTEM = "system"
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   235
  val STDOUT = "stdout"
45633
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45445
diff changeset
   236
  val STDERR = "stderr"
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29488
diff changeset
   237
  val EXIT = "exit"
29195
ea51797fa416 more markup elements;
wenzelm
parents: 29185
diff changeset
   238
44549
5e5e6ad3922c explicit markup for legacy warnings;
wenzelm
parents: 44476
diff changeset
   239
  val LEGACY = "legacy"
5e5e6ad3922c explicit markup for legacy warnings;
wenzelm
parents: 44476
diff changeset
   240
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39171
diff changeset
   241
  val NO_REPORT = "no_report"
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 39171
diff changeset
   242
39171
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   243
  val BAD = "bad"
525a13b9ac74 highlight bad range of nested error (here from inner parsing);
wenzelm
parents: 39168
diff changeset
   244
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
   245
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46649
diff changeset
   246
  /* protocol message functions */
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   247
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   248
  val FUNCTION = "function"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
   249
  val Function = new Properties.String(FUNCTION)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   250
46121
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 45702
diff changeset
   251
  val Ready: Properties.T = List((FUNCTION, "ready"))
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 45702
diff changeset
   252
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   253
  object Loaded_Theory
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   254
  {
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   255
    def unapply(props: Properties.T): Option[String] =
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   256
      props match {
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   257
        case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   258
        case _ => None
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   259
      }
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   260
  }
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   261
46123
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   262
  object Keyword_Decl
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   263
  {
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   264
    def unapply(props: Properties.T): Option[String] =
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   265
      props match {
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   266
        case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   267
        case _ => None
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   268
      }
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   269
  }
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   270
  object Command_Decl
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   271
  {
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   272
    def unapply(props: Properties.T): Option[(String, String)] =
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   273
      props match {
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   274
        case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   275
          Some((name, kind))
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   276
        case _ => None
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   277
      }
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   278
  }
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 46122
diff changeset
   279
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44549
diff changeset
   280
  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   281
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44549
diff changeset
   282
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   283
  object Invoke_Scala
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   284
  {
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
   285
    def unapply(props: Properties.T): Option[(String, String)] =
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   286
      props match {
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   287
        case List((FUNCTION, "invoke_scala"), (Markup.NAME, name), (ID, id)) => Some((name, id))
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   288
        case _ => None
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   289
      }
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   290
  }
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   291
  object Cancel_Scala
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   292
  {
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   293
    def unapply(props: Properties.T): Option[String] =
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   294
      props match {
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   295
        case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   296
        case _ => None
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   297
      }
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 43780
diff changeset
   298
  }
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
   299
}
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37195
diff changeset
   300