src/Pure/General/antiquote.ML

--- a/src/Pure/General/antiquote.ML	Sun Oct 18 18:09:48 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Sun Oct 18 20:28:29 2015 +0200
@@ -6,14 +6,14 @@
 
 signature ANTIQUOTE =
 sig
-  type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
-  datatype 'a antiquote =
-    Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq
+  type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
+  type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
+  datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
   type text_antiquote = Symbol_Pos.T list antiquote
   val range: text_antiquote list -> Position.range
   val split_lines: text_antiquote list -> text_antiquote list list
   val antiq_reports: 'a antiquote list -> Position.report list
-  val scan_control: Symbol_Pos.T list -> (Symbol_Pos.T * Symbol_Pos.T list) * Symbol_Pos.T list
+  val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
   val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
   val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
@@ -25,15 +25,15 @@
 
 (* datatype antiquote *)
 
-type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
-datatype 'a antiquote =
-  Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq;
+type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
+type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
+datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
 
 type text_antiquote = Symbol_Pos.T list antiquote;
 
 fun antiquote_range (Text ss) = Symbol_Pos.range ss
-  | antiquote_range (Control (s, ss)) = Symbol_Pos.range (s :: ss)
-  | antiquote_range (Antiq (_, {range, ...})) = range;
+  | antiquote_range (Control {range, ...}) = range
+  | antiquote_range (Antiq {range, ...}) = range;
 
 fun range ants =
   if null ants then Position.no_range
@@ -60,8 +60,8 @@
 
 fun antiq_reports ants = ants |> maps
   (fn Text _ => []
-    | Control (s, ss) => [(#1 (Symbol_Pos.range (s :: ss)), Markup.antiquoted)]
-    | Antiq (_, {start, stop, range = (pos, _)}) =>
+    | Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)]
+    | Antiq {start, stop, range = (pos, _), ...} =>
         [(start, Markup.antiquote),
          (stop, Markup.antiquote),
          (pos, Markup.antiquoted),
@@ -91,17 +91,22 @@
 
 val scan_control =
   Scan.one (Symbol.is_control o Symbol_Pos.symbol) --
-  (Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2);
+  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >>
+    (fn ((control, pos), (_, body)) =>
+      let
+        val Symbol.Ctrl name = Symbol.decode control;
+        val range = Symbol_Pos.range ((control, pos) :: body);
+      in {name = (name, pos), range = range, body = body} end);
 
 val scan_antiq =
   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 -- ($$ "}" |-- 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}));
+      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
+    (fn (pos1, (pos2, ((body, pos3), pos4))) =>
+      {start = Position.set_range (pos1, pos2),
+       stop = Position.set_range (pos3, pos4),
+       range = Position.range pos1 pos4,
+       body = flat body});
 
 val scan_antiquote =
   scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;