src/Pure/Isar/antiquote.ML

+(*  Title:      Pure/Isar/antiquote.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Text with antiquotations of inner items (terms, types etc.).
+*)
+
+signature ANTIQUOTE =
+sig
+  datatype antiquote = Text of string | Antiq of string * Position.T
+  val is_antiq: antiquote -> bool
+  val antiquotes_of: string * Position.T -> antiquote list
+end;
+
+structure Antiquote: ANTIQUOTE =
+struct
+
+(* datatype antiquote *)
+
+datatype antiquote =
+  Text of string |
+  Antiq of string * Position.T;
+
+fun is_antiq (Text _) = false
+  | is_antiq (Antiq _) = true;
+
+
+(* scan_antiquote *)
+
+local
+
+structure T = OuterLex;
+
+val scan_txt =
+  T.scan_blank ||
+  T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
+  T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
+
+fun escape "\\" = "\\\\"
+  | escape "\"" = "\\\""
+  | escape s = s;
+
+val quote_escape = quote o implode o map escape o Symbol.explode;
+
+val scan_ant =
+  T.scan_blank ||
+  T.scan_string >> quote_escape ||
+  T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
+
+val scan_antiq =
+  T.keep_line ($$ "@" -- $$ "{") |--
+    T.!!! "missing closing brace of antiquotation"
+      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
+
+in
+
+fun scan_antiquote (pos, ss) = (pos, ss) |>
+  (Scan.repeat1 scan_txt >> (Text o implode) ||
+    scan_antiq >> (fn s => Antiq (s, pos)));
+
+end;
+
+
+(* antiquotes_of *)
+
+fun antiquotes_of (s, pos) =
+  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
+      (pos, Symbol.explode s) of
+    (xs, (_, [])) => xs
+  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
+      quote (Symbol.beginning ss) ^ Position.str_of pos'));
+
+
+end;