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