src/Pure/Isar/antiquote.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 19305 5c16895d548b
child 22114 560c5b5dda1c
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     1 (*  Title:      Pure/Isar/antiquote.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Text with antiquotations of inner items (terms, types etc.).
     6 *)
     7 
     8 signature ANTIQUOTE =
     9 sig
    10   exception ANTIQUOTE_FAIL of (string * Position.T) * exn
    11   datatype antiquote = Text of string | Antiq of string * Position.T
    12   val is_antiq: antiquote -> bool
    13   val antiquotes_of: string * Position.T -> antiquote list
    14 end;
    15 
    16 structure Antiquote: ANTIQUOTE =
    17 struct
    18 
    19 (* datatype antiquote *)
    20 
    21 exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
    22 
    23 datatype antiquote =
    24   Text of string |
    25   Antiq of string * Position.T;
    26 
    27 fun is_antiq (Text _) = false
    28   | is_antiq (Antiq _) = true;
    29 
    30 
    31 (* scan_antiquote *)
    32 
    33 local
    34 
    35 structure T = OuterLex;
    36 
    37 val scan_txt =
    38   T.scan_blank ||
    39   T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
    40   T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    41 
    42 fun escape "\\" = "\\\\"
    43   | escape "\"" = "\\\""
    44   | escape s = s;
    45 
    46 val quote_escape = Library.quote o implode o map escape o Symbol.explode;
    47 
    48 val scan_ant =
    49   T.scan_blank ||
    50   T.scan_string >> quote_escape ||
    51   T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    52 
    53 val scan_antiq =
    54   T.keep_line ($$ "@" -- $$ "{") |--
    55     T.!!! "missing closing brace of antiquotation"
    56       (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
    57 
    58 in
    59 
    60 fun scan_antiquote (pos, ss) = (pos, ss) |>
    61   (Scan.repeat1 scan_txt >> (Text o implode) ||
    62     scan_antiq >> (fn s => Antiq (s, pos)));
    63 
    64 end;
    65 
    66 
    67 (* antiquotes_of *)
    68 
    69 fun antiquotes_of (s, pos) =
    70   (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
    71       (pos, Symbol.explode s) of
    72     (xs, (_, [])) => xs
    73   | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
    74       quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
    75 
    76 
    77 end;