# HG changeset patch
# User wenzelm
# Date 1392632066 -3600
# Node ID 39708e59f4b010e1be111856a54e7979d81b0adc
# Parent  70b7e91fa1f99e7fd1324843f1e8f2b71573c1a0
more markup;

diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Mon Feb 17 11:14:26 2014 +0100
@@ -6,13 +6,12 @@
 
 signature ANTIQUOTE =
 sig
-  datatype 'a antiquote =
-    Text of 'a |
-    Antiq of Symbol_Pos.T list * Position.range
+  type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
+  datatype 'a antiquote = Text of 'a | Antiq of antiq
   val is_text: 'a antiquote -> bool
   val reports_of: ('a -> Position.report_text list) ->
     'a antiquote list -> Position.report_text list
-  val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
+  val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
   val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
   val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
 end;
@@ -22,9 +21,8 @@
 
 (* datatype antiquote *)
 
-datatype 'a antiquote =
-  Text of 'a |
-  Antiq of Symbol_Pos.T list * Position.range;
+type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
+datatype 'a antiquote = Text of 'a | Antiq of antiq;
 
 fun is_text (Text _) = true
   | is_text _ = false;
@@ -32,8 +30,11 @@
 
 (* reports *)
 
+fun reports_of_antiq ((_, {start, stop, range = (pos, _)}): antiq) =
+  map (rpair "") [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
+
 fun reports_of text =
-  maps (fn Text x => text x | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]);
+  maps (fn Text x => text x | Antiq antiq => reports_of_antiq antiq);
 
 
 (* scan *)
@@ -56,10 +57,14 @@
 in
 
 val scan_antiq =
-  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
+  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
-      (Scan.repeat scan_antiq_body -- ($$ "}" |-- Symbol_Pos.scan_pos)))
-  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
+      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos)))
+  >> (fn (pos1, (pos2, ((body, pos3), pos4))) =>
+      (flat body,
+        {start = Position.set_range (pos1, pos2),
+         stop = Position.set_range (pos3, pos4),
+         range = Position.range pos1 pos4}));
 
 val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text;
 
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Mon Feb 17 11:14:26 2014 +0100
@@ -158,7 +158,7 @@
           fun no_decl _ = ([], []);
 
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
-            | expand (Antiquote.Antiq (ss, range)) ctxt =
+            | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
                 let
                   val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
                   val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Feb 17 11:14:26 2014 +0100
@@ -83,7 +83,8 @@
   val ML_typingN: string val ML_typing: T
   val ML_sourceN: string val ML_source: T
   val document_sourceN: string val document_source: T
-  val antiqN: string val antiq: T
+  val antiquotedN: string val antiquoted: T
+  val antiquoteN: string val antiquote: T
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
@@ -348,7 +349,9 @@
 val (ML_sourceN, ML_source) = markup_elem "ML_source";
 val (document_sourceN, document_source) = markup_elem "document_source";
 
-val (antiqN, antiq) = markup_elem "antiq";
+val (antiquotedN, antiquoted) = markup_elem "antiquoted";
+val (antiquoteN, antiquote) = markup_elem "antiquote";
+
 val ML_antiquotationN = "ML_antiquotation";
 val document_antiquotationN = "document_antiquotation";
 val document_antiquotation_optionN = "document_antiquotation_option";
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Feb 17 11:14:26 2014 +0100
@@ -155,7 +155,9 @@
   val ML_SOURCE = "ML_source"
   val DOCUMENT_SOURCE = "document_source"
 
-  val ANTIQ = "antiq"
+  val ANTIQUOTED = "antiquoted"
+  val ANTIQUOTE = "antiquote"
+
   val ML_ANTIQUOTATION = "ML_antiquotation"
   val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Feb 17 11:14:26 2014 +0100
@@ -23,7 +23,7 @@
   val boolean: string -> bool
   val integer: string -> int
   datatype markup = Markup | MarkupEnv | Verbatim
-  val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
+  val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
@@ -165,7 +165,7 @@
 
 (* eval_antiquote *)
 
-fun eval_antiq lex state (ss, (pos, _)) =
+fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
   let
     val (opts, src) = Token.read_antiq lex antiq (ss, pos);
     fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Pure/Tools/rail.ML	Mon Feb 17 11:14:26 2014 +0100
@@ -13,7 +13,7 @@
 (* datatype token *)
 
 datatype kind =
-  Keyword | Ident | String | Antiq of Symbol_Pos.T list * Position.range | EOF;
+  Keyword | Ident | String | Antiq of Antiquote.antiq | EOF;
 
 datatype token = Token of Position.range * (kind * string);
 
@@ -132,7 +132,7 @@
   Newline of int |
   Nonterminal of string |
   Terminal of bool * string |
-  Antiquote of bool * (Symbol_Pos.T list * Position.range);
+  Antiquote of bool * Antiquote.antiq;
 
 fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
 and reverse (Bar cats) = Bar (map reverse_cat cats)
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Feb 17 11:14:26 2014 +0100
@@ -76,6 +76,7 @@
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
+option antiquote_color : string = "6600CCFF"
 option highlight_color : string = "50505032"
 option hyperlink_color : string = "000000FF"
 option active_color : string = "DCDCDCFF"
diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 11:14:26 2014 +0100
@@ -177,6 +177,7 @@
   val intensify_color = color_value("intensify_color")
   val quoted_color = color_value("quoted_color")
   val antiquoted_color = color_value("antiquoted_color")
+  val antiquote_color = color_value("antiquote_color")
   val highlight_color = color_value("highlight_color")
   val hyperlink_color = color_value("hyperlink_color")
   val active_color = color_value("active_color")
@@ -606,13 +607,13 @@
 
 
   private val foreground_include =
-    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ)
+    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
 
   def foreground(range: Text.Range): List[Text.Info[Color]] =
     snapshot.select_markup(range, Some(foreground_include), _ =>
       {
         case Text.Info(_, elem) =>
-          if (elem.name == Markup.ANTIQ) Some(antiquoted_color)
+          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
           else if (foreground_include.contains(elem.name)) Some(quoted_color)
           else None
       })
@@ -637,6 +638,7 @@
       Markup.INNER_CARTOUCHE -> inner_cartouche_color,
       Markup.INNER_COMMENT -> inner_comment_color,
       Markup.DYNAMIC_FACT -> dynamic_color,
+      Markup.ANTIQUOTE -> antiquote_color,
       Markup.ML_KEYWORD1 -> keyword1_color,
       Markup.ML_KEYWORD2 -> keyword2_color,
       Markup.ML_KEYWORD3 -> keyword3_color,