src/Pure/PIDE/markup.scala
author wenzelm
Tue, 18 Feb 2014 17:03:12 +0100
changeset 55551 4a5f65df29fa
parent 55550 bcc643ac071a
child 55553 99409ccbe04a
permissions -rw-r--r--
tuned signature;
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 {
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
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
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    70
  /* position */
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 LINE = "line"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    73
  val OFFSET = "offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    74
  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
    75
  val FILE = "file"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    76
  val ID = "id"
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 DEF_LINE = "def_line"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    79
  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
    80
  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
    81
  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
    82
  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
    83
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    84
  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
    85
  val POSITION = "position"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    86
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    87
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    88
  /* embedded languages */
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    89
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    90
  val LANGUAGE = "language"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    91
  val Language = new Markup_String(LANGUAGE, NAME)
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    92
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
    93
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
    94
  /* external resources */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    95
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    96
  val PATH = "path"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    97
  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
    98
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
    99
  val URL = "url"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   100
  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
   101
50201
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
  /* pretty printing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   104
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   105
  val Block = new Markup_Int("block", "indent")
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   106
  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
   107
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
   108
  val ITEM = "item"
51574
2b58d7b139d6 ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents: 51570
diff changeset
   109
  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
   110
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   111
  val SEPARATOR = "separator"
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
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   114
  /* hidden text */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   115
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   116
  val HIDDEN = "hidden"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   117
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   118
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   119
  /* logical entities */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   120
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   121
  val CLASS = "class"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   122
  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
   123
  val FIXED = "fixed"
53378
07990ba8c0ea cases: more position information and PIDE markup;
wenzelm
parents: 53055
diff changeset
   124
  val CASE = "case"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   125
  val CONSTANT = "constant"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   126
  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
   127
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
  /* inner syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   130
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   131
  val TFREE = "tfree"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   132
  val TVAR = "tvar"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   133
  val FREE = "free"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   134
  val SKOLEM = "skolem"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   135
  val BOUND = "bound"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   136
  val VAR = "var"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   137
  val NUMERAL = "numeral"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   138
  val LITERAL = "literal"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   139
  val DELIMITER = "delimiter"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   140
  val INNER_STRING = "inner_string"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   141
  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
   142
  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
   143
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   144
  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
   145
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   146
  val SORTING = "sorting"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   147
  val TYPING = "typing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   148
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   149
  val ATTRIBUTE = "attribute"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   150
  val METHOD = "method"
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
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   153
  /* antiquotations */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   154
55526
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   155
  val ANTIQUOTED = "antiquoted"
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   156
  val ANTIQUOTE = "antiquote"
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   157
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   158
  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
   159
  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
   160
  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
   161
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   162
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   163
  /* text structure */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   164
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   165
  val PARAGRAPH = "paragraph"
50545
00bdc48c5f71 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents: 50543
diff changeset
   166
  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
   167
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   168
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   169
  /* ML syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   170
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   171
  val ML_KEYWORD1 = "ML_keyword1"
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   172
  val ML_KEYWORD2 = "ML_keyword2"
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   173
  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
   174
  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
   175
  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
   176
  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
   177
  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
   178
  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
   179
  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
   180
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   181
  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
   182
  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
   183
  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
   184
  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
   185
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   186
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   187
  /* outer syntax */
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
  val KEYWORD = "keyword"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   190
  val OPERATOR = "operator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   191
  val COMMAND = "command"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   192
  val STRING = "string"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   193
  val ALTSTRING = "altstring"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   194
  val VERBATIM = "verbatim"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   195
  val CARTOUCHE = "cartouche"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   196
  val COMMENT = "comment"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   197
  val CONTROL = "control"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   198
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   199
  val KEYWORD1 = "keyword1"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   200
  val KEYWORD2 = "keyword2"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   202
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   203
  /* timing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   204
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   205
  val Elapsed = new Properties.Double("elapsed")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   206
  val CPU = new Properties.Double("cpu")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   207
  val GC = new Properties.Double("gc")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   208
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   209
  object Timing_Properties
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   210
  {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   211
    def apply(timing: isabelle.Timing): Properties.T =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   212
      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
   213
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   214
    def unapply(props: Properties.T): Option[isabelle.Timing] =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   215
      (props, props, props) match {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   216
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   217
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   218
        case _ => None
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   219
      }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   220
  }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   221
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   222
  val TIMING = "timing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   223
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   224
  object Timing
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   225
  {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   226
    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
   227
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   228
    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
   229
      markup match {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   230
        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
   231
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   232
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   233
  }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   234
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   235
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   236
  /* command timing */
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   237
51818
517f232e867d clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents: 51662
diff changeset
   238
  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
   239
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51574
diff changeset
   240
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   241
  /* toplevel */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   242
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   243
  val SUBGOALS = "subgoals"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   244
  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
   245
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   246
  val STATE = "state"
50543
42bbe637be54 fold main goal;
wenzelm
parents: 50503
diff changeset
   247
  val GOAL = "goal"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   248
  val SUBGOAL = "subgoal"
50215
97959912840a more general sendback properties;
wenzelm
parents: 50201
diff changeset
   249
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
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
  /* command status */
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
  val TASK = "task"
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
  val ACCEPTED = "accepted"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   256
  val FORKED = "forked"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   257
  val JOINED = "joined"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   258
  val RUNNING = "running"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   259
  val FINISHED = "finished"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   260
  val FAILED = "failed"
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
  /* interactive documents */
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 VERSION = "version"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   266
  val ASSIGN = "assign"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   267
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   268
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   269
  /* prover process */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   270
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   271
  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
   272
  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
   273
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
  /* messages */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   276
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
   277
  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
   278
  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
   279
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   280
  val MESSAGE = "message"
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 INIT = "init"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   283
  val STATUS = "status"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   284
  val REPORT = "report"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   285
  val RESULT = "result"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   286
  val WRITELN = "writeln"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   287
  val TRACING = "tracing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   288
  val WARNING = "warning"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   289
  val ERROR = "error"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   290
  val PROTOCOL = "protocol"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   291
  val SYSTEM = "system"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   292
  val STDOUT = "stdout"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   293
  val STDERR = "stderr"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   294
  val EXIT = "exit"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   295
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   296
  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
   297
  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
   298
  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
   299
  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
   300
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   301
  val messages =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   302
    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   303
        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   304
  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
   305
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   306
  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
   307
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   308
  val LEGACY = "legacy"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   309
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   310
  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
   311
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   312
  val BAD = "bad"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   313
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   314
  val INTENSIFY = "intensify"
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52563
diff changeset
   315
  val INFORMATION = "information"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   316
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   317
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   318
  /* active areas */
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   319
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50545
diff changeset
   320
  val BROWSER = "browser"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   321
  val GRAPHVIEW = "graphview"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   322
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   323
  val SENDBACK = "sendback"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   324
  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
   325
  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
   326
  val PADDING_COMMAND = (PADDING, "command")
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   327
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   328
  val DIALOG = "dialog"
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50501
diff changeset
   329
  val Result = new Properties.String(RESULT)
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   330
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   331
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   332
  /* protocol message functions */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   333
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   334
  val FUNCTION = "function"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   335
  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
   336
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52697
diff changeset
   337
  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
   338
52563
f9a20c2c3b70 tuned protocol terminology;
wenzelm
parents: 52111
diff changeset
   339
  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
   340
  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
   341
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   342
  object Protocol_Handler
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   343
  {
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   344
    def unapply(props: Properties.T): Option[(String)] =
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   345
      props match {
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   346
        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
   347
        case _ => None
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   348
      }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   349
  }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   350
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   351
  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
   352
  object Invoke_Scala
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
    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
   355
      props match {
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   356
        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
   357
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   358
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   359
  }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   360
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   361
  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
   362
  object Cancel_Scala
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   363
  {
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   364
    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
   365
      props match {
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   366
        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
   367
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   368
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   369
  }
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   370
53055
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   371
  val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   372
  val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 52877
diff changeset
   373
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   374
  object ML_Statistics
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   375
  {
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   376
    def unapply(props: Properties.T): Option[Properties.T] =
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   377
      props match {
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   378
        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   379
        case _ => None
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   380
      }
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   381
  }
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   382
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   383
  object Task_Statistics
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   384
  {
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   385
    def unapply(props: Properties.T): Option[Properties.T] =
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   386
      props match {
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   387
        case (FUNCTION, "task_statistics") :: stats => Some(stats)
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   388
        case _ => None
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   389
      }
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   390
  }
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
   391
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
   392
  /* 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
   393
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
   394
  val TEXT = "text"
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
   395
  val Text = new Properties.String(TEXT)
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
   396
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
   397
  val PARENT = "parent"
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
   398
  val Parent = new Properties.Long(PARENT)
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
   399
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
   400
  val SUCCESS = "success"
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
   401
  val Success = new Properties.Boolean(SUCCESS)
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
   402
55390
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   403
  val MEMORY = "memory"
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   404
  val Memory = new Properties.Boolean(MEMORY)
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   405
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
   406
  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
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
   407
  object Cancel_Simp_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
   408
  {
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
   409
    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
   410
      props match {
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
   411
        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
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
   412
        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
   413
      }
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
   414
  }
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
   415
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
   416
  val SIMP_TRACE = "simp_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
   417
  object Simp_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
   418
  {
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
   419
    def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
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
      tree match {
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
   421
        case XML.Elem(Markup(SIMP_TRACE, props), _) =>
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
          (props, props) match {
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
            case (Serial(serial), Name(name)) =>
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
   424
              Simplifier_Trace.all_answers.find(_.name == name).map((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
   425
            case _ =>
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
   426
              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
   427
          }
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
   428
        case _ =>
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
   429
          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
   430
      }
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
  }
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
   432
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
   433
  /* trace items from the prover */
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
  object Simp_Trace_Item
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
  {
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
   437
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
    def unapply(tree: XML.Tree): Option[(String, Data)] =
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
      tree match {
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
        case XML.Elem(Markup(RESULT, Serial(serial)), List(
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
   441
          XML.Elem(Markup(markup, props), content)
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
   442
        )) if markup.startsWith("simp_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
   443
          (props, props) match {
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
   444
            case (Text(text), Parent(parent)) =>
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
   445
              Some((markup, Data(serial, markup, text, parent, props, content)))
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
   446
            case _ =>
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
   447
              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
   448
          }
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
   449
        case _ =>
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
   450
          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
   451
      }
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
   452
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
   453
    val LOG = "simp_trace_log"
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
   454
    val STEP = "simp_trace_step"
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
   455
    val RECURSE = "simp_trace_recurse"
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
   456
    val HINT = "simp_trace_hint"
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
   457
    val IGNORE = "simp_trace_ignore"
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
   458
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
   459
    case class Data(serial: Long, markup: String, text: String,
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
   460
                    parent: Long, props: Properties.T, content: XML.Body)
55390
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   461
    {
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   462
      def memory: Boolean =
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   463
        Memory.unapply(props) getOrElse true
36550a4eac5e "no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents: 55316
diff changeset
   464
    }
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
   465
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
   466
  }
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
   467
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   468
}
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   469
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   470
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   471
sealed case class Markup(name: String, properties: Properties.T)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   472