src/Pure/PIDE/markup.scala
author wenzelm
Sun, 13 Dec 2020 22:30:30 +0100
changeset 72903 8f586c241071
parent 72902 3c09adb4b042
child 72929 776198313227
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
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     3
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
     4
Quasi-abstract markup elements.
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     5
*/
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     6
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     7
package isabelle
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     8
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
     9
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    10
object Markup
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    11
{
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    12
  /* elements */
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    13
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    14
  object Elements
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    15
  {
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    16
    def apply(elems: Set[String]): Elements = new Elements(elems)
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    17
    def apply(elems: String*): Elements = apply(Set(elems: _*))
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    18
    val empty: Elements = apply()
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    19
    val full: Elements =
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    20
      new Elements(Set.empty)
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    21
      {
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    22
        override def apply(elem: String): Boolean = true
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    23
        override def toString: String = "Elements.full"
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    24
      }
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    25
  }
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    26
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    27
  sealed class Elements private[Markup](private val rep: Set[String])
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    28
  {
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    29
    def apply(elem: String): Boolean = rep.contains(elem)
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    30
    def + (elem: String): Elements = new Elements(rep + elem)
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    31
    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
65176
908d8be90533 suppress irrelevant markup for VSCode;
wenzelm
parents: 64370
diff changeset
    32
    def - (elem: String): Elements = new Elements(rep - elem)
908d8be90533 suppress irrelevant markup for VSCode;
wenzelm
parents: 64370
diff changeset
    33
    def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    34
    override def toString: String = rep.mkString("Elements(", ",", ")")
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    35
  }
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    36
81370dfadb1d tuned signature;
wenzelm
parents: 56733
diff changeset
    37
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    38
  /* properties */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    39
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    40
  val NAME = "name"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    41
  val Name = new Properties.String(NAME)
42136
826168ae0213 added Markup.Name and Markup.Kind convenience;
wenzelm
parents: 41483
diff changeset
    42
68997
4278947ba336 more exports;
wenzelm
parents: 68884
diff changeset
    43
  val XNAME = "xname"
4278947ba336 more exports;
wenzelm
parents: 68884
diff changeset
    44
  val XName = new Properties.String(XNAME)
4278947ba336 more exports;
wenzelm
parents: 68884
diff changeset
    45
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    46
  val KIND = "kind"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    47
  val Kind = new Properties.String(KIND)
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    48
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65753
diff changeset
    49
  val CONTENT = "content"
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65753
diff changeset
    50
  val Content = new Properties.String(CONTENT)
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65753
diff changeset
    51
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    52
  val SERIAL = "serial"
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    53
  val Serial = new Properties.Long(SERIAL)
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    54
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
    55
  val INSTANCE = "instance"
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
    56
  val Instance = new Properties.String(INSTANCE)
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52800
diff changeset
    57
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    58
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    59
  /* basic markup */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    60
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71153
diff changeset
    61
  val Empty: Markup = Markup("", Nil)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71153
diff changeset
    62
  val Broken: Markup = Markup("broken", Nil)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    63
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    64
  class Markup_String(val name: String, prop: String)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    65
  {
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    66
    private val Prop = new Properties.String(prop)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    67
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    68
    def apply(s: String): Markup = Markup(name, Prop(s))
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    69
    def unapply(markup: Markup): Option[String] =
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    70
      if (markup.name == name) Prop.unapply(markup.properties) else None
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    71
  }
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    72
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    73
  class Markup_Int(val name: String, prop: String)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    74
  {
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    75
    private val Prop = new Properties.Int(prop)
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    76
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    77
    def apply(i: Int): Markup = Markup(name, Prop(i))
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    78
    def unapply(markup: Markup): Option[Int] =
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    79
      if (markup.name == name) Prop.unapply(markup.properties) else None
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    80
  }
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
    81
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    82
  class Markup_Long(val name: String, prop: String)
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    83
  {
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    84
    private val Prop = new Properties.Long(prop)
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    85
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    86
    def apply(i: Long): Markup = Markup(name, Prop(i))
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    87
    def unapply(markup: Markup): Option[Long] =
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    88
      if (markup.name == name) Prop.unapply(markup.properties) else None
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    89
  }
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
    90
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
    91
69889
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    92
  /* meta data */
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    93
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    94
  val META_TITLE = "meta_title"
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    95
  val META_CREATOR = "meta_creator"
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    96
  val META_CONTRIBUTOR = "meta_contributor"
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    97
  val META_DATE = "meta_date"
69962
82e945d472d5 documentation of document markers and re-interpreted command tags;
wenzelm
parents: 69916
diff changeset
    98
  val META_LICENSE = "meta_license"
69889
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
    99
  val META_DESCRIPTION = "meta_description"
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
diff changeset
   100
be04e9a053a7 markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents: 69788
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
  /* formal entities */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   103
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   104
  val BINDING = "binding"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   105
  val ENTITY = "entity"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   106
72902
3c09adb4b042 tuned signature;
wenzelm
parents: 72861
diff changeset
   107
  val Def = new Properties.Long("def")
3c09adb4b042 tuned signature;
wenzelm
parents: 72861
diff changeset
   108
  val Ref = new Properties.Long("ref")
3c09adb4b042 tuned signature;
wenzelm
parents: 72861
diff changeset
   109
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   110
  object Entity
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   111
  {
72903
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   112
    object Def
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   113
    {
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   114
      def unapply(markup: Markup): Option[Long] =
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   115
        if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   116
    }
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   117
    object Ref
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   118
    {
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   119
      def unapply(markup: Markup): Option[Long] =
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   120
        if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   121
    }
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   122
    object Id
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   123
    {
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   124
      def unapply(markup: Markup): Option[Long] =
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   125
        Def.unapply(markup) orElse Ref.unapply(markup)
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   126
    }
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   127
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   128
    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
   129
      markup match {
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   130
        case Markup(ENTITY, props) =>
63337
ae9330fdbc16 position information for literal facts;
wenzelm
parents: 62986
diff changeset
   131
          val kind = Kind.unapply(props).getOrElse("")
ae9330fdbc16 position information for literal facts;
wenzelm
parents: 62986
diff changeset
   132
          val name = Name.unapply(props).getOrElse("")
ae9330fdbc16 position information for literal facts;
wenzelm
parents: 62986
diff changeset
   133
          Some((kind, name))
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   134
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   135
      }
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
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   139
  /* completion */
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   140
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   141
  val COMPLETION = "completion"
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55837
diff changeset
   142
  val NO_COMPLETION = "no_completion"
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   143
69557
e72360fef69a update theory sources based on PIDE markup;
wenzelm
parents: 69320
diff changeset
   144
  val UPDATE = "update"
e72360fef69a update theory sources based on PIDE markup;
wenzelm
parents: 69320
diff changeset
   145
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55666
diff changeset
   146
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   147
  /* position */
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 LINE = "line"
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58853
diff changeset
   150
  val END_LINE = "line"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   151
  val OFFSET = "offset"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   152
  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
   153
  val FILE = "file"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   154
  val ID = "id"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   155
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   156
  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
   157
  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
   158
  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
   159
  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
   160
  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
   161
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   162
  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
72708
0cc96d337e8f tuned signature;
wenzelm
parents: 72692
diff changeset
   163
  def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
0cc96d337e8f tuned signature;
wenzelm
parents: 72692
diff changeset
   164
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   165
  val POSITION = "position"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   166
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   167
58464
5e7fc9974aba support for sub-expression markup;
wenzelm
parents: 58048
diff changeset
   168
  /* expression */
5e7fc9974aba support for sub-expression markup;
wenzelm
parents: 58048
diff changeset
   169
5e7fc9974aba support for sub-expression markup;
wenzelm
parents: 58048
diff changeset
   170
  val EXPRESSION = "expression"
62806
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   171
  object Expression
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   172
  {
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   173
    def unapply(markup: Markup): Option[String] =
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   174
      markup match {
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   175
        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   176
        case Markup(EXPRESSION, _) => Some("")
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   177
        case _ => None
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   178
      }
de9bf8171626 more markup;
wenzelm
parents: 61864
diff changeset
   179
  }
58464
5e7fc9974aba support for sub-expression markup;
wenzelm
parents: 58048
diff changeset
   180
5e7fc9974aba support for sub-expression markup;
wenzelm
parents: 58048
diff changeset
   181
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents: 58464
diff changeset
   182
  /* citation */
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents: 58464
diff changeset
   183
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents: 58464
diff changeset
   184
  val CITATION = "citation"
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58544
diff changeset
   185
  val Citation = new Markup_String(CITATION, NAME)
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents: 58464
diff changeset
   186
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents: 58464
diff changeset
   187
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   188
  /* embedded languages */
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   189
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55616
diff changeset
   190
  val Symbols = new Properties.Boolean("symbols")
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55616
diff changeset
   191
  val Antiquotes = new Properties.Boolean("antiquotes")
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   192
  val Delimited = new Properties.Boolean("delimited")
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   193
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   194
  val LANGUAGE = "language"
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   195
  object Language
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   196
  {
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   197
    val DOCUMENT = "document"
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55615
diff changeset
   198
    val ML = "ML"
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56202
diff changeset
   199
    val SML = "SML"
56843
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56743
diff changeset
   200
    val PATH = "path"
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55615
diff changeset
   201
    val UNKNOWN = "unknown"
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55615
diff changeset
   202
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   203
    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
   204
      markup match {
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   205
        case Markup(LANGUAGE, props) =>
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   206
          (props, props, props, props) match {
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   207
            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55765
diff changeset
   208
              Some((name, symbols, antiquotes, delimited))
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   209
            case _ => None
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   210
          }
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   211
        case _ => None
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   212
      }
72842
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   213
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   214
    object Path
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   215
    {
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   216
      def unapply(markup: Markup): Option[Boolean] =
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   217
        markup match {
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   218
          case Language(PATH, _, _, delimited) => Some(delimited)
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   219
          case _ => None
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   220
        }
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72782
diff changeset
   221
    }
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55553
diff changeset
   222
  }
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   223
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   224
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
   225
  /* external resources */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   226
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   227
  val PATH = "path"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   228
  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
   229
70016
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69965
diff changeset
   230
  val EXPORT_PATH = "export_path"
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69965
diff changeset
   231
  val Export_Path = new Markup_String(EXPORT_PATH, NAME)
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69965
diff changeset
   232
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 53378
diff changeset
   233
  val URL = "url"
55551
4a5f65df29fa tuned signature;
wenzelm
parents: 55550
diff changeset
   234
  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
   235
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61598
diff changeset
   236
  val DOC = "doc"
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61598
diff changeset
   237
  val Doc = new Markup_String(DOC, NAME)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61598
diff changeset
   238
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   239
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   240
  /* pretty printing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   241
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   242
  val Consistent = new Properties.Boolean("consistent")
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   243
  val Indent = new Properties.Int("indent")
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   244
  val Width = new Properties.Int("width")
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   245
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   246
  object Block
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   247
  {
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   248
    val name = "block"
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   249
    def apply(c: Boolean, i: Int): Markup =
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   250
      Markup(name,
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   251
        (if (c) Consistent(c) else Nil) :::
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   252
        (if (i != 0) Indent(i) else Nil))
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   253
    def unapply(markup: Markup): Option[(Boolean, Int)] =
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   254
      if (markup.name == name) {
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   255
        val c = Consistent.unapply(markup.properties).getOrElse(false)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   256
        val i = Indent.unapply(markup.properties).getOrElse(0)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   257
        Some((c, i))
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   258
      }
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   259
      else None
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   260
  }
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   261
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   262
  object Break
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   263
  {
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   264
    val name = "break"
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   265
    def apply(w: Int, i: Int): Markup =
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   266
      Markup(name,
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   267
        (if (w != 0) Width(w) else Nil) :::
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   268
        (if (i != 0) Indent(i) else Nil))
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   269
    def unapply(markup: Markup): Option[(Int, Int)] =
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   270
      if (markup.name == name) {
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   271
        val w = Width.unapply(markup.properties).getOrElse(0)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   272
        val i = Indent.unapply(markup.properties).getOrElse(0)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61862
diff changeset
   273
        Some((w, i))
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   274
      }
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   275
      else None
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 61660
diff changeset
   276
  }
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   277
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
   278
  val ITEM = "item"
51574
2b58d7b139d6 ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents: 51570
diff changeset
   279
  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
   280
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   281
  val SEPARATOR = "separator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   282
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   283
56548
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56278
diff changeset
   284
  /* text properties */
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56278
diff changeset
   285
ae6870efc28d markup for prose words within formal comments;
wenzelm
parents: 56278
diff changeset
   286
  val WORDS = "words"
50201
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 HIDDEN = "hidden"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   289
68298
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68148
diff changeset
   290
  val DELETE = "delete"
2c3ce27cf4a8 markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents: 68148
diff changeset
   291
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   292
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 57595
diff changeset
   293
  /* misc entities */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   294
72781
15a8de807f21 tuned signature;
wenzelm
parents: 72711
diff changeset
   295
  val THEORY = "theory"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   296
  val CLASS = "class"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   297
  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
   298
  val FIXED = "fixed"
53378
07990ba8c0ea cases: more position information and PIDE markup;
wenzelm
parents: 53055
diff changeset
   299
  val CASE = "case"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   300
  val CONSTANT = "constant"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   301
  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
   302
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   303
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   304
  /* inner syntax */
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 TFREE = "tfree"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   307
  val TVAR = "tvar"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   308
  val FREE = "free"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   309
  val SKOLEM = "skolem"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   310
  val BOUND = "bound"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   311
  val VAR = "var"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   312
  val NUMERAL = "numeral"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   313
  val LITERAL = "literal"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   314
  val DELIMITER = "delimiter"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   315
  val INNER_STRING = "inner_string"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   316
  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
   317
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   318
  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
   319
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   320
  val SORTING = "sorting"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   321
  val TYPING = "typing"
63347
e344dc82f6c2 report class parameters within instantiation;
wenzelm
parents: 63337
diff changeset
   322
  val CLASS_PARAMETER = "class_parameter"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   323
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   324
  val ATTRIBUTE = "attribute"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   325
  val METHOD = "method"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   326
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   327
55550
bcc643ac071a generic markup for embedded languages;
wenzelm
parents: 55526
diff changeset
   328
  /* antiquotations */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   329
55526
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   330
  val ANTIQUOTED = "antiquoted"
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   331
  val ANTIQUOTE = "antiquote"
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
   332
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   333
  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
   334
  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
   335
  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
   336
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   337
70135
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   338
  /* document text */
69965
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69962
diff changeset
   339
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69962
diff changeset
   340
  val RAW_TEXT = "raw_text"
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69962
diff changeset
   341
  val PLAIN_TEXT = "plain_text"
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69962
diff changeset
   342
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   343
  val PARAGRAPH = "paragraph"
50545
00bdc48c5f71 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents: 50543
diff changeset
   344
  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
   345
70135
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   346
  object Document_Tag
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   347
  {
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   348
    val ELEMENT = "document_tag"
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   349
    val IMPORTANT = "important"
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   350
    val UNIMPORTANT = "unimportant"
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   351
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   352
    def unapply(markup: Markup): Option[String] =
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   353
      markup match {
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   354
        case Markup(ELEMENT, Name(name)) => Some(name)
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   355
        case _ => None
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   356
      }
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   357
  }
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 70016
diff changeset
   358
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   359
61449
4f31f79cf2d1 report Markdown document structure;
wenzelm
parents: 60882
diff changeset
   360
  /* Markdown document structure */
4f31f79cf2d1 report Markdown document structure;
wenzelm
parents: 60882
diff changeset
   361
4f31f79cf2d1 report Markdown document structure;
wenzelm
parents: 60882
diff changeset
   362
  val MARKDOWN_PARAGRAPH = "markdown_paragraph"
67323
d02208cefbdb PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents: 67322
diff changeset
   363
  val MARKDOWN_ITEM = "markdown_item"
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   364
  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
61449
4f31f79cf2d1 report Markdown document structure;
wenzelm
parents: 60882
diff changeset
   365
  val Markdown_List = new Markup_String("markdown_list", "kind")
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   366
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   367
  val ITEMIZE = "itemize"
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   368
  val ENUMERATE = "enumerate"
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   369
  val DESCRIPTION = "description"
61449
4f31f79cf2d1 report Markdown document structure;
wenzelm
parents: 60882
diff changeset
   370
4f31f79cf2d1 report Markdown document structure;
wenzelm
parents: 60882
diff changeset
   371
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
   372
  /* ML */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   373
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   374
  val ML_KEYWORD1 = "ML_keyword1"
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   375
  val ML_KEYWORD2 = "ML_keyword2"
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55390
diff changeset
   376
  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
   377
  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
   378
  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
   379
  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
   380
  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
   381
  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
   382
  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
   383
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   384
  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
   385
  val ML_OPEN = "ML_open"
55837
154855d9a564 clarified names of antiquotations and markup;
wenzelm
parents: 55828
diff changeset
   386
  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
   387
  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
   388
60744
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
   389
  val ML_BREAKPOINT = "ML_breakpoint"
4eba53a0ac3d report possible breakpoint positions;
wenzelm
parents: 59707
diff changeset
   390
50201
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
  /* outer syntax */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   393
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55694
diff changeset
   394
  val COMMAND = "command"
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 65937
diff changeset
   395
  val KEYWORD = "keyword"
55744
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55694
diff changeset
   396
  val KEYWORD1 = "keyword1"
4a4e5686e091 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents: 55694
diff changeset
   397
  val KEYWORD2 = "keyword2"
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55744
diff changeset
   398
  val KEYWORD3 = "keyword3"
55919
2eb8c13339a5 more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents: 55914
diff changeset
   399
  val QUASI_KEYWORD = "quasi_keyword"
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 55919
diff changeset
   400
  val IMPROPER = "improper"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   401
  val OPERATOR = "operator"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   402
  val STRING = "string"
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 58978
diff changeset
   403
  val ALT_STRING = "alt_string"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   404
  val VERBATIM = "verbatim"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54702
diff changeset
   405
  val CARTOUCHE = "cartouche"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   406
  val COMMENT = "comment"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   407
72782
98ecb951d911 more completion;
wenzelm
parents: 72781
diff changeset
   408
  val LOAD_COMMAND = "load_command"
98ecb951d911 more completion;
wenzelm
parents: 72781
diff changeset
   409
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   410
69320
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   411
  /* comments */
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   412
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   413
  val COMMENT1 = "comment1"
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   414
  val COMMENT2 = "comment2"
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   415
  val COMMENT3 = "comment3"
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   416
fc221fa79741 more comment markup;
wenzelm
parents: 68997
diff changeset
   417
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   418
  /* timing */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   419
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   420
  val Elapsed = new Properties.Double("elapsed")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   421
  val CPU = new Properties.Double("cpu")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   422
  val GC = new Properties.Double("gc")
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   423
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   424
  object Timing_Properties
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   425
  {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   426
    def apply(timing: isabelle.Timing): Properties.T =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   427
      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
   428
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   429
    def unapply(props: Properties.T): Option[isabelle.Timing] =
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   430
      (props, props, props) match {
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   431
        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   432
          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   433
        case _ => None
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   434
      }
72013
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72008
diff changeset
   435
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72008
diff changeset
   436
    def parse(props: Properties.T): isabelle.Timing =
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72008
diff changeset
   437
      unapply(props) getOrElse isabelle.Timing.zero
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   438
  }
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   439
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   440
  val TIMING = "timing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   441
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   442
  object Timing
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   443
  {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   444
    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
   445
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   446
    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
   447
      markup match {
50781
a0f22c2d60cc standardized treatment of timing properties;
wenzelm
parents: 50715
diff changeset
   448
        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
   449
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   450
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   451
  }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   452
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   453
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   454
  /* process result */
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   455
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   456
  val Return_Code = new Properties.Int("return_code")
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   457
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   458
  object Process_Result
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   459
  {
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   460
    def apply(result: Process_Result): Properties.T =
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   461
      Return_Code(result.rc) :::
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   462
        (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   463
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   464
    def unapply(props: Properties.T): Option[Process_Result] =
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   465
      props match {
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   466
        case Return_Code(rc) =>
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   467
          val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   468
          Some(isabelle.Process_Result(rc, timing = timing))
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   469
        case _ => None
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   470
      }
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   471
  }
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   472
b9f5cd845616 more informative session result;
wenzelm
parents: 65313
diff changeset
   473
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   474
  /* command indentation */
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   475
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   476
  object Command_Indent
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   477
  {
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   478
    val name = "command_indent"
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   479
    def unapply(markup: Markup): Option[Int] =
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   480
      if (markup.name == name) Indent.unapply(markup.properties) else None
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   481
  }
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   482
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   483
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63347
diff changeset
   484
  /* goals */
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   485
50543
42bbe637be54 fold main goal;
wenzelm
parents: 50503
diff changeset
   486
  val GOAL = "goal"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   487
  val SUBGOAL = "subgoal"
50215
97959912840a more general sendback properties;
wenzelm
parents: 50201
diff changeset
   488
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
diff changeset
   489
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   490
  /* command status */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   491
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   492
  val TASK = "task"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   493
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   494
  val ACCEPTED = "accepted"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   495
  val FORKED = "forked"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   496
  val JOINED = "joined"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   497
  val RUNNING = "running"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   498
  val FINISHED = "finished"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   499
  val FAILED = "failed"
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68822
diff changeset
   500
  val CANCELED = "canceled"
68323
bf7336731981 more node status information;
wenzelm
parents: 68298
diff changeset
   501
  val INITIALIZED = "initialized"
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68871
diff changeset
   502
  val FINALIZED = "finalized"
70780
034742453594 more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents: 70665
diff changeset
   503
  val CONSOLIDATING = "consolidating"
66379
6392766f3c25 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents: 66044
diff changeset
   504
  val CONSOLIDATED = "consolidated"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   505
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   506
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   507
  /* interactive documents */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   508
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   509
  val VERSION = "version"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   510
  val ASSIGN = "assign"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   511
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   512
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   513
  /* prover process */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   514
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   515
  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
   516
  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
   517
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   518
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   519
  /* messages */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   520
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   521
  val INIT = "init"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   522
  val STATUS = "status"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   523
  val REPORT = "report"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   524
  val RESULT = "result"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   525
  val WRITELN = "writeln"
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   526
  val STATE = "state"
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   527
  val INFORMATION = "information"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   528
  val TRACING = "tracing"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   529
  val WARNING = "warning"
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59186
diff changeset
   530
  val LEGACY = "legacy"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   531
  val ERROR = "error"
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68323
diff changeset
   532
  val NODES_STATUS = "nodes_status"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   533
  val PROTOCOL = "protocol"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   534
  val SYSTEM = "system"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   535
  val STDOUT = "stdout"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   536
  val STDERR = "stderr"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   537
  val EXIT = "exit"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   538
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   539
  val WRITELN_MESSAGE = "writeln_message"
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   540
  val STATE_MESSAGE = "state_message"
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   541
  val INFORMATION_MESSAGE = "information_message"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   542
  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
   543
  val WARNING_MESSAGE = "warning_message"
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59186
diff changeset
   544
  val LEGACY_MESSAGE = "legacy_message"
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   545
  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
   546
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   547
  val messages = Map(
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   548
    WRITELN -> WRITELN_MESSAGE,
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   549
    STATE -> STATE_MESSAGE,
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   550
    INFORMATION -> INFORMATION_MESSAGE,
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   551
    TRACING -> TRACING_MESSAGE,
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   552
    WARNING -> WARNING_MESSAGE,
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59186
diff changeset
   553
    LEGACY -> LEGACY_MESSAGE,
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   554
    ERROR -> ERROR_MESSAGE)
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59112
diff changeset
   555
52876
78989972d5b8 more explicit status for query operation;
wenzelm
parents: 52854
diff changeset
   556
  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
   557
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   558
  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
   559
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   560
  val BAD = "bad"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   561
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   562
  val INTENSIFY = "intensify"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   563
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   564
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   565
  /* active areas */
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   566
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50545
diff changeset
   567
  val BROWSER = "browser"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   568
  val GRAPHVIEW = "graphview"
69650
c95edf19133b clarified message;
wenzelm
parents: 69648
diff changeset
   569
  val THEORY_EXPORTS = "theory_exports"
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   570
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   571
  val SENDBACK = "sendback"
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   572
  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
   573
  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
   574
  val PADDING_COMMAND = (PADDING, "command")
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   575
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   576
  val DIALOG = "dialog"
50503
50f141b34bb7 enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents: 50501
diff changeset
   577
  val Result = new Properties.String(RESULT)
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   578
63681
d2448471ffba active jEdit actions;
wenzelm
parents: 63475
diff changeset
   579
  val JEDIT_ACTION = "jedit_action"
d2448471ffba active jEdit actions;
wenzelm
parents: 63475
diff changeset
   580
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   581
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   582
  /* protocol message functions */
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   583
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   584
  val FUNCTION = "function"
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   585
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   586
  class Function(val name: String)
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   587
  {
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   588
    val PROPERTY: Properties.Entry = (FUNCTION, name)
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   589
  }
66942
91a21a5631ae proper order of initialization (amending 9953ae603a23);
wenzelm
parents: 66873
diff changeset
   590
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   591
  class Properties_Function(name: String) extends Function(name)
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   592
  {
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   593
    def unapply(props: Properties.T): Option[Properties.T] =
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   594
      props match {
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   595
        case PROPERTY :: args => Some(args)
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   596
        case _ => None
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   597
      }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   598
  }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   599
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   600
  class Name_Function(name: String) extends Function(name)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   601
  {
72112
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   602
    def unapply(props: Properties.T): Option[String] =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   603
      props match {
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   604
        case List(PROPERTY, (NAME, a)) => Some(a)
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   605
        case _ => None
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   606
      }
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   607
  }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 51818
diff changeset
   608
72116
7773ec172572 clarified names;
wenzelm
parents: 72112
diff changeset
   609
  object ML_Statistics extends Function("ML_statistics")
72112
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   610
  {
72119
d115d50a19c0 provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents: 72116
diff changeset
   611
    def unapply(props: Properties.T): Option[(Long, String)] =
72112
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   612
      props match {
72119
d115d50a19c0 provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents: 72116
diff changeset
   613
        case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
d115d50a19c0 provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents: 72116
diff changeset
   614
          Some((pid, stats_dir))
72112
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   615
        case _ => None
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   616
      }
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   617
  }
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   618
72107
1b06ed254943 more compact command_timings, as in former batch-build;
wenzelm
parents: 72013
diff changeset
   619
  val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
72711
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72708
diff changeset
   620
  def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
72107
1b06ed254943 more compact command_timings, as in former batch-build;
wenzelm
parents: 72013
diff changeset
   621
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   622
  object Command_Timing extends Properties_Function("command_timing")
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   623
  object Theory_Timing extends Properties_Function("theory_timing")
72002
5c4800f6b25a more robust protocol for "Timing ..." messages, notably for pide_session=true;
wenzelm
parents: 71673
diff changeset
   624
  object Session_Timing extends Properties_Function("session_timing")
72008
7a53fc156c2b proper session Timing for build_history log file (see 5c4800f6b25a);
wenzelm
parents: 72002
diff changeset
   625
  {
72013
6a24ecc4ff1b clarified signature;
wenzelm
parents: 72008
diff changeset
   626
    val Threads = new Properties.Int("threads")
72008
7a53fc156c2b proper session Timing for build_history log file (see 5c4800f6b25a);
wenzelm
parents: 72002
diff changeset
   627
  }
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   628
  object Task_Statistics extends Properties_Function("task_statistics")
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   629
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72332
diff changeset
   630
  object Loading_Theory extends Properties_Function("loading_theory")
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   631
  object Build_Session_Finished extends Function("build_session_finished")
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   632
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   633
  object Commands_Accepted extends Function("commands_accepted")
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   634
  object Assign_Update extends Function("assign_update")
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   635
  object Removed_Versions extends Function("removed_versions")
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   636
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   637
  object Invoke_Scala extends Function("invoke_scala")
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   638
  {
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
   639
    def unapply(props: Properties.T): Option[(String, String, Boolean)] =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49613
diff changeset
   640
      props match {
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
   641
        case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) =>
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72156
diff changeset
   642
          Some((name, id, thread))
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   643
        case _ => None
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   644
      }
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50215
diff changeset
   645
  }
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   646
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   647
  object Cancel_Scala extends Function("cancel_scala")
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   648
  {
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   649
    def unapply(props: Properties.T): Option[String] =
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   650
      props match {
71673
88dfbc382a3d clarified signature;
wenzelm
parents: 71624
diff changeset
   651
        case List(PROPERTY, (ID, id)) => Some(id)
50975
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   652
        case _ => None
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   653
      }
73ec6ad6700e more systematic task statistics;
wenzelm
parents: 50781
diff changeset
   654
  }
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
   655
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69650
diff changeset
   656
  val PRINT_OPERATIONS = "print_operations"
c175499a7537 added executable flag for exports;
wenzelm
parents: 69650
diff changeset
   657
c175499a7537 added executable flag for exports;
wenzelm
parents: 69650
diff changeset
   658
c175499a7537 added executable flag for exports;
wenzelm
parents: 69650
diff changeset
   659
  /* export */
c175499a7537 added executable flag for exports;
wenzelm
parents: 69650
diff changeset
   660
68088
0763d4eb3ebc protocol message for export of theory resources;
wenzelm
parents: 67870
diff changeset
   661
  val EXPORT = "export"
71624
f0499449e149 clarified modules;
wenzelm
parents: 71623
diff changeset
   662
  val THEORY_NAME = "theory_name"
f0499449e149 clarified modules;
wenzelm
parents: 71623
diff changeset
   663
  val EXECUTABLE = "executable"
f0499449e149 clarified modules;
wenzelm
parents: 71623
diff changeset
   664
  val COMPRESS = "compress"
f0499449e149 clarified modules;
wenzelm
parents: 71623
diff changeset
   665
  val STRICT = "strict"
68088
0763d4eb3ebc protocol message for export of theory resources;
wenzelm
parents: 67870
diff changeset
   666
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   667
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   668
  /* debugger output */
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   669
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   670
  val DEBUGGER_STATE = "debugger_state"
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   671
  object Debugger_State
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   672
  {
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   673
    def unapply(props: Properties.T): Option[String] =
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   674
      props match {
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   675
        case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   676
        case _ => None
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   677
      }
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   678
  }
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   679
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   680
  val DEBUGGER_OUTPUT = "debugger_output"
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   681
  object Debugger_Output
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   682
  {
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60831
diff changeset
   683
    def unapply(props: Properties.T): Option[String] =
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   684
      props match {
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60831
diff changeset
   685
        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   686
        case _ => None
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   687
      }
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   688
  }
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   689
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60744
diff changeset
   690
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
   691
  /* 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
   692
57594
037f3b251df5 regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents: 56864
diff changeset
   693
  val SIMP_TRACE_PANEL = "simp_trace_panel"
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
   694
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   695
  val SIMP_TRACE_LOG = "simp_trace_log"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   696
  val SIMP_TRACE_STEP = "simp_trace_step"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   697
  val SIMP_TRACE_RECURSE = "simp_trace_recurse"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   698
  val SIMP_TRACE_HINT = "simp_trace_hint"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   699
  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
   700
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   701
  val SIMP_TRACE_CANCEL = "simp_trace_cancel"
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   702
  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
   703
  {
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
   704
    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
   705
      props match {
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55551
diff changeset
   706
        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
   707
        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
   708
      }
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
   709
  }
65335
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   710
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   711
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   712
  /* XML data representation */
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   713
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   714
  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   715
  {
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   716
    import XML.Encode._
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   717
    pair(string, properties)((markup.name, markup.properties))
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   718
  }
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   719
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   720
  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   721
  {
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   722
    import XML.Decode._
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   723
    val (name, props) = pair(string, properties)(body)
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   724
    Markup(name, props)
7634d33c1a79 support to encode/decode command state;
wenzelm
parents: 65317
diff changeset
   725
  }
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   726
}
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   727
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
   728
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   729
sealed case class Markup(name: String, properties: Properties.T)
59707
10effab11669 tuned signature;
wenzelm
parents: 59369
diff changeset
   730
{
10effab11669 tuned signature;
wenzelm
parents: 59369
diff changeset
   731
  def markup(s: String): String =
10effab11669 tuned signature;
wenzelm
parents: 59369
diff changeset
   732
    YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
64358
15c90b744481 more operations (see also properties.ML);
wenzelm
parents: 63681
diff changeset
   733
15c90b744481 more operations (see also properties.ML);
wenzelm
parents: 63681
diff changeset
   734
  def update_properties(more_props: Properties.T): Markup =
15c90b744481 more operations (see also properties.ML);
wenzelm
parents: 63681
diff changeset
   735
    if (more_props.isEmpty) this
15c90b744481 more operations (see also properties.ML);
wenzelm
parents: 63681
diff changeset
   736
    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
65753
787e5ee6ef53 more operations;
wenzelm
parents: 65335
diff changeset
   737
787e5ee6ef53 more operations;
wenzelm
parents: 65335
diff changeset
   738
  def + (entry: Properties.Entry): Markup =
787e5ee6ef53 more operations;
wenzelm
parents: 65335
diff changeset
   739
    Markup(name, Properties.put(properties, entry))
59707
10effab11669 tuned signature;
wenzelm
parents: 59369
diff changeset
   740
}