src/Pure/PIDE/markup.scala
author wenzelm
Sat, 17 Aug 2013 22:15:45 +0200
changeset 53055 0fe8a9972eda
parent 52877 9a26ec5739dd
child 53378 07990ba8c0ea
permissions -rw-r--r--
some protocol to determine provers according to ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45670
b84170538043 rearranged files;
wenzelm
parents: 45667
diff changeset
     1
/*  Title:      Pure/PIDE/markup.scala
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45670
diff changeset
     2
    Module:     PIDE
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     4
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
     5
Isabelle-specific implementation of quasi-abstract markup elements.
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     6
*/
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     7
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     8
package isabelle
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     9
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
    10
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    11
object Markup
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    12
{
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    13
  /* properties */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    14
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    15
  val NAME = "name"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    16
  val Name = new Properties.String(NAME)
42136
826168ae0213 added Markup.Name and Markup.Kind convenience;
wenzelm
parents: 41483
diff changeset
    17
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    18
  val KIND = "kind"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    19
  val Kind = new Properties.String(KIND)
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    20
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
    21
  val INSTANCE = "instance"
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
    22
  val Instance = new Properties.String(INSTANCE)
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
    23
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    24
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    25
  /* basic markup */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    26
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    27
  val Empty = Markup("", Nil)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    28
  val Broken = Markup("broken", Nil)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    29
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    30
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    31
  /* formal entities */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    32
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    33
  val BINDING = "binding"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    34
  val ENTITY = "entity"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    35
  val DEF = "def"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    36
  val REF = "ref"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    37
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    38
  object Entity
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    39
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    40
    def unapply(markup: Markup): Option[(String, String)] =
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    41
      markup match {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    42
        case Markup(ENTITY, props @ Kind(kind)) =>
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    43
          props match {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    44
            case Name(name) => Some(kind, name)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    45
            case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    46
          }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    47
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    48
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    49
  }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    50
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    51
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    52
  /* position */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    53
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    54
  val LINE = "line"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    55
  val OFFSET = "offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    56
  val END_OFFSET = "end_offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    57
  val FILE = "file"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    58
  val ID = "id"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    59
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    60
  val DEF_LINE = "def_line"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    61
  val DEF_OFFSET = "def_offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    62
  val DEF_END_OFFSET = "def_end_offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    63
  val DEF_FILE = "def_file"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    64
  val DEF_ID = "def_id"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    65
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    66
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    67
  val POSITION = "position"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    68
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    69
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    70
  /* path */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    71
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    72
  val PATH = "path"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    73
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    74
  object Path
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    75
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    76
    def unapply(markup: Markup): Option[String] =
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    77
      markup match {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    78
        case Markup(PATH, Name(name)) => Some(name)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    79
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    80
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    81
  }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    82
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    83
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    84
  /* pretty printing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    85
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    86
  val Indent = new Properties.Int("indent")
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    87
  val BLOCK = "block"
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 50975
diff changeset
    88
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    89
  val Width = new Properties.Int("width")
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    90
  val BREAK = "break"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    91
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 50975
diff changeset
    92
  val ITEM = "item"
51574
2b58d7b139d6 ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents: 51570
diff changeset
    93
  val BULLET = "bullet"
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 50975
diff changeset
    94
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    95
  val SEPARATOR = "separator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    96
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    97
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    98
  /* hidden text */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    99
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   100
  val HIDDEN = "hidden"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   101
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   102
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   103
  /* logical entities */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   104
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   105
  val CLASS = "class"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   106
  val TYPE_NAME = "type_name"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   107
  val FIXED = "fixed"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   108
  val CONSTANT = "constant"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   109
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   110
  val DYNAMIC_FACT = "dynamic_fact"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   111
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   112
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   113
  /* inner syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   114
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   115
  val TFREE = "tfree"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   116
  val TVAR = "tvar"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   117
  val FREE = "free"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   118
  val SKOLEM = "skolem"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   119
  val BOUND = "bound"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   120
  val VAR = "var"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   121
  val NUMERAL = "numeral"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   122
  val LITERAL = "literal"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   123
  val DELIMITER = "delimiter"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   124
  val INNER_STRING = "inner_string"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   125
  val INNER_COMMENT = "inner_comment"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   126
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   127
  val TOKEN_RANGE = "token_range"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   128
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   129
  val SORT = "sort"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   130
  val TYP = "typ"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   131
  val TERM = "term"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   132
  val PROP = "prop"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   133
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   134
  val SORTING = "sorting"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   135
  val TYPING = "typing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   136
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   137
  val ATTRIBUTE = "attribute"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   138
  val METHOD = "method"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   139
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   140
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   141
  /* embedded source text */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   142
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   143
  val ML_SOURCE = "ML_source"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   144
  val DOCUMENT_SOURCE = "document_source"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   145
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   146
  val ANTIQ = "antiq"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   147
  val ML_ANTIQUOTATION = "ML_antiquotation"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   148
  val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   149
  val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   150
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   151
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   152
  /* text structure */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   153
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   154
  val PARAGRAPH = "paragraph"
50545
00bdc48c5f71 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents: 50543
diff changeset
   155
  val TEXT_FOLD = "text_fold"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   156
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   157
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   158
  /* ML syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   159
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   160
  val ML_KEYWORD = "ML_keyword"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   161
  val ML_DELIMITER = "ML_delimiter"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   162
  val ML_TVAR = "ML_tvar"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   163
  val ML_NUMERAL = "ML_numeral"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   164
  val ML_CHAR = "ML_char"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   165
  val ML_STRING = "ML_string"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   166
  val ML_COMMENT = "ML_comment"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   167
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   168
  val ML_DEF = "ML_def"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   169
  val ML_OPEN = "ML_open"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   170
  val ML_STRUCT = "ML_struct"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   171
  val ML_TYPING = "ML_typing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   172
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   173
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   174
  /* outer syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   175
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   176
  val KEYWORD = "keyword"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   177
  val OPERATOR = "operator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   178
  val COMMAND = "command"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   179
  val STRING = "string"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   180
  val ALTSTRING = "altstring"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   181
  val VERBATIM = "verbatim"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   182
  val COMMENT = "comment"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   183
  val CONTROL = "control"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   184
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   185
  val KEYWORD1 = "keyword1"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   186
  val KEYWORD2 = "keyword2"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   187
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   188
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   189
  /* timing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   190
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   191
  val Elapsed = new Properties.Double("elapsed")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   192
  val CPU = new Properties.Double("cpu")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   193
  val GC = new Properties.Double("gc")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   194
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   195
  object Timing_Properties
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   196
  {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   197
    def apply(timing: isabelle.Timing): Properties.T =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   198
      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   199
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   200
    def unapply(props: Properties.T): Option[isabelle.Timing] =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   201
      (props, props, props) match {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   202
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   203
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   204
        case _ => None
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   205
      }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   206
  }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   207
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   208
  val TIMING = "timing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   209
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   210
  object Timing
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   211
  {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   212
    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   213
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   214
    def unapply(markup: Markup): Option[isabelle.Timing] =
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   215
      markup match {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   216
        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   217
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   218
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   219
  }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   220
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   221
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   222
  /* command timing */
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   223
51818
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51662
diff changeset
   224
  val COMMAND_TIMING = "command_timing"
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   225
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   226
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   227
  /* toplevel */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   228
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   229
  val SUBGOALS = "subgoals"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   230
  val PROOF_STATE = "proof_state"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   231
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   232
  val STATE = "state"
50543
42bbe637be54 fold main goal;
wenzelm
parents: 50503
diff changeset
   233
  val GOAL = "goal"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   234
  val SUBGOAL = "subgoal"
50215
97959912840a more general sendback properties;
wenzelm
parents: 50201
diff changeset
   235
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
diff changeset
   236
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   237
  /* command status */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   238
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   239
  val TASK = "task"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   240
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   241
  val ACCEPTED = "accepted"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   242
  val FORKED = "forked"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   243
  val JOINED = "joined"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   244
  val RUNNING = "running"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   245
  val FINISHED = "finished"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   246
  val FAILED = "failed"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   247
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   248
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   249
  /* interactive documents */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   250
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   251
  val VERSION = "version"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   252
  val ASSIGN = "assign"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   253
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   254
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   255
  /* prover process */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   256
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   257
  val PROVER_COMMAND = "prover_command"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   258
  val PROVER_ARG = "prover_arg"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   259
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   260
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   261
  /* messages */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   262
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   263
  val Serial = new Properties.Long("serial")
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   264
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   265
  val MESSAGE = "message"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   266
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   267
  val INIT = "init"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   268
  val STATUS = "status"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   269
  val REPORT = "report"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   270
  val RESULT = "result"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   271
  val WRITELN = "writeln"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   272
  val TRACING = "tracing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   273
  val WARNING = "warning"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   274
  val ERROR = "error"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   275
  val PROTOCOL = "protocol"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   276
  val SYSTEM = "system"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   277
  val STDOUT = "stdout"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   278
  val STDERR = "stderr"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   279
  val EXIT = "exit"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   280
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   281
  val WRITELN_MESSAGE = "writeln_message"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   282
  val TRACING_MESSAGE = "tracing_message"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   283
  val WARNING_MESSAGE = "warning_message"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   284
  val ERROR_MESSAGE = "error_message"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   285
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   286
  val messages =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   287
    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   288
        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   289
  val message: String => String = messages.withDefault((s: String) => s)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   290
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   291
  val Return_Code = new Properties.Int("return_code")
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   292
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   293
  val LEGACY = "legacy"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   294
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   295
  val NO_REPORT = "no_report"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   296
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   297
  val BAD = "bad"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   298
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   299
  val INTENSIFY = "intensify"
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52563
diff changeset
   300
  val INFORMATION = "information"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   301
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   302
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   303
  /* active areas */
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   304
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50545
diff changeset
   305
  val BROWSER = "browser"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   306
  val GRAPHVIEW = "graphview"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   307
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   308
  val SENDBACK = "sendback"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   309
  val PADDING = "padding"
52697
6fb98a20c349 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents: 52643
diff changeset
   310
  val PADDING_LINE = (PADDING, "line")
6fb98a20c349 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents: 52643
diff changeset
   311
  val PADDING_COMMAND = (PADDING, "command")
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   312
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   313
  val DIALOG = "dialog"
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50501
diff changeset
   314
  val Result = new Properties.String(RESULT)
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   315
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   316
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   317
  /* protocol message functions */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   318
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   319
  val FUNCTION = "function"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   320
  val Function = new Properties.String(FUNCTION)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   321
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52697
diff changeset
   322
  val Flush: Properties.T = List((FUNCTION, "flush"))
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52697
diff changeset
   323
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52111
diff changeset
   324
  val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   325
  val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   326
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   327
  object Protocol_Handler
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   328
  {
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   329
    def unapply(props: Properties.T): Option[(String)] =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   330
      props match {
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   331
        case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   332
        case _ => None
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   333
      }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   334
  }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   335
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   336
  val INVOKE_SCALA = "invoke_scala"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   337
  object Invoke_Scala
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   338
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   339
    def unapply(props: Properties.T): Option[(String, String)] =
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   340
      props match {
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   341
        case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   342
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   343
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   344
  }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   345
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   346
  val CANCEL_SCALA = "cancel_scala"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   347
  object Cancel_Scala
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   348
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   349
    def unapply(props: Properties.T): Option[String] =
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   350
      props match {
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   351
        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   352
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   353
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   354
  }
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   355
53055
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   356
  val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   357
  val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   358
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   359
  object ML_Statistics
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   360
  {
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   361
    def unapply(props: Properties.T): Option[Properties.T] =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   362
      props match {
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   363
        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   364
        case _ => None
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   365
      }
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   366
  }
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   367
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   368
  object Task_Statistics
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   369
  {
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   370
    def unapply(props: Properties.T): Option[Properties.T] =
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   371
      props match {
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   372
        case (FUNCTION, "task_statistics") :: stats => Some(stats)
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   373
        case _ => None
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   374
      }
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   375
  }
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   376
}
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   377
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   378
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   379
sealed case class Markup(name: String, properties: Properties.T)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   380