more markup -- complete symbols within antiquotation, notably with broken arguments;
--- 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));
--- 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;