src/Pure/Isar/antiquote.ML
changeset 9138 6a4fae41a75f
child 12881 eeb36b66480e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/antiquote.ML	Sun Jun 25 23:56:47 2000 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +(*  Title:      Pure/Isar/antiquote.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Text with antiquotations of inner items (terms, types etc.).
    1.10 +*)
    1.11 +
    1.12 +signature ANTIQUOTE =
    1.13 +sig
    1.14 +  datatype antiquote = Text of string | Antiq of string * Position.T
    1.15 +  val is_antiq: antiquote -> bool
    1.16 +  val antiquotes_of: string * Position.T -> antiquote list
    1.17 +end;
    1.18 +
    1.19 +structure Antiquote: ANTIQUOTE =
    1.20 +struct
    1.21 +
    1.22 +(* datatype antiquote *)
    1.23 +
    1.24 +datatype antiquote =
    1.25 +  Text of string |
    1.26 +  Antiq of string * Position.T;
    1.27 +
    1.28 +fun is_antiq (Text _) = false
    1.29 +  | is_antiq (Antiq _) = true;
    1.30 +
    1.31 +
    1.32 +(* scan_antiquote *)
    1.33 +
    1.34 +local
    1.35 +
    1.36 +structure T = OuterLex;
    1.37 +
    1.38 +val scan_txt =
    1.39 +  T.scan_blank ||
    1.40 +  T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
    1.41 +  T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
    1.42 +
    1.43 +fun escape "\\" = "\\\\"
    1.44 +  | escape "\"" = "\\\""
    1.45 +  | escape s = s;
    1.46 +
    1.47 +val quote_escape = quote o implode o map escape o Symbol.explode;
    1.48 +
    1.49 +val scan_ant =
    1.50 +  T.scan_blank ||
    1.51 +  T.scan_string >> quote_escape ||
    1.52 +  T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
    1.53 +
    1.54 +val scan_antiq =
    1.55 +  T.keep_line ($$ "@" -- $$ "{") |--
    1.56 +    T.!!! "missing closing brace of antiquotation"
    1.57 +      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
    1.58 +
    1.59 +in
    1.60 +
    1.61 +fun scan_antiquote (pos, ss) = (pos, ss) |>
    1.62 +  (Scan.repeat1 scan_txt >> (Text o implode) ||
    1.63 +    scan_antiq >> (fn s => Antiq (s, pos)));
    1.64 +
    1.65 +end;
    1.66 +
    1.67 +
    1.68 +(* antiquotes_of *)
    1.69 +
    1.70 +fun antiquotes_of (s, pos) =
    1.71 +  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
    1.72 +      (pos, Symbol.explode s) of
    1.73 +    (xs, (_, [])) => xs
    1.74 +  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
    1.75 +      quote (Symbol.beginning ss) ^ Position.str_of pos'));
    1.76 +
    1.77 +
    1.78 +end;