# HG changeset patch
# User wenzelm
# Date 1392998154 -3600
# Node ID 528de9a2005443a8f598825261e34574d5612d68
# Parent  33ad12ef79ffba592d88984f29703a34f72327d4
more markup -- complete symbols within antiquotation, notably with broken arguments;

diff -r 33ad12ef79ff -r 528de9a20054 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Feb 21 16:14:35 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Fri Feb 21 16:55:54 2014 +0100
@@ -32,7 +32,8 @@
 (* reports *)
 
 fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
-  [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
+  [(start, Markup.antiquote), (stop, Markup.antiquote),
+   (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)];
 
 fun antiquote_reports text =
   maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
diff -r 33ad12ef79ff -r 528de9a20054 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Feb 21 16:14:35 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Feb 21 16:55:54 2014 +0100
@@ -28,6 +28,7 @@
   val language_prop: T
   val language_ML: T
   val language_document: T
+  val language_antiquotation: T
   val language_text: T
   val language_rail: T
   val bindingN: string val binding: T
@@ -255,9 +256,9 @@
 val language_type = language "type" true;
 val language_term = language "term" true;
 val language_prop = language "prop" true;
-
 val language_ML = language "ML" false;
 val language_document = language "document" false;
+val language_antiquotation = language "antiquotation" true;
 val language_text = language "text" true;
 val language_rail = language "rail" true;