more markup -- complete symbols within antiquotation, notably with broken arguments;
authorwenzelm
Fri, 21 Feb 2014 16:55:54 +0100
changeset 55653 528de9a20054
parent 55652 33ad12ef79ff
child 55654 5ff4742f27ec
more markup -- complete symbols within antiquotation, notably with broken arguments;
src/Pure/General/antiquote.ML
src/Pure/PIDE/markup.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));
--- 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;