# HG changeset patch
# User wenzelm
# Date 1411736711 -7200
# Node ID 5e7fc9974abaad94fe1a7bcd4a4531c55e82cff2
# Parent  0bf0e9788d54ad5eff4ef24d1e389e829ee3631a
support for sub-expression markup;

diff -r 0bf0e9788d54 -r 5e7fc9974aba src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Sep 26 14:29:06 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Sep 26 15:05:11 2014 +0200
@@ -54,6 +54,7 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
+  val expressionN: string val expression: T
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
   val indentN: string
@@ -340,6 +341,11 @@
 val (positionN, position) = markup_elem "position";
 
 
+(* expression *)
+
+val (expressionN, expression) = markup_elem "expression";
+
+
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
diff -r 0bf0e9788d54 -r 5e7fc9974aba src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Sep 26 14:29:06 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Sep 26 15:05:11 2014 +0200
@@ -115,6 +115,11 @@
   val POSITION = "position"
 
 
+  /* expression */
+
+  val EXPRESSION = "expression"
+
+
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
diff -r 0bf0e9788d54 -r 5e7fc9974aba src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Sep 26 14:29:06 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Sep 26 15:05:11 2014 +0200
@@ -139,8 +139,8 @@
   private val language_elements = Markup.Elements(Markup.LANGUAGE)
 
   private val highlight_elements =
-    Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
-      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
+    Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
+      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR)
 
@@ -156,6 +156,7 @@
 
   private val tooltip_descriptions =
     Map(
+      Markup.EXPRESSION -> "expression",
       Markup.TOKEN_RANGE -> "inner syntax token",
       Markup.FREE -> "free variable",
       Markup.SKOLEM -> "skolem variable",