src/Pure/Isar/antiquote.ML

RuleContext.intro_query_local;

(*  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;