src/Pure/PIDE/markup.scala
author wenzelm
Tue, 25 Mar 2014 16:11:00 +0100
changeset 56278 2576d3a40ed6
parent 56202 0a11d17eeeff
child 56548 ae6870efc28d
permissions -rw-r--r--
separate tokenization and language context for SML: no symbols, no antiquotes;
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
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    30
  class Markup_String(val name: String, prop: String)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    31
  {
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    32
    private val Prop = new Properties.String(prop)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    33
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    34
    def apply(s: String): Markup = Markup(name, Prop(s))
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    35
    def unapply(markup: Markup): Option[String] =
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    36
      if (markup.name == name) Prop.unapply(markup.properties) else None
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    37
  }
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    38
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    39
  class Markup_Int(val name: String, prop: String)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    40
  {
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    41
    private val Prop = new Properties.Int(prop)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    42
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    43
    def apply(i: Int): Markup = Markup(name, Prop(i))
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    44
    def unapply(markup: Markup): Option[Int] =
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    45
      if (markup.name == name) Prop.unapply(markup.properties) else None
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    46
  }
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    47
50201
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
  /* formal entities */
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
  val BINDING = "binding"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    52
  val ENTITY = "entity"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    53
  val DEF = "def"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    54
  val REF = "ref"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    55
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    56
  object Entity
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    57
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    58
    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
    59
      markup match {
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    60
        case Markup(ENTITY, props) =>
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    61
          (props, props) match {
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
    62
            case (Kind(kind), Name(name)) => Some((kind, name))
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    63
            case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    64
          }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    65
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    66
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    67
  }
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
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
    70
  /* completion */
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
    71
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
    72
  val COMPLETION = "completion"
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55837
diff changeset
    73
  val NO_COMPLETION = "no_completion"
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
    74
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
    75
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    76
  /* position */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    77
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    78
  val LINE = "line"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    79
  val OFFSET = "offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    80
  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
    81
  val FILE = "file"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    82
  val ID = "id"
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
  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
    85
  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
    86
  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
    87
  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
    88
  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
    89
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    90
  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
    91
  val POSITION = "position"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    92
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    93
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    94
  /* embedded languages */
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    95
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55616
diff changeset
    96
  val Symbols = new Properties.Boolean("symbols")
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55616
diff changeset
    97
  val Antiquotes = new Properties.Boolean("antiquotes")
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
    98
  val Delimited = new Properties.Boolean("delimited")
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
    99
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   100
  val LANGUAGE = "language"
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   101
  object Language
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   102
  {
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55615
diff changeset
   103
    val ML = "ML"
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56202
diff changeset
   104
    val SML = "SML"
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55615
diff changeset
   105
    val UNKNOWN = "unknown"
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55615
diff changeset
   106
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   107
    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   108
      markup match {
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   109
        case Markup(LANGUAGE, props) =>
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   110
          (props, props, props, props) match {
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   111
            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   112
              Some((name, symbols, antiquotes, delimited))
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   113
            case _ => None
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   114
          }
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   115
        case _ => None
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   116
      }
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   117
  }
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   118
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   119
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
   120
  /* external resources */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   121
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   122
  val PATH = "path"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   123
  val Path = new Markup_String(PATH, NAME)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   124
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
   125
  val URL = "url"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   126
  val Url = new Markup_String(URL, NAME)
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
   127
50201
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
  /* pretty printing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   130
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   131
  val Block = new Markup_Int("block", "indent")
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   132
  val Break = new Markup_Int("break", "width")
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   133
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
   134
  val ITEM = "item"
51574
2b58d7b139d6 ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents: 51570
diff changeset
   135
  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
   136
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   137
  val SEPARATOR = "separator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   138
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
  /* hidden text */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   141
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   142
  val HIDDEN = "hidden"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   143
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   144
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   145
  /* logical entities */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   146
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   147
  val CLASS = "class"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   148
  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
   149
  val FIXED = "fixed"
53378
07990ba8c0ea cases: more position information and PIDE markup;
wenzelm
parents: 53055
diff changeset
   150
  val CASE = "case"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   151
  val CONSTANT = "constant"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   152
  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
   153
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   154
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   155
  /* inner syntax */
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
  val TFREE = "tfree"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   158
  val TVAR = "tvar"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   159
  val FREE = "free"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   160
  val SKOLEM = "skolem"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   161
  val BOUND = "bound"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   162
  val VAR = "var"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   163
  val NUMERAL = "numeral"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   164
  val LITERAL = "literal"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   165
  val DELIMITER = "delimiter"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   166
  val INNER_STRING = "inner_string"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   167
  val INNER_CARTOUCHE = "inner_cartouche"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   168
  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
   169
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   170
  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
   171
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   172
  val SORTING = "sorting"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   173
  val TYPING = "typing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   174
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   175
  val ATTRIBUTE = "attribute"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   176
  val METHOD = "method"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   177
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   178
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   179
  /* antiquotations */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   180
55526
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   181
  val ANTIQUOTED = "antiquoted"
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   182
  val ANTIQUOTE = "antiquote"
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   183
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   184
  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
   185
  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
   186
  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
   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
  /* text structure */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   190
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   191
  val PARAGRAPH = "paragraph"
50545
00bdc48c5f71 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents: 50543
diff changeset
   192
  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
   193
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   194
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   195
  /* ML syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   196
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   197
  val ML_KEYWORD1 = "ML_keyword1"
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   198
  val ML_KEYWORD2 = "ML_keyword2"
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   199
  val ML_KEYWORD3 = "ML_keyword3"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   200
  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
   201
  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
   202
  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
   203
  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
   204
  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
   205
  val ML_COMMENT = "ML_comment"
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56202
diff changeset
   206
  val SML_STRING = "SML_string"
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56202
diff changeset
   207
  val SML_COMMENT = "SML_comment"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   208
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   209
  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
   210
  val ML_OPEN = "ML_open"
55837
154855d9a564 clarified names of antiquotations and markup;
wenzelm
parents: 55828
diff changeset
   211
  val ML_STRUCTURE = "ML_structure"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   212
  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
   213
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   214
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   215
  /* outer syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   216
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55694
diff changeset
   217
  val COMMAND = "command"
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55694
diff changeset
   218
  val KEYWORD1 = "keyword1"
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55694
diff changeset
   219
  val KEYWORD2 = "keyword2"
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55744
diff changeset
   220
  val KEYWORD3 = "keyword3"
55919
2eb8c13339a5 more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents: 55914
diff changeset
   221
  val QUASI_KEYWORD = "quasi_keyword"
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 55919
diff changeset
   222
  val IMPROPER = "improper"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   223
  val OPERATOR = "operator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   224
  val STRING = "string"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   225
  val ALTSTRING = "altstring"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   226
  val VERBATIM = "verbatim"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   227
  val CARTOUCHE = "cartouche"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   228
  val COMMENT = "comment"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   229
  val CONTROL = "control"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   230
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
  /* timing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   233
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   234
  val Elapsed = new Properties.Double("elapsed")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   235
  val CPU = new Properties.Double("cpu")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   236
  val GC = new Properties.Double("gc")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   237
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   238
  object Timing_Properties
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   239
  {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   240
    def apply(timing: isabelle.Timing): Properties.T =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   241
      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
   242
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   243
    def unapply(props: Properties.T): Option[isabelle.Timing] =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   244
      (props, props, props) match {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   245
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   246
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   247
        case _ => None
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   248
      }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   249
  }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   250
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   251
  val TIMING = "timing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   252
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   253
  object Timing
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   254
  {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   255
    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
   256
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   257
    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
   258
      markup match {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   259
        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
   260
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   261
      }
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
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   264
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   265
  /* command timing */
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   266
51818
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51662
diff changeset
   267
  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
   268
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   269
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   270
  /* toplevel */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   271
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   272
  val SUBGOALS = "subgoals"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   273
  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
   274
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   275
  val STATE = "state"
50543
42bbe637be54 fold main goal;
wenzelm
parents: 50503
diff changeset
   276
  val GOAL = "goal"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   277
  val SUBGOAL = "subgoal"
50215
97959912840a more general sendback properties;
wenzelm
parents: 50201
diff changeset
   278
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
diff changeset
   279
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   280
  /* command status */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   281
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   282
  val TASK = "task"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   283
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   284
  val ACCEPTED = "accepted"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   285
  val FORKED = "forked"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   286
  val JOINED = "joined"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   287
  val RUNNING = "running"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   288
  val FINISHED = "finished"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   289
  val FAILED = "failed"
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
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   292
  /* interactive documents */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   293
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   294
  val VERSION = "version"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   295
  val ASSIGN = "assign"
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
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   298
  /* prover process */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   299
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   300
  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
   301
  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
   302
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   303
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   304
  /* messages */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   305
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   306
  val SERIAL = "serial"
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   307
  val Serial = new Properties.Long(SERIAL)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   308
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   309
  val MESSAGE = "message"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   310
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   311
  val INIT = "init"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   312
  val STATUS = "status"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   313
  val REPORT = "report"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   314
  val RESULT = "result"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   315
  val WRITELN = "writeln"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   316
  val TRACING = "tracing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   317
  val WARNING = "warning"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   318
  val ERROR = "error"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   319
  val PROTOCOL = "protocol"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   320
  val SYSTEM = "system"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   321
  val STDOUT = "stdout"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   322
  val STDERR = "stderr"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   323
  val EXIT = "exit"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   324
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   325
  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
   326
  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
   327
  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
   328
  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
   329
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   330
  val messages =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   331
    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   332
        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   333
  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
   334
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   335
  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
   336
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   337
  val LEGACY = "legacy"
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
  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
   340
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   341
  val BAD = "bad"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   342
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   343
  val INTENSIFY = "intensify"
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52563
diff changeset
   344
  val INFORMATION = "information"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   345
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   346
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   347
  /* active areas */
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   348
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50545
diff changeset
   349
  val BROWSER = "browser"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   350
  val GRAPHVIEW = "graphview"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   351
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   352
  val SENDBACK = "sendback"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   353
  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
   354
  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
   355
  val PADDING_COMMAND = (PADDING, "command")
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   356
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   357
  val DIALOG = "dialog"
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50501
diff changeset
   358
  val Result = new Properties.String(RESULT)
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   359
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   360
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   361
  /* protocol message functions */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   362
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   363
  val FUNCTION = "function"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   364
  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
   365
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52697
diff changeset
   366
  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
   367
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52111
diff changeset
   368
  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
   369
  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
   370
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   371
  object Protocol_Handler
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   372
  {
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   373
    def unapply(props: Properties.T): Option[(String)] =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   374
      props match {
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   375
        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
   376
        case _ => None
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   377
      }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   378
  }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   379
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   380
  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
   381
  object Invoke_Scala
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   382
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   383
    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
   384
      props match {
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   385
        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
   386
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   387
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   388
  }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   389
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   390
  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
   391
  object Cancel_Scala
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   392
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   393
    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
   394
      props match {
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   395
        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
   396
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   397
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   398
  }
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   399
53055
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   400
  val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   401
  val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   402
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   403
  object ML_Statistics
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   404
  {
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   405
    def unapply(props: Properties.T): Option[Properties.T] =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   406
      props match {
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   407
        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   408
        case _ => None
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   409
      }
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   410
  }
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   411
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   412
  object Task_Statistics
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   413
  {
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   414
    def unapply(props: Properties.T): Option[Properties.T] =
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   415
      props match {
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   416
        case (FUNCTION, "task_statistics") :: stats => Some(stats)
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   417
        case _ => None
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   418
      }
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   419
  }
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   420
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   421
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   422
  /* simplifier trace */
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   423
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   424
  val SIMP_TRACE = "simp_trace"
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   425
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   426
  val SIMP_TRACE_LOG = "simp_trace_log"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   427
  val SIMP_TRACE_STEP = "simp_trace_step"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   428
  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   429
  val SIMP_TRACE_HINT = "simp_trace_hint"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   430
  val SIMP_TRACE_IGNORE = "simp_trace_ignore"
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   431
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   432
  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   433
  object Simp_Trace_Cancel
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   434
  {
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   435
    def unapply(props: Properties.T): Option[Long] =
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   436
      props match {
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   437
        case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   438
        case _ => None
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   439
      }
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 55033
diff changeset
   440
  }
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   441
}
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   442
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   443
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   444
sealed case class Markup(name: String, properties: Properties.T)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   445