src/Pure/Isar/antiquote.ML
author wenzelm
Sun Jul 08 19:51:58 2007 +0200 (2007-07-08)
changeset 23655 d2d1138e0ddc
parent 22114 560c5b5dda1c
child 23677 1114cc909800
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
     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 scan_antiquotes: string * Position.T -> antiquote list
    14   val scan_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
    15     string * Position.T -> 'a
    16 end;
    17 
    18 structure Antiquote: ANTIQUOTE =
    19 struct
    20 
    21 (* datatype antiquote *)
    22 
    23 exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
    24 
    25 datatype antiquote =
    26   Text of string |
    27   Antiq of string * Position.T;
    28 
    29 fun is_antiq (Text _) = false
    30   | is_antiq (Antiq _) = true;
    31 
    32 
    33 (* scan_antiquote *)
    34 
    35 structure T = OuterLex;
    36 
    37 local
    38 
    39 val scan_txt =
    40   T.scan_blank ||
    41   T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
    42   T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    43 
    44 fun escape "\\" = "\\\\"
    45   | escape "\"" = "\\\""
    46   | escape s = s;
    47 
    48 val quote_escape = Library.quote o implode o map escape o Symbol.explode;
    49 
    50 val scan_ant =
    51   T.scan_blank ||
    52   T.scan_string >> quote_escape ||
    53   T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
    54 
    55 val scan_antiq =
    56   T.keep_line ($$ "@" -- $$ "{") |--
    57     T.!!! "missing closing brace of antiquotation"
    58       (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
    59 
    60 in
    61 
    62 fun scan_antiquote (pos, ss) = (pos, ss) |>
    63   (Scan.repeat1 scan_txt >> (Text o implode) ||
    64     scan_antiq >> (fn s => Antiq (s, pos)));
    65 
    66 end;
    67 
    68 
    69 (* scan_antiquotes *)
    70 
    71 fun scan_antiquotes (s, pos) =
    72   (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
    73       (pos, Symbol.explode s) of
    74     (xs, (_, [])) => xs
    75   | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
    76       quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
    77 
    78 
    79 (* scan_arguments *)
    80 
    81 fun scan_arguments lex antiq (s, pos) =
    82   let
    83     fun err msg = cat_error msg
    84       ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
    85 
    86     val res =
    87       Source.of_string s
    88       |> Symbol.source false
    89       |> T.source false (K (lex, Scan.empty_lexicon)) pos
    90       |> T.source_proper
    91       |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
    92       |> Source.exhaust;
    93   in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
    94 
    95 end;