1.1 --- a/src/Pure/General/antiquote.ML	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Mon Feb 17 11:14:26 2014 +0100
     1.3 @@ -6,13 +6,12 @@
     1.4  
     1.5  signature ANTIQUOTE =
     1.6  sig
     1.7 -  datatype 'a antiquote =
     1.8 -    Text of 'a |
     1.9 -    Antiq of Symbol_Pos.T list * Position.range
    1.10 +  type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
    1.11 +  datatype 'a antiquote = Text of 'a | Antiq of antiq
    1.12    val is_text: 'a antiquote -> bool
    1.13    val reports_of: ('a -> Position.report_text list) ->
    1.14      'a antiquote list -> Position.report_text list
    1.15 -  val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
    1.16 +  val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
    1.17    val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    1.18    val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
    1.19  end;
    1.20 @@ -22,9 +21,8 @@
    1.21  
    1.22  (* datatype antiquote *)
    1.23  
    1.24 -datatype 'a antiquote =
    1.25 -  Text of 'a |
    1.26 -  Antiq of Symbol_Pos.T list * Position.range;
    1.27 +type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
    1.28 +datatype 'a antiquote = Text of 'a | Antiq of antiq;
    1.29  
    1.30  fun is_text (Text _) = true
    1.31    | is_text _ = false;
    1.32 @@ -32,8 +30,11 @@
    1.33  
    1.34  (* reports *)
    1.35  
    1.36 +fun reports_of_antiq ((_, {start, stop, range = (pos, _)}): antiq) =
    1.37 +  map (rpair "") [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
    1.38 +
    1.39  fun reports_of text =
    1.40 -  maps (fn Text x => text x | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]);
    1.41 +  maps (fn Text x => text x | Antiq antiq => reports_of_antiq antiq);
    1.42  
    1.43  
    1.44  (* scan *)
    1.45 @@ -56,10 +57,14 @@
    1.46  in
    1.47  
    1.48  val scan_antiq =
    1.49 -  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
    1.50 +  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
    1.51      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
    1.52 -      (Scan.repeat scan_antiq_body -- ($$ "}" |-- Symbol_Pos.scan_pos)))
    1.53 -  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    1.54 +      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos)))
    1.55 +  >> (fn (pos1, (pos2, ((body, pos3), pos4))) =>
    1.56 +      (flat body,
    1.57 +        {start = Position.set_range (pos1, pos2),
    1.58 +         stop = Position.set_range (pos3, pos4),
    1.59 +         range = Position.range pos1 pos4}));
    1.60  
    1.61  val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text;
    1.62  

     2.1 --- a/src/Pure/ML/ml_context.ML	Sun Feb 16 21:33:28 2014 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Mon Feb 17 11:14:26 2014 +0100
     2.3 @@ -158,7 +158,7 @@
     2.4            fun no_decl _ = ([], []);
     2.5  
     2.6            fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
     2.7 -            | expand (Antiquote.Antiq (ss, range)) ctxt =
     2.8 +            | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
     2.9                  let
    2.10                    val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
    2.11                    val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));

     3.1 --- a/src/Pure/PIDE/markup.ML	Sun Feb 16 21:33:28 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Mon Feb 17 11:14:26 2014 +0100
     3.3 @@ -83,7 +83,8 @@
     3.4    val ML_typingN: string val ML_typing: T
     3.5    val ML_sourceN: string val ML_source: T
     3.6    val document_sourceN: string val document_source: T
     3.7 -  val antiqN: string val antiq: T
     3.8 +  val antiquotedN: string val antiquoted: T
     3.9 +  val antiquoteN: string val antiquote: T
    3.10    val ML_antiquotationN: string
    3.11    val document_antiquotationN: string
    3.12    val document_antiquotation_optionN: string
    3.13 @@ -348,7 +349,9 @@
    3.14  val (ML_sourceN, ML_source) = markup_elem "ML_source";
    3.15  val (document_sourceN, document_source) = markup_elem "document_source";
    3.16  
    3.17 -val (antiqN, antiq) = markup_elem "antiq";
    3.18 +val (antiquotedN, antiquoted) = markup_elem "antiquoted";
    3.19 +val (antiquoteN, antiquote) = markup_elem "antiquote";
    3.20 +
    3.21  val ML_antiquotationN = "ML_antiquotation";
    3.22  val document_antiquotationN = "document_antiquotation";
    3.23  val document_antiquotation_optionN = "document_antiquotation_option";

     4.1 --- a/src/Pure/PIDE/markup.scala	Sun Feb 16 21:33:28 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Mon Feb 17 11:14:26 2014 +0100
     4.3 @@ -155,7 +155,9 @@
     4.4    val ML_SOURCE = "ML_source"
     4.5    val DOCUMENT_SOURCE = "document_source"
     4.6  
     4.7 -  val ANTIQ = "antiq"
     4.8 +  val ANTIQUOTED = "antiquoted"
     4.9 +  val ANTIQUOTE = "antiquote"
    4.10 +
    4.11    val ML_ANTIQUOTATION = "ML_antiquotation"
    4.12    val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
    4.13    val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"

     5.1 --- a/src/Pure/Thy/thy_output.ML	Sun Feb 16 21:33:28 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Feb 17 11:14:26 2014 +0100
     5.3 @@ -23,7 +23,7 @@
     5.4    val boolean: string -> bool
     5.5    val integer: string -> int
     5.6    datatype markup = Markup | MarkupEnv | Verbatim
     5.7 -  val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
     5.8 +  val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
     5.9    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    5.10    val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
    5.11    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    5.12 @@ -165,7 +165,7 @@
    5.13  
    5.14  (* eval_antiquote *)
    5.15  
    5.16 -fun eval_antiq lex state (ss, (pos, _)) =
    5.17 +fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
    5.18    let
    5.19      val (opts, src) = Token.read_antiq lex antiq (ss, pos);
    5.20      fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();

     6.1 --- a/src/Pure/Tools/rail.ML	Sun Feb 16 21:33:28 2014 +0100
     6.2 +++ b/src/Pure/Tools/rail.ML	Mon Feb 17 11:14:26 2014 +0100
     6.3 @@ -13,7 +13,7 @@
     6.4  (* datatype token *)
     6.5  
     6.6  datatype kind =
     6.7 -  Keyword | Ident | String | Antiq of Symbol_Pos.T list * Position.range | EOF;
     6.8 +  Keyword | Ident | String | Antiq of Antiquote.antiq | EOF;
     6.9  
    6.10  datatype token = Token of Position.range * (kind * string);
    6.11  
    6.12 @@ -132,7 +132,7 @@
    6.13    Newline of int |
    6.14    Nonterminal of string |
    6.15    Terminal of bool * string |
    6.16 -  Antiquote of bool * (Symbol_Pos.T list * Position.range);
    6.17 +  Antiquote of bool * Antiquote.antiq;
    6.18  
    6.19  fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
    6.20  and reverse (Bar cats) = Bar (map reverse_cat cats)

     7.1 --- a/src/Tools/jEdit/etc/options	Sun Feb 16 21:33:28 2014 +0100
     7.2 +++ b/src/Tools/jEdit/etc/options	Mon Feb 17 11:14:26 2014 +0100
     7.3 @@ -76,6 +76,7 @@
     7.4  option intensify_color : string = "FFCC6664"
     7.5  option quoted_color : string = "8B8B8B19"
     7.6  option antiquoted_color : string = "FFC83219"
     7.7 +option antiquote_color : string = "6600CCFF"
     7.8  option highlight_color : string = "50505032"
     7.9  option hyperlink_color : string = "000000FF"
    7.10  option active_color : string = "DCDCDCFF"

     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 21:33:28 2014 +0100
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 11:14:26 2014 +0100
     8.3 @@ -177,6 +177,7 @@
     8.4    val intensify_color = color_value("intensify_color")
     8.5    val quoted_color = color_value("quoted_color")
     8.6    val antiquoted_color = color_value("antiquoted_color")
     8.7 +  val antiquote_color = color_value("antiquote_color")
     8.8    val highlight_color = color_value("highlight_color")
     8.9    val hyperlink_color = color_value("hyperlink_color")
    8.10    val active_color = color_value("active_color")
    8.11 @@ -606,13 +607,13 @@
    8.12  
    8.13  
    8.14    private val foreground_include =
    8.15 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ)
    8.16 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
    8.17  
    8.18    def foreground(range: Text.Range): List[Text.Info[Color]] =
    8.19      snapshot.select_markup(range, Some(foreground_include), _ =>
    8.20        {
    8.21          case Text.Info(_, elem) =>
    8.22 -          if (elem.name == Markup.ANTIQ) Some(antiquoted_color)
    8.23 +          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
    8.24            else if (foreground_include.contains(elem.name)) Some(quoted_color)
    8.25            else None
    8.26        })
    8.27 @@ -637,6 +638,7 @@
    8.28        Markup.INNER_CARTOUCHE -> inner_cartouche_color,
    8.29        Markup.INNER_COMMENT -> inner_comment_color,
    8.30        Markup.DYNAMIC_FACT -> dynamic_color,
    8.31 +      Markup.ANTIQUOTE -> antiquote_color,
    8.32        Markup.ML_KEYWORD1 -> keyword1_color,
    8.33        Markup.ML_KEYWORD2 -> keyword2_color,
    8.34        Markup.ML_KEYWORD3 -> keyword3_color,