src/Pure/Isar/antiquote.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 9138 6a4fae41a75f
child 12881 eeb36b66480e
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/antiquote.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Text with antiquotations of inner items (terms, types etc.).
     7 *)
     8 
     9 signature ANTIQUOTE =
    10 sig
    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 datatype antiquote =
    22   Text of string |
    23   Antiq of string * Position.T;
    24 
    25 fun is_antiq (Text _) = false
    26   | is_antiq (Antiq _) = true;
    27 
    28 
    29 (* scan_antiquote *)
    30 
    31 local
    32 
    33 structure T = OuterLex;
    34 
    35 val scan_txt =
    36   T.scan_blank ||
    37   T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
    38   T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
    39 
    40 fun escape "\\" = "\\\\"
    41   | escape "\"" = "\\\""
    42   | escape s = s;
    43 
    44 val quote_escape = quote o implode o map escape o Symbol.explode;
    45 
    46 val scan_ant =
    47   T.scan_blank ||
    48   T.scan_string >> quote_escape ||
    49   T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
    50 
    51 val scan_antiq =
    52   T.keep_line ($$ "@" -- $$ "{") |--
    53     T.!!! "missing closing brace of antiquotation"
    54       (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
    55 
    56 in
    57 
    58 fun scan_antiquote (pos, ss) = (pos, ss) |>
    59   (Scan.repeat1 scan_txt >> (Text o implode) ||
    60     scan_antiq >> (fn s => Antiq (s, pos)));
    61 
    62 end;
    63 
    64 
    65 (* antiquotes_of *)
    66 
    67 fun antiquotes_of (s, pos) =
    68   (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
    69       (pos, Symbol.explode s) of
    70     (xs, (_, [])) => xs
    71   | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
    72       quote (Symbol.beginning ss) ^ Position.str_of pos'));
    73 
    74 
    75 end;