1.1 --- a/src/Pure/PIDE/markup.ML	Fri Sep 26 14:29:06 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Fri Sep 26 15:05:11 2014 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4    val position_properties': string list
     1.5    val position_properties: string list
     1.6    val positionN: string val position: T
     1.7 +  val expressionN: string val expression: T
     1.8    val pathN: string val path: string -> T
     1.9    val urlN: string val url: string -> T
    1.10    val indentN: string
    1.11 @@ -340,6 +341,11 @@
    1.12  val (positionN, position) = markup_elem "position";
    1.13  
    1.14  
    1.15 +(* expression *)
    1.16 +
    1.17 +val (expressionN, expression) = markup_elem "expression";
    1.18 +
    1.19 +
    1.20  (* external resources *)
    1.21  
    1.22  val (pathN, path) = markup_string "path" nameN;

     2.1 --- a/src/Pure/PIDE/markup.scala	Fri Sep 26 14:29:06 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Fri Sep 26 15:05:11 2014 +0200
     2.3 @@ -115,6 +115,11 @@
     2.4    val POSITION = "position"
     2.5  
     2.6  
     2.7 +  /* expression */
     2.8 +
     2.9 +  val EXPRESSION = "expression"
    2.10 +
    2.11 +
    2.12    /* embedded languages */
    2.13  
    2.14    val Symbols = new Properties.Boolean("symbols")

     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Sep 26 14:29:06 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Sep 26 15:05:11 2014 +0200
     3.3 @@ -139,8 +139,8 @@
     3.4    private val language_elements = Markup.Elements(Markup.LANGUAGE)
     3.5  
     3.6    private val highlight_elements =
     3.7 -    Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
     3.8 -      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
     3.9 +    Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
    3.10 +      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    3.11        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    3.12        Markup.VAR, Markup.TFREE, Markup.TVAR)
    3.13  
    3.14 @@ -156,6 +156,7 @@
    3.15  
    3.16    private val tooltip_descriptions =
    3.17      Map(
    3.18 +      Markup.EXPRESSION -> "expression",
    3.19        Markup.TOKEN_RANGE -> "inner syntax token",
    3.20        Markup.FREE -> "free variable",
    3.21        Markup.SKOLEM -> "skolem variable",